ext
plain-language theorem explainer
Two counted histories of the same bound are equal whenever their posted carriers coincide. Anyone rewriting or transporting data along CanonicalHistory equality will cite this extensionality lemma. The proof is a short cases/rfl destructuring: the Prop field pinning the dual-entry state is proof-irrelevant once the carriers match.
Claim. Fix a bound $B \in \mathbb{N}$. Let $\mathrm{CH}_1$ and $\mathrm{CH}_2$ be counted histories of bound $B$ (each a posted bounded history together with a proof that its dual-entry state is the canonical balanced zero). If the underlying posted carriers are equal, then $\mathrm{CH}_1 = \mathrm{CH}_2$.
background
This module builds the Wave C1 R5 gauge-counting measure from a posted-history presentation. A posted bounded history is a labeled bounded complex whose incidence indices are posting-alphabet elements of a dual-entry ledger state. History relabeling is treated as posting-alphabet gauge redundancy; the class measure is $\nu(c) = (#\text{ histories presenting }c)/(\text{history gauge volume of }c)$.
A counted history packages that posted carrier with an explicit Prop that the dual-entry state equals the canonical balanced zero (debit = credit = 0, mag = 0). Dual-entry is therefore present-and-pinned rather than erased, so arbitrary state fields cannot inflate the history count. The structure is parameterized by a natural bound $B$.
The field named $H$ on a counted history is exactly that posted carrier. Equality of counted histories is what this extensionality rule reduces to carrier equality.
proof idea
Term-style tactic proof with four steps. Destructure the first counted history into carrier plus canonical-state proof; destructure the second the same way. Cases on the hypothesis that the two carriers are equal, which identifies the carrier components. The remaining Prop fields both assert equality to the balanced zero state on the (now identical) carrier, so rfl closes by proof irrelevance. No external lemmas are invoked.
why it matters
Extensionality is the practical equality interface for counted histories in the gap-2 gauge-counting stack. Downstream constructions that define $\nu$ via history counts, or that transport along presentation bijections with banked orbit/pair counts, need to know that a counted history is determined by its posted carrier once the state is pinned.
The module's design adjudication insists that dual-entry anchors the substrate reading while the count is driven only by posting/relabel degrees of freedom. This lemma makes that design operational: equality ignores the Prop witness and tracks only the carrier. No used_by edges are recorded yet; the lemma is infrastructure for the nuBuild / GaugeCountingPrinciple development rather than a paper-level forcing step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.