Pith. sign in
module module high

IndisputableMonolith.Gravity.Track1BCorrectedQuadratic

show as:
view Lean formalization →

Local cubic-Taylor gate: near the flat configuration the nonlinear Regge action equals its flat value plus half a candidate quadratic Q, up to a controlled cubic remainder. Gravity workers on Track 1.B cite the legacy edge-stencil instance and the Session-202 corrected mixed-axis instance. The module also proves uniqueness of each quadratic under its correspondence and that the two quadratics are distinct. Argument is by local expansion plus certified stencil coefficients.

claimNear the flat configuration, the full nonlinear Regge action equals its flat value plus $\frac12 Q$, up to a controlled cubic remainder, for an arbitrary candidate quadratic $Q$. Legacy Track 1.B takes $Q$ as the periodic edge-stencil Dirichlet action; the corrected target takes $Q$ as the canonical periodic mixed-axis stencil action. Each correspondence forces uniqueness of its quadratic; the two quadratics are not identical.

background

Track 1.B in the RS gravity stack asks for a local Taylor match between the nonlinear Regge action and a discrete quadratic stencil near the flat background. The match is cubic-order: action = flat value + (1/2)Q + O(cubic), with the remainder controlled on a neighborhood of the flat configuration.

Two candidate quadratics appear. The legacy choice is the periodic edge-stencil Dirichlet action. Session 202 replaces it by the canonical periodic mixed-axis stencil action, whose coefficients are audited by the Freudenthal axis-stencil certificate (exact rational monomial check at N=5, no floating point). Upstream D2 damped-schedule closure supplies the uniform residual schedule used in the product-filter setting rather than leaving it as a free hypothesis.

The module therefore treats an abstract local-quadratic correspondence predicate, specializes it to both stencils, and records nonnegativity and scaling lemmas for the actions.

proof idea

The module is a theorem package, not a single lemma. It defines the abstract Regge-local-quadratic correspondence (flat value + half Q + cubic remainder), then the edge-stencil and canonical mixed-axis specializations. Uniqueness of Q under each correspondence is proved by comparing two quadratics that both satisfy the same local expansion. A separate non-coincidence theorem shows the two stencil quadratics differ, so both correspondences cannot hold for unequal Q. Normalized remainder bounds (absolute deviation of the normalized Regge residual from half the quadratic) are obtained from the correspondence hypothesis together with the certified axis-stencil coefficients. Several one-line scaling and nonnegativity facts for the periodic actions support the gate statements used downstream at N=5.

why it matters in Recognition Science

This module is the corrected local-Taylor gate for Track 1.B at the quadratic level. Downstream, CorrectedTaylorHigherCardinality lifts the N=5 native_decide certificate (5³ = 125 vertex table) to higher cardinality and parameterized reduction, quoting that Track1BCorrectedQuadratic closed the corrected gate at N=5. Track1BCompilerTrustStatus records that the N=5 corrected gate relies on native_decide and therefore extends the kernel basis, packaging that fact as a machine-checkable CompilerTrustStatus.

In the broader RS gravity program the gate separates the legacy edge stencil from the Session-202 mixed-axis stencil and forces any accepted Q to be the unique quadratic compatible with the local expansion. It sits on the Freudenthal coefficient certificate and the D2 schedule closure, so the residual and the stencil weights are derived rather than postulated.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (17)