state_factored_weight_is_complex_function
plain-language theorem explainer
Any weight that factors through complex and dual-entry state collapses, on the pinned (canonical) carrier, to a function of the complex alone. Gravity and gauge-counting workers cite it when arguing that the posting layer injects no state-dependent factor into counts routed through CanonicalHistory. The proof builds that complex-only map by evaluating at the balanced zero state and rewrites via the pin equality.
Claim. Fix a bound $B\in\mathbb{N}$. Let $F$ assign to each bounded complex $K$ of bound $B$ a real weight on dual-entry strain states over the posting alphabet of $K$. Then there exists $g$ depending only on the complex such that, for every canonical (state-pinned) history $\mathrm{CH}$ of bound $B$, $F(\mathrm{underlying}(\mathrm{CH}),\,\mathrm{state}(\mathrm{CH}))=g(\mathrm{underlying}(\mathrm{CH}))$.
background
Gap 2 of the gravity completion track asks whether the gauge-counting principle can be derived from substrate structure richer than bare counting at the posting layer. The module's committed answer is no, split into three parts: what the pinned carrier contains by design, a uniqueness wall that excludes invariant enrichments, and the routes the wall does not touch.
Counted histories are built by pinning every dual-entry strain state to the balanced zero state, so there is one counted history per complex and the count does not inflate. The unpinned posted history still carries a free dual-entry state; the pin discards it. A state-factored weight is any real assignment $F(K,s)$ of complex and state. On the pinned carrier the state is forced equal to the balanced zero state, so such an $F$ can only see the complex.
This is a theorem about the design of the pinned carrier, not a discovery that the posting layer is empty. The free state lives one type up; any derivation that routes through the pinned counted carrier has only the complex to work with.
proof idea
Term-mode existence proof. Witness the complex-only map by $g(K):=F(K,\mathrm{balancedZeroState})$. For an arbitrary canonical history $\mathrm{CH}$, the field state_canonical supplies the equality of its dual-entry state with the balanced zero state on the underlying complex. Applying congruence in the second argument of $F$ (with the underlying complex fixed) rewrites $F(\mathrm{underlying},\mathrm{state})$ into $g(\mathrm{underlying})$. No further lemmas are needed.
why it matters
This is part one of the pinned-carrier floor: together with the companion count identity (canonical count equals complex count), it shows that anything state-factored contributes nothing beyond the complex once histories are pinned. Downstream, R06_pinned_weights_are_complex is a direct re-export under the inevitable-reasons index, and index_audit conjoins it with the uniqueness wall (invariant enrichment forces Gibbs) and the equivariant-cost non-contribution theorem.
In the Recognition gravity story this closes the honest reading of Track A1.2: a derivation of the gauge-counting principle that routes through the pinned counted carrier receives no state-dependent posting-layer factor. What remains open is exactly what the module names in part three: premise-level justifications of the Gibbs weight itself, and label-asymmetric structure on the unpinned carrier. Those are scoped out, not refuted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.