Manuscript Oai119-A@1 · Oai119-A.tex · section · fdff7292
Gate 4: asymmetric Hellinger induction and arithmetic
Stage 1: the five proof interfaces › Gate 4: asymmetric Hellinger induction and arithmetic · lines 661–725
Oai119-A@1#eq:Hrecursion, Oai119-A@1#eq:Henergy
Let be Boolean sections and on the remaining cube. The exact recursion is
The means of the sections may differ. Replacing them by a balanced pair would change the problem.
The 119-02 route uses asymmetric profiles before reflection, and a separately calibrated semigroup-energy continuation OpenAI119Induction,OpenAI119II. For , the elementary derivative underlying such a continuation is
whenever the field is interior. The identity follows from and symmetrization under coordinate flips. For a noised coordinate the derivative is . An estimate must preserve that calibration to preserve sharpness.
The source's finite arithmetic certificates concern scalar inequalities supporting this route OpenAI119Arithmetic. Their audit requires:
the complete parameter domain and every subdivision;
positivity of any cleared denominator;
nonnegative sides before squaring;
rigorous interval endpoints and series tails;
coverage of seams, singular limits, and all bias regimes;
the correct logical passage from the scalar estimates to the dimension-free assertion.
For example, nonnegative Bernstein coefficients prove the sign of a specified polynomial on a specified box because the Bernstein basis is nonnegative and sums to one. They do not identify an omitted polynomial or cover an omitted box.
We do not report execution of the source's certificates. The arithmetic in Section sec:finite instead belongs to our entirely specified sixteen-function instance.
Displayed formulas in this passage
Oai119-A@1#eq:Hrecursion · line 665
Oai119-A@1#eq:Henergy · line 682