orbitCellCount_eq_classification
plain-language theorem explainer
For each lattice hinge orbit type, the committed per-orbit cell multiplicity equals the enumerated count of oriented triangle slots of matching popcount class. Gravity analysts assembling the zero-momentum 4D Regge Hessian cite this to justify the hard-coded weights 72/48/48/24/24 against the classification sum. The proof is a pure case split with definitional equality on each constructor.
Claim. For every hinge orbit type $\tau$ under coordinate permutation, the committed cell multiplicity of $\tau$ equals the number of oriented triangle slots in a 4-cell whose edge-class popcount pair matches the popcount pair associated to $\tau$.
background
This module assembles the flat second-variation class quadratic of the 4D Regge action at zero momentum. Orbit types are the lattice classes of hinges under coordinate permutation: the inductive family with constructors for popcount patterns $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$. Each type carries a committed cell multiplicity used as a true weight in the Hessian sum.
The classification side counts oriented triangle slots directly: sum over the 24 simplex orientations and 10 triangle choices of the indicator that the slot has a given popcount pair. The local map from orbit type to that pair is the bridge between the two sides.
Upstream, the multiplicity table is the definition sending those five types to $72,48,48,24,24$. The classification count is the double sum that enumerates matching slots. The module scope is zero-momentum per-cell Hessian only; finite-momentum Bloch folding remains open.
proof idea
Term-mode proof by exhaustive case analysis on the orbit-type inductive. For each constructor the left-hand multiplicity is a numeral and the right-hand side reduces, via the popcount map and the classification sum definition, to the same numeral, so rfl closes every goal. No lemmas beyond definitional unfolding are required.
why it matters
The equality lets downstream code replace a hard-coded weight table by the geometric slot enumeration. Its sole recorded consumer is the Bloch-side theorem that the oriented slot count for each orbit type equals the committed cell count: that proof rewrites through this identity, then unfolds the classification sum and compares indicators pointwise.
In the QG campaign this underwrites deliverable A item 3 of the module: the orbit-count-weighted sum of area-gradient times deficit-kernel contributions that builds the true-weight flat Hessian. Those weights (not reverse-engineered from Einstein–Hilbert) are what kill pure gauge on the decoy modes at zero momentum. The result does not touch continuum EH recovery or the gap-action flag; it only certifies internal consistency of the discrete orbit bookkeeping used by the Hessian assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.