Pith. sign in
module module high

IndisputableMonolith.Gravity.Track1BCorrectedQuadratic

show as:
view Lean formalization →

Defines the local cubic-Taylor gate for Track 1.B gravity: near the flat configuration the nonlinear Regge action equals its flat value plus half a candidate quadratic Q, with a controlled cubic remainder. Legacy Q is the periodic edge-stencil Dirichlet action; the Session-202 correction uses the canonical periodic mixed-axis stencil. Gravity auditors cite it as the N=5 corrected-quadratic certificate. The module packages correspondence predicates, uniqueness of the quadratic, and native_decide residual bounds.

claimNear the flat configuration, the full nonlinear Regge action equals its flat value plus $\frac12 Q$, up to a controlled cubic remainder, for a candidate quadratic $Q$. The legacy Track 1.B choice is the periodic edge-stencil Dirichlet action; the corrected choice is the canonical periodic mixed-axis stencil action. At $N=5$ the corrected gate is closed by an exact residual certificate.

background

Recognition Science gravity work packages discrete Regge calculus on a finite lattice and asks which quadratic form correctly captures the second variation of the nonlinear action about the flat background. The local cubic-Taylor correspondence asserts that, in a neighborhood of the flat configuration, the full action is flat value plus half $Q$ plus a remainder of cubic order in the defect variables.

Two candidate quadratics compete. The legacy Track 1.B target 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 checks for the $N=5$ mixed explicit-fiber residual, no floating point). Upstream damped-schedule closure supplies the uniform residual schedule that the product-filter datum previously carried as a free hypothesis.

The module therefore sits at the interface between stencil coefficient certificates and the Taylor-gate statements used by higher-cardinality reductions.

proof idea

The module is a theorem package, not a single lemma. It introduces correspondence predicates equating the local Taylor expansion of the Regge action to a named quadratic $Q$, then specializes to the edge-stencil and mixed-axis stencils. Uniqueness results show that if two correspondences hold then the underlying quadratics agree; a companion non-equality lemma separates the two stencil quadratics, so both correspondences cannot hold simultaneously. Nonnegativity and scalar-homogeneity lemmas for the canonical mixed-axis and periodic edge actions support the algebraic bookkeeping. Residual bounds (normalized Regge minus half-quadratic controlled in absolute value) are discharged by exact certificates, including native_decide over the $5^3=125$ vertex table at $N=5$, feeding the corrected gate closure.

why it matters in Recognition Science

This module is the corrected local-Taylor gate for Track 1.B at $N=5$. Downstream, CorrectedTaylorHigherCardinality records that the gate closed here via the native_decide certificate over the 125-vertex table, and lifts the result to higher cardinality by parameterized reduction. Track1BCompilerTrustStatus records in a machine-checkable structure that the corrected gate relies on native_decide and therefore extends the kernel basis, listing the extra axioms introduced.

In the broader RS gravity stack the corrected mixed-axis stencil replaces an incorrect legacy quadratic, so subsequent curvature and continuum-limit arguments rest on the Freudenthal-audited coefficients rather than the edge-only Dirichlet form. The module does not itself derive continuum Einstein equations; it locks the discrete second-variation identification that those arguments consume.

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)