Track1MixedAxisExplicitFiberLhsSoundnessEndpoint
plain-language theorem explainer
Names the Track 1.B Session-230 endpoint asserting that, at five vertices, the real explicit-fiber mixed left-hand side equals the rational unordered coefficient expansion. Gravity auditors and Track-7 handoff consumers cite it as the scalar finite LHS soundness receipt. The body is a pure Prop alias of the upstream N=5 soundness statement.
Claim. The Track-1 mixed-axis explicit-fiber LHS soundness endpoint is the proposition that for every five-vertex potential $\xi$, the real explicit-fiber mixed left-hand side at $N=5$ equals the unordered rational coefficient expansion of that same left-hand side.
background
This module is the Track-7 integration-lane receipt for parallel fork handoffs in the gravity master-theorem stack. It records what each fork endpoint proves without upgrading the discovery claim, and keeps remaining Track-1 displacement-class leaves as open dependencies.
The upstream statement being aliased is the $N=5$ explicit-fiber mixed LHS coefficient soundness fact: for every vertex potential $\xi$ on five vertices, the real explicit-fiber mixed left-hand side equals the unordered rational LHS coefficient expansion. That equality identifies two quadratic forms, one written in the real fiber geometry and one in the rational unordered coefficient model.
Track 1.B is the scalar finite / stationarity-reduction lane of the gravity program (Fork A in the handoff list). The mixed-axis explicit-fiber LHS is the concrete residual side being certified before residual and Bianchi interfaces are packaged further downstream.
proof idea
Definitional alias only. The Prop is definitionally equal to the upstream $N=5$ soundness proposition (explicit-fiber mixed LHS equals unordered rational coefficient expansion for every five-vertex potential). No tactics, no new proof obligations; the holding theorem later discharges it by citing the corresponding upstream certificate.
why it matters
Gives Track 7 a named Session-230 receipt for scalar finite LHS soundness on the mixed-axis explicit-fiber side. The companion holding theorem asserts this endpoint, and the fork handoff integration certificate consumes Track-1 reduction/interface packages alongside many-body, Page-capacity, dark-energy $w(z)$, and falsifier-sensitivity handoffs.
Per the integration certificate, the structural master theorem still uses structural witnesses where required; Track-1 contributions here are reduction/interface packages, not closure of the open Schläfli leaves. In the broader Recognition gravity stack this pins the finite $N=5$ LHS model agreement that later residual and stationarity arguments rely on, without claiming full master-theorem closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.