Track1LocalCorrespondenceReducedToMixedLengthEndpoint
plain-language theorem explainer
Packages Track 1.B after Schläfli closure: at the canonical N=5 scale, the local Regge/J-cost edge-stencil correspondence is reduced to a single remaining obligation, the mixed hinge-deficit length-chain identity. Gravity auditors and Track 7 handoff consumers cite it as the named reduction interface. It is a pure Prop abbreviation (implication), not a proved closure.
Claim. At the canonical certificate scale $N=5$, the mixed hinge-deficit length-chain identity implies the local Regge/$J$-cost edge-stencil correspondence (periodic cubic six-tet Dirichlet instance).
background
Track 7 is the fork-handoff integration lane for gravity: it records what parallel endpoints prove without upgrading the discovery claim. Fork A covers Track 1.B stationarity reduction at $N=5$; this definition is the packaging endpoint for the local correspondence leaf of that fork.
The consequent is the Track 1.B local Regge/$J$-cost correspondence target at $N=5$: edge-stencil agreement between the discrete Regge geometry and the Recognition $J$-cost on the canonical periodic instance. The antecedent is the mixed hinge-deficit length-chain target at the same scale. Upstream notes that Session 202 finite audits find the old edge-stencil surface wrong-weighted as stated; the abbreviation is kept for packaging while a corrected mixed/Hessian target is named.
$J$ is the unique cost from the forcing chain ($J(x)=(x+x^{-1})/2-1$). The setting is discrete gravity on a six-tet cubic Dirichlet stencil, not continuum GR.
proof idea
No proof body: this is a Prop definition equating the packaging name to the implication
CanonicalPeriodicMixedHingeDeficitLengthChainTargetAtN5 → CanonicalPeriodicEdgeStencilLocalCorrespondenceAtN5
(both specialized at $N=5$ with decidable side conditions). Discharge is separate: the sibling theorem applies canonicalPeriodicEdgeStencilLocalCorrespondenceAtN5_of_mixedLengthChain to inhabit the implication.
why it matters
Gives Track 7 a single named reduction interface for Fork A’s local-correspondence leaf after Schläfli packaging. Downstream, track1_local_correspondence_reduced_to_mixed_length_endpoint_holds asserts the implication; ForkHandoffIntegrationCert and fork_A_B_C_D_E_F_handoffs_integrated_one_statement consume the Track 1 reduction package alongside many-body, Page-capacity, $w(z)$, and falsifier-sensitivity handoffs.
Per the integration cert, Track 1 here is a reduction/interface package, not closure of open Schläfli or displacement-class leaves. Session 202 still flags scalar inconsistency of the old mixed length-chain RHS with exact finite $N=5$ data, so the remaining obligation is live. Lands in the gravity master-theorem stack that ties discrete Regge structure to Recognition $J$-cost, short of an unconditional discovery theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.