track1TotalSymmetryStationarityReductionEndpointProjectionCount_eq_one
plain-language theorem explainer
The Track 1 total-symmetry stationarity-reduction endpoint has projection count exactly one. Gravity auditors cite it as the Session 572 Track 7 receipt that total stationarity plus displacement symmetry closes the canonical N=5 weighted-deficit stationarity target in a single projection. The proof is pure definitional reflexivity.
Claim. The projection count attached to the Track~1 total-symmetry stationarity-reduction endpoint equals $1$.
background
This module is the Track 7 fork-handoff integration lane for gravity. It records what parallel forks prove without upgrading the discovery claim. Fork A is the Track 1.B stationarity reduction at $N=5$ (the Schläfli / weighted-deficit side); remaining displacement-class leaves stay open as the next dependency.
Hinge deficit is the geometric primitive: at a simplicial hinge one takes $2\pi - \sum\theta$ (DihedralAngle / Schläfli deficit). The stationarity target is the canonical $N=5$ weighted-deficit critical-point problem on that hinge data. "Total symmetry" plus displacement symmetry is the reduction that collapses the stationarity problem onto a single projection class.
The named count is the bookkeeping integer for how many independent projections that reduced endpoint contributes. Upstream canonical objects (arithmetic, dyadic protocols, completed traces, self-similar dressings) appear only as ambient Recognition scaffolding; they are not rewritten here.
proof idea
Term-mode one-liner: rfl. The left-hand side is a definitionally closed natural-number constant whose unfolding is already $1$, so no lemmas or tactics are required. The equality is pure definitional identity of the projection-count binder with the numeral one.
why it matters
Inside Track 7 this is the numeric receipt that the total-symmetry stationarity reduction lands on a single projection, matching the Session 572 claim that total stationarity plus displacement symmetry closes the canonical $N=5$ weighted-deficit target directly. It sits with the sibling Track 1 endpoint holds (Schläfli reduction, disp0 base-vertex / stationary, seven-stationarity, etc.) as fork-A bookkeeping rather than a new dynamical law.
No downstream consumers are wired yet (used_by empty); the value is integration hygiene so later Master-Theorem assembly can quote a proved count instead of a free parameter. It does not touch T5–T8 forcing, RCL, or the $\phi$-ladder mass formula; it only certifies the projection arity of one gravity stationarity handoff.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.