R06_reason
plain-language theorem explainer
State-factored weights on the pinned carrier collapse to functions of the underlying bounded complex alone. Auditors of the Gap-2 gauge-counting necessary-reasons census cite this as the R06 entry: pinned weights reduce to complex counting. The proof is a one-line wrapper that applies the already-proved collapse lemma for state-factored weights.
Claim. For every bound $B\in\mathbb{N}$ and every family of real weights $F$ sending each bounded complex $K$ of bound $B$ to a function of dual-entry strain states on the posting alphabet of $K$, there exists $g$ depending only on the underlying complex such that for every canonical history $CH$, $F(CH.\mathrm{underlying}, CH.H.\mathrm{state})=g(CH.\mathrm{underlying})$.
background
The module is a necessary-reasons census for Gap-2 measure structure. Richer RecognitionLedger and posting-layer data are assumed to force the Gauge Counting Principle for physical class mass (equivalently $\nu=1/|\mathrm{Aut}|$). Each candidate reason is scored proved, open, model, or refuted; a failed reason forces a corrected floor plan rather than its opposite.
R06 is the pinned-carrier collapse item. A dual-entry strain state records the posting-layer configuration on a bounded complex; a canonical history pairs an underlying complex with such a state. The claim is that any weight depending on complex and strain state, when evaluated on canonical histories, factors through the underlying complex alone.
Upstream, the collapse is already stated as the lemma that state-factored weights are complex functions on the pinned carrier. The census entry simply records that proposition as an inevitable reason.
proof idea
One-line wrapper. Introduce the bound $B$ and the weight family $F$, then apply the upstream lemma that state-factored weights collapse on the pinned carrier. That lemma itself reduces to the general fact that a state-factored weight is a function of the underlying complex. No extra algebra is done at this site.
why it matters
This is the census packaging of R06 as THEOREM in the gauge-counting inevitable-reasons table. It underwrites the module honesty line that the pinned carrier collapses to complex counting, one of the positive theorems beside invariance underdetermination, the GCP equivalence with gauge-orbit mass, and the failure of uniform class mass.
No downstream consumers are recorded; the declaration scores a reason rather than feeding a parent derivation of GCP. It sits next to the sibling on pinned-count complexity and opposite the refuted routes (invariant enrichment, equivariant posting cost, bare-posting gluing, unit fugacity from posting+gluing, size-blindness, ledger-cost readout). The residual open selector remains an action-first prior outside the R18 rebooking wall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.