Released More Asymmetry witness: graded global joint finite recipe
Provedmme_more_asymmetry_global_graded_finite_witnessThere exist n > 0, a level ell and a graded global start D on 4n positions of CW_5 with at least one input and positive matrix volume, such that
n (2.81302098456 - 10^-6) + log(inputs) <= logOutputs
and
n (3 * 2.09612367517 - 10^-7) <= log(a b c).
This is the global joint finite witness with graded-source constituent steps. The released More Asymmetry parameters (published as exact rationals in mme_more_asymmetry_released_parameters_data) meet both rates exactly, with slack of about 10^-6 and 10^-7 for finite-length losses.
The graded form is needed for the construction to chain its stages. With ordinary integer steps, the source of each constituent stage must contain its whole typical band, including words in which a few parent blocks have the wrong shape. The global stage's exact outputs fix every block's shape, so they cannot cover such words. Enumerating nearby shape patterns as extra types is ruled out by the divisibility requirement on split counts.
import Definitions.Def_mme_global_CW_graded_start_data open MME MME.GlobalCW set_option autoImplicit false
theorem mme_more_asymmetry_global_graded_finite_witness :
∃ (n ell : ℕ) (D : GlobalCW.StartG (4 * n) ell),
0 < n ∧ 1 ≤ D.inputs ∧ 1 ≤ D.a * D.b * D.c ∧
(n : ℝ) * ((281302098456 : ℝ) / 100000000000 - 1 / 1000000) +
Real.log D.inputs ≤ D.logOutputs ∧
(n : ℝ) * (3 * ((209612367517 : ℝ) / 100000000000) - 1 / 10000000) ≤
Real.log ((D.a * D.b * D.c : ℕ) : ℝ) := by sorry