track1TotalSymmetryStationarityEndpointProjectionCount_eq_one
plain-language theorem explainer
The Track 1 total-symmetry stationarity endpoint has projection count exactly one. Gravity handoff integrators cite this as the receipt that the direct conformal Schläfli-along-line route is a single projection, not a multi-leaf fan. The equality is definitional: the count reduces by reflexivity to the numeral 1.
Claim. The projection count attached to the Track 1 total-symmetry stationarity endpoint equals $1$.
background
This module is the Track 7 fork-handoff integration lane for gravity. It records what parallel endpoints actually prove without upgrading the discovery claim. Fork A is the Track 1.B 1B-SCH stationarity reduction at tetrahedron count $N=5$; remaining displacement-class leaves stay as open dependencies.
Two competing stationarity surfaces sit in the sibling cluster. One is the seven per-displacement-class stationarity targets. The other is a single total-symmetry route: the conformal Schläfli identity $V(t)=0$ along a line, which closes the full $N=5$ weighted-deficit stationarity target in one stroke and bypasses the seven-class fan.
The declaration names the projection count of that total-symmetry endpoint. In the handoff ledger, a count of one means the route collapses to a single projection leaf rather than a multi-endpoint bundle.
proof idea
Term-mode one-liner: rfl. The left-hand side is a definitional natural-number constant (or an abbrev that unfolds to one), so Lean closes the equality by reflexivity with no lemmas, rewrites, or case splits.
why it matters
In the Recognition gravity stack this is bookkeeping, not new physics: it certifies that the total-symmetry stationarity handoff projects to exactly one endpoint. That matches the intended Fork A story in which classical Schläfli along a conformal line, summed over tetrahedra at $N=5$, should discharge the full weighted-deficit stationarity input without walking the seven displacement-class leaves.
No downstream consumers are wired yet (used_by is empty), so the theorem is a ledger receipt inside MasterTheoremHandoffIntegration. The real open surface named beside this cluster is proving the canonical periodic conformal Schläfli-along-line target at $N=5$; once that holds, the full Track 1.B stationarity input follows. This count result only locks the projection arity of that route to one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.