Track1MixedAxisRhsSoundnessEndpoint
plain-language theorem explainer
Aliases the N=5 three-axis stencil RHS soundness statement as the Track 1.B scalar finite endpoint for Session 230. Gravity auditors and the Track 7 fork-handoff certificate cite it when packaging the corrected stencil against the unordered coefficient expansion. The body is a one-line definitional wrapper equal to the upstream soundness proposition.
Claim. The Track 1 mixed-axis right-hand-side soundness endpoint is the proposition that, for every five-vertex potential $\xi$, the axis-stencil residual at $N=5$ equals the unordered three-axis coefficient expansion of $\xi$.
background
This module is the Track 7 integration-lane receipt for parallel fork handoffs in the gravity master theorem. It records what each fork endpoint proves without upgrading the discovery claim, and leaves remaining Track 1 displacement-class leaves open.
The upstream proposition asserts that the corrected three-axis stencil is sound with respect to the unordered coefficient expansion: for every vertex potential $\xi$ on five vertices, the axis-stencil residual equals that expansion. That closes the RHS half of the finite scalar comparison at $N=5$.
In the Recognition gravity stack, Track 1.B concerns stationarity and stencil reductions feeding the structural master theorem. The mixed-axis RHS endpoint is the Session 230 packaging of that soundness fact for handoff into Fork A / Track 7.
proof idea
Definitional alias only: the endpoint proposition is definitionally identical to the upstream axis-stencil coefficient soundness statement at $N=5$. No extra proof obligations are introduced here; discharge is deferred to the companion theorem that applies the upstream certificate.
why it matters
Gives Track 7 a named RHS soundness receipt for Session 230 Track 1.B. The companion theorem proves the endpoint holds by invoking the upstream $N=5$ soundness certificate, and the fork handoff integration structure consumes related Track 1 reduction endpoints as part of the multi-fork package.
Per the module framing, this is a reduction/interface package, not a closure of the open Schläfli leaves. It sits beside other Track 1 endpoints (Schläfli reduction, disp0 base-vertex and stationary reductions, seven-stationarity) that the integration certificate records without claiming full master-theorem closure.
No direct T0–T8 forcing step is discharged here; the role is gravity-side stencil bookkeeping for the handoff lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.