track1_mixed_axis_coeff_cert_endpoint_holds
plain-language theorem explainer
The translation-normalized origin-offset residual coefficients for the corrected N=5 axis-stencil target vanish as an exact rational Lean certificate. Track 7 gravity handoff integration cites this Session 207 coefficient endpoint when assembling the fork receipt. The proof is a one-line term discharging the endpoint by the precomputed origin-residual vanishing lemma.
Claim. The Track 1 mixed-axis coefficient endpoint holds: the boolean certificate that the translation-normalized origin-offset residual coefficients of the corrected $N=5$ axis-stencil target are identically zero evaluates to true.
background
Track 7 is the integration-lane receipt for parallel gravity fork handoffs (Tracks 1.B stationarity, physical residual/Bianchi, many-body amplitude lift, Page capacity, dark-energy $w(z)$, and falsifier sensitivity). It records exactly what each new endpoint proves and does not upgrade the discovery claim; remaining Track 1 displacement-class leaves stay as the next dependency.
The endpoint proposition is the equality of the origin-residual coefficient vanishing flag to true. Its defining doc states that "the translation-normalized origin-offset residual coefficients for the corrected $N=5$ axis-stencil target vanish in Lean," while "the full unordered-pair table is still audited by the Python exact checker." This is the Session 207 coefficient leaf consumed by the handoff bundle.
proof idea
Term-mode one-line wrapper. The goal is the endpoint proposition, which is definitionally originResidualCoeffsZero = true. The proof applies the existing lemma originResidualCoeffsZero_eq_true and closes.
why it matters
Session 207 coefficient endpoint consumed by Track 7. It is wired into the integration-lane certificate instance that bundles the fork handoffs (many-body amplitude-linear lift, Schlaefli and displacement stationarity reductions, and sibling Track 1.B leaves).
In the Recognition gravity program this is a concrete exact-rational check: after translation normalization, the origin-offset residual coefficients of the corrected $N=5$ axis stencil vanish in Lean. That is algebraic bookkeeping on the discrete stencil, not a continuum GR derivation. The module keeps the remaining displacement-class leaves open; a nearby Session 208 split-row probe notes that one non-origin row also vanishes and that the full 125-row table should eventually be generated sparsely or replaced by translation invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.