Manuscript Oai119-A@1 · Oai119-A.tex · section · fdff7292

Release: the completed plan and unchanged general claims

Release: the completed plan and unchanged general claims · lines 1631–1709

Stage	Completed task	Status
0	Uniform input, independent symmetric noise, the two profiles, information units, external statements, and formalization scope are distinguished.	Frozen; no external general theorem is a premise.
1	Scalar, joining, semigroup, asymmetric Hellinger, arithmetic, and implication interfaces are audited.	Elementary identities proved; universal proof obligations remain explicit.
2	A concrete sampler and finite-sample allowance are supplied. Comparison ledgers retain their own interfaces.	No decoder or resource optimum is inferred from a template.
3	The exact kernel, posterior tables, equality example, and strict numerical gaps are printed.	Evaluation supplied for the frozen instance.
4	Input law, independence, summary type, functional, coding task, and quantum interface are varied separately.	No silent hypothesis weakening.
5	Thermal, gravitational, temporal, and recovery readings are kept separate.	No standing physical problem is solved.
6	The one selected finite Hellinger theorem is proved, with the Courtade–Kumar conclusion as a corollary.	Completed by Theorem thm:finite and Corollary cor:finiteCK.

The exact mathematical conclusion is

n = 2, ρ = \frac{1}{2}, H (E f) - E H (T_{1/2} f) \leq 1 - \frac{3}{2}, equality exactly for \pm x_{1}, \pm x_{2}, Γ (f) > \frac{27}{1000} for every other Boolean function, \frac{102}{1000} < Γ (x_{1} x_{2}) < \frac{103}{1000}, I_{2} (f (X); Y) \leq 1 - h_{2} (1/4), information gap > \frac{1}{50} bit for every nonsigned-coordinate function .

The finite certificate now exists. The following conclusions still do not follow:

independent verification of 119-01 or 119-02;
a completed proof of the inspected Lean targets;
formalization of 119-02's thm:main by targets that name 119-01;
a noncommutative fidelity inequality, a quantum mutual-information inequality, or a collective-measurement optimizer;
a Page curve or a gravity test.

These are logical scope boundaries. They do not assert that other researchers cannot prove a broader statement independently, or that no proof exists elsewhere.

Displayed formulas in this passage

unlabeled · line 1676
$n = 2, ρ = \frac{1}{2}, H (E f) - E H (T_{1/2} f) \leq 1 - \frac{3}{2}, equality exactly for \pm x_{1}, \pm x_{2}, Γ (f) > \frac{27}{1000} for every other Boolean function, \frac{102}{1000} < Γ (x_{1} x_{2}) < \frac{103}{1000}, I_{2} (f (X); Y) \leq 1 - h_{2} (1/4), information gap > \frac{1}{50} bit for every nonsigned-coordinate function .$