R16_refuted
plain-language theorem explainer
Any pointwise non-negative real assignment on bounded 2-complexes is realized exactly as the off-diagonal cost of some two-site recognition-ledger encoding. Gap-2 gauge-counting census work cites this to close the ledger-cost-readout route to the Gauge Counting Principle. The proof is a one-line application of the unconstrained-encoding theorem on bound 2.
Claim. For every function $f$ from bounded complexes of bound $2$ into $\mathbb{R}$ with $f(K)\ge 0$ for all $K$, there exists an encoding of those complexes into recognition ledgers on two sites such that the ledger cost between the two sites equals $f(K)$ for every complex $K$.
background
Gap 2 in the gravity stack asks whether richer RecognitionLedger / posting-layer structure forces the Gauge Counting Principle (GCP) for physical class mass, equivalently $\nu=1/|\mathrm{Aut}|$. This module runs a necessary-reasons census: every candidate fact that would make GCP unavoidable is proved, left open, recorded as model, or refuted.
Reason R16 is the ledger-cost-readout candidate: if ledger axioms constrained which costs a complex may carry, that constraint might select the gauge-orbit measure. The proposition asserts the opposite freedom: every non-negative assignment on BoundedComplex 2 is realized exactly as the off-diagonal cost of some encoding into RecognitionLedger (Fin 2).
Upstream, encoding_unconstrained already states the same freedom for general bound $B$: "the ledger axioms therefore say nothing about which ledger a complex should become." R16 is that statement specialized to $B=2$.
proof idea
One-line wrapper. Introduce the assignment $f$ and its non-negativity hypothesis, then apply encoding_unconstrained at bound $2$. That upstream theorem builds the encoding by sending each complex to a uniform ledger whose single off-diagonal cost equals $f(K)$, using the uniform-ledger off-diagonal identity.
why it matters
In the Gap-2 necessary-reasons census this declaration discharges R16 as a proved freedom statement, thereby refuting ledger-cost readout as a derivation of GCP from richer structure. The module doc lists that route among the REFUTED candidates (alongside invariant enrichment, equivariant posting cost, bare-posting gluing, unit fugacity from posting+gluing, size-blindness, and label indifference).
A failed reason does not automatically install its opposite; it forces a corrected floor plan. With ledger costs unconstrained, any remaining path to GCP must come from elsewhere (the residual open selector named in the module is an action-first prior). No downstream theorem yet consumes this fact; it stands as a census closure entry rather than a lemma in a longer derivation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.