Rational profile pairs approach any admissible real rate
Provedmme_stothers_theorem53_rational_dense_rateEvery rate achievable by a real stationary pair is achievable by an integral one.
Let be strictly positive real ten-class profiles with and , the two-dimensional kernel of the marginal map spanned by the displayed vectors and . Then for every
there are strictly positive integral profiles with the same nine-grade marginals, , whose normalised partner is again stationary, , and which already beat :
The point is that is cut out by two binomial relations, and , both homogeneous of degree three. Binomial equations are solvable for one variable in terms of the others, so the positive rational points of are dense in its positive real points — one approximates eight coordinates freely and defines the remaining two by the relations, which then hold exactly rather than approximately. Homogeneity means no normalisation is needed to stay on . Together with the fact that is spanned by two integer vectors, both profiles can be produced directly as integers on a common marginal fibre.
This is what turns the integral form of Theorem 5.3 into the real one: the rate is continuous in the profile on the positive orthant, so a strict inequality at the real pair survives the approximation.
Formalization note. The construction is explicit. At scale one takes ceilings of eight coordinates, multiplies through by to clear denominators, and sets the second and third coordinates to and ; the two relations then hold as identities in . The companion profile is obtained by adding integer multiples of the two kernel vectors, which changes neither the marginals nor the class-weighted total.
import Definitions.Def_mme_stothers_general_outer_profile open MME BigOperators Filter set_option autoImplicit false
theorem mme_stothers_theorem53_rational_dense_rate
(tau : ℝ) (a b : Fin 10 → ℝ)
(hb : MME.StothersFourth.InN b)
(haPos : ∀ i, 0 < a i) (hbPos : ∀ i, 0 < b i)
(hsame : MME.StothersFourth.InY (fun i ↦ a i - b i))
(V : ℝ)
(hVlt : V < MME.StothersFourth.globalRate 6 tau a a *
(MME.StothersFourth.entropyProduct b / MME.StothersFourth.entropyProduct a)) :
∃ base bstar : Fin 10 → ℕ,
(∀ r, 0 < base r) ∧ (∀ r, 0 < bstar r) ∧
(∀ j, MME.StothersFourth.genMarginalBaseCount bstar j =
MME.StothersFourth.genMarginalBaseCount base j) ∧
MME.StothersFourth.InN (MME.StothersFourth.genProfileB bstar) ∧
V < MME.StothersFourth.globalRate 6 tau
(MME.StothersFourth.genProfileB base)
(MME.StothersFourth.genProfileB base) *
(MME.StothersFourth.entropyProduct (MME.StothersFourth.genProfileB bstar) /
MME.StothersFourth.entropyProduct (MME.StothersFourth.genProfileB base)) := by
sorry