pinning_is_a_counting_normalization
plain-language theorem explainer
Over any fixed labeled complex the fiber of counted (canonical) histories is a singleton. Gap-2 workers cite this to separate the measure's pinning from questions of which letter charges are admitted. One-line wrapper of the canonical-history fiber-uniqueness lemma; packaged as a def because Unique is Type-valued.
Claim. For every natural number $B$ and every bounded complex $K$ of bound $B$, there is a unique canonical history whose underlying complex equals $K$. Equivalently, the fiber of counted histories over a labeled complex is a singleton.
background
Gap 2 asks whether the letter-cost space forces the kind rule: a letter's cost depends only on its kind, via the same three reals at every complex. An earlier module derived a posted kind-only cost normalized at the atoms and left open whether the substrate forces that rule. The present module works strictly inside the letter-cost layer (not the dual-entry ledger below it).
GaugeHistoryMeasure pins counted histories to the balanced zero dual-entry state. A natural reading is that this pinning is what excludes countermodel charges (incidence-aware or non-constant counts-only charges). The type of letter cost, however, takes only a complex and an alphabet letter, never a dual-entry state, so the pinning cannot see those charges.
A canonical history is a counted history whose underlying labeled complex is fixed and whose state is the canonical balanced zero. The uniqueness of that fiber is what makes orbit counts on counted histories coincide with orbit counts on labeled complexes.
proof idea
One-line wrapper: the definition is definitionally CanonicalHistory.fiber_unique applied to the given bounded complex $K$. No extra algebra; the content is the naming and the Type-valued packaging via Unique.
why it matters
Inside the T2 arc of the Gap-2 kind-rule module, this declaration records what the pinning actually does: it is a counting normalization (exactly one counted history per complex), not a filter on admissible charges. That separation blocks the tempting claim that the measure's state pin excludes incidence or pair-cost countermodels. Those exclusions, if they exist, must come from elsewhere (the measure formula, size-blindness, or a future state-bearing cost carrier).
The module header stresses the referee-required scope: letter-cost space only. Whether the dual-entry lattice one layer below forces the kind rule remains the open successor. No downstream consumers are wired yet; the def is a named restatement for the T2 narrative and for later measure-orbit equalities that need the fiber to be a singleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.