Realize the released stronger witness within half of the finite loss budgets

Open

mme_more_asymmetry_released_witness_finite_log_recipe_half_loss

by Eyal1990 · Sep 21, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

entropymatrix-multiplication

Construct a genuine finite logarithmic regional recipe for the released q=5 More Asymmetry witness on 4n original copies, with n>0, positive input count, and positive matrix volume. Its certified rates satisfy

\log(\mathrm{outputs})-\log(\mathrm{inputs})\ge n(2.81302098456-0.0000005)

and

\log(abc)\ge n(3\cdot 2.09612367517-0.00000005).

This strengthens the published finite-loss target by using half of each allowed loss budget. It isolates the core finite-realization obligation: actual integer profiles, source inclusions, unique type covers, recursive compatibility, boundary maps, and checked logarithmic budgets.

Preamble

import Definitions.Def_mme_logarithmic_regional_CW_recipe
open MME MME.ProfiledCW MME.RegionRealization
set_option autoImplicit false

Formal statement

theorem mme_more_asymmetry_released_witness_finite_log_recipe_half_loss :
    ∃ (n ell : ℕ) (P : Predicate (4 * n)) (D : LogRecipe (4 * n) ell P),
      0 < n ∧ 1 ≤ D.inputs ∧ 1 ≤ D.a * D.b * D.c ∧
      (n : ℝ) * ((281302098456 : ℝ) / 100000000000 - 1 / 2000000) +
          Real.log (D.inputs : ℝ) ≤ D.logOutputs ∧
      (n : ℝ) * (3 * ((209612367517 : ℝ) / 100000000000) - 1 / 20000000) ≤
          Real.log ((D.a * D.b * D.c : ℕ) : ℝ) := by sorry

Source

More Asymmetry, arXiv:2404.16349v2; W1.00_2.371339.mat SHA256 783353fda82acb3fb93c247dcad857b2db5f61944f5d0e91ae5f9e5a6c7feec3

View graph