historyOrbitCardClass_eq_orbitCardClass
plain-language theorem explainer
For each triangulation class c of bound B, the history-orbit cardinality equals the ordinary gauge-orbit cardinality. Anyone assembling the history-built gauge measure ν cites this to swap history counting for banked orbit counting. The proof is a short card-congruence via the history-class/orbit equivalence, then definitional identification on the quotient out-representative.
Claim. Let $c$ be a triangulation class at bound $B$. Then the cardinality of the posted-history orbit of $c$ equals the gauge-orbit cardinality of $c$: $\lvert\mathrm{HistOrbit}(c)\rvert = \lvert\mathrm{GaugeOrbit}(c)\rvert$.
background
Module Wave C1 R5 builds a gauge-counting measure from a posted-history presentation of bounded complexes. A posted bounded history is a labeled bounded complex whose incidence indices are posting-alphabet elements of a dual-entry ledger state, pinned to the canonical balanced zero state so that dual-entry anchors the substrate without inflating the count. History relabeling is the posting-alphabet gauge redundancy.
The class measure is $\nu(c)=(#\text{ histories presenting }c)/(\text{history gauge volume of }c)$, and must match banked orbit/pair counts by explicit bijections, not by defining $\nu$ to be the banked mass. Two parallel orbit-size functions appear: the history-side orbit card of a triangulation class, and the banked orbitCardClass / gaugeOrbitCard from the exact-shell gauge preflight. This theorem equates them classwise.
Upstream, history_class_equiv_orbit supplies the set bijection between history presentations of $c$ and complexes equivalent to a fixed out-representative; Quotient.out_eq restores the class from that representative.
proof idea
Fix $c$. Let $K_0$ be Quotient.out c, so Quotient.mk (relabelSetoid B) K_0 = c by Quotient.out_eq.
Unfold the history-orbit card and rewrite by Nat.card_congr along history_class_equiv_orbit c. The resulting subtype card of complexes equivalent to $K_0$ is definitionally gaugeOrbitCard K_0 (rfl). Rewrite the right-hand side of the goal using the out-equation so both sides are the orbit card of the same representative, then close by rfl against orbitCardClass.
No arithmetic: pure transport of finite cardinality across the history/orbit equivalence plus quotient bookkeeping.
why it matters
Parent use is the headline nuBuild_gaugeCounting: the history-built mass satisfies GaugeCountingPrinciple. That proof unfolds nuBuild and needs history-side orbit sizes to agree with banked orbitCardClass / pair counts so the normalized ratio matches the gauge-counting identity.
In the Seven Gaps gravity stack this is residual R5 of the QG Wave C1 design: gauge counting from history without circular appeal to Aut/$\mu$. Equality with gaugeOrbitMass is allowed only through gaugeCountingPrinciple_iff_eq_gaugeOrbitMass; this lemma is the orbit-card half of that bridge. It keeps the dual-entry ledger present-and-pinned while the count is driven by posting/relabel degrees of freedom, aligning the history presentation with the banked shell gauge preflight used elsewhere in the gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.