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

Back to manuscript

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:

  1. the complete parameter domain and every subdivision;

  2. positivity of any cleared denominator;

  3. nonnegative sides before squaring;

  4. rigorous interval endpoints and series tails;

  5. coverage of seams, singular limits, and all bias regimes;

  6. 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