encoding_unconstrained
plain-language theorem explainer
Any non-negative assignment of reals to bounded complexes is realized exactly as the off-diagonal cost of some encoding into two-site recognition ledgers. Anyone claiming the ledger axioms force a unique complex-to-ledger map (or a measure read from that map) must confront this freedom. The proof is a one-line existential packaging of the uniform-ledger construction.
Claim. For every $B \in \mathbb{N}$ and every $f$ sending $B$-bounded complexes to non-negative reals, there exists a map $\mathrm{enc}$ from those complexes into recognition ledgers on a two-element site type such that $(\mathrm{enc}\,K).\mathrm{cost}(0,1) = f(K)$ for every complex $K$.
background
Gap 2 of the Seven Gaps program asks whether the recognition ledger can supply the gauge-counting measure by reading site symmetry: how many relabelings of the site type leave the ledger cost fixed. On a two-element site type a recognition ledger is a symmetric zero-diagonal cost matrix, hence determined by the single number $\mathrm{cost}(0,1)$. The transposition therefore fixes every such ledger, while two two-vertex complexes (edgeless pair vs single directed edge) have different automorphism counts.
A recognition ledger on sites $S$ is the substrate carrier of pairwise cost. Bounded complexes are the combinatorial objects whose automorphism counts the gauge-counting principle wants to convert into masses $1/|\mathrm{Aut}|$. The uniform ledger on two sites is the ledger whose sole off-diagonal entry equals a prescribed non-negative real; sibling lemmas record that this construction is well-typed and that its off-diagonal cost recovers the input.
The module's local claim is conditional: under the premise that the candidate measure factors through site-symmetry cardinality on the vertex site type, gauge counting fails. This theorem isolates the encoding step of that argument.
proof idea
Term-mode existential. The witness encoding sends each complex $K$ to the uniform two-site ledger whose off-diagonal cost is $f(K)$, using non-negativity of $f(K)$ to satisfy the ledger cost axiom. The second component of the pair is the sibling identity that the uniform ledger's cost between $0$ and $1$ equals the prescribed value. No further case analysis or induction.
why it matters
This is the named import for the open measure obligation: any derivation that encodes complexes as ledgers and reads a measure off cost has its answer supplied by the encoding, not by the ledger axioms. Downstream, R16_refuted is literally the application of this theorem, discharging one inevitable-reason candidate in the gauge-counting catalogue. The sibling headline siteSymmetry_is_chosen_by_the_encoding lifts the same freedom to three-or-more sites, showing both fully symmetric and transposition-breaking ledgers are admitted by the axioms.
In the Gap 2 no-go, this closes the "value route is fitting, not deriving" half: the identity readout on off-diagonal cost returns the symmetry-factor measure under one encoding and the wrong answer under another. Combined with the two-site blindness (every ledger is fixed by the transposition while complexes are not), it forces any successful derivation to import either an orientation-carrying refinement of the ledger or sites for simplices rather than vertices alone. It does not touch status flags; it only kills one shape of substrate premise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.