value_route_is_encoding_choice
plain-language theorem explainer
On any two-site recognition ledger, the single off-diagonal cost can be forced either to equal the symmetry-factor measure μ of a bounded complex or to vanish, by choice of encoding alone. Anyone arguing that gauge counting is read off ledger cost must therefore import a canonical complex-to-ledger map; the ledger axioms do not pick one. The proof exhibits two explicit encodings (uniform and flat) and checks μ of the two-point complex is nonzero.
Claim. For every bound $B \ge 2$ there exist two encodings $\mathrm{enc},\mathrm{enc}'$ from $B$-bounded complexes into recognition ledgers on two sites such that, for every complex $K$, the off-diagonal cost of $\mathrm{enc}(K)$ equals the symmetry-factor measure $\mu(K)$, while the off-diagonal cost of $\mathrm{enc}'(K)$ is identically zero, and moreover $\mu$ of the two-point complex is nonzero.
background
Gap 2 of the gravity seven-gaps program asks whether a recognition ledger can supply the gauge-counting measure that assigns mass $1/|\mathrm{Aut}|$ to complexes. The module kills one natural route: reading the measure from the ledger's site-symmetry count on vertex sites. On a two-element site type every recognition ledger is a symmetric zero-diagonal matrix, hence fixed by the transposition, so site-symmetry cardinality is always 2; yet the edgeless pair and the single directed edge have $|\mathrm{Aut}|=2$ and $1$ respectively.
A second candidate route remains: ignore symmetry counts and read the measure straight off the single free cost entry $\mathrm{cost},0,1$. The symmetry-factor measure $\mu$ is the target readout (orbit-stabilizer mass). A recognition ledger on $\mathrm{Fin},2$ is determined by that one nonnegative off-diagonal number. The uniform ledger places a chosen $t\ge 0$ off-diagonal; the flat ledger places zero. Both satisfy the ledger axioms.
The local claim is that this value route is fitting, not deriving: the same identity readout returns $\mu$ under one encoding and the wrong answer under another.
proof idea
Term-mode existence proof. The first encoding sends each complex $K$ to the uniform ledger whose off-diagonal cost is $\mu(K)$ (well-defined by positivity of $\mu$). The second encoding is constantly the flat ledger on $\mathrm{Fin},2$. The three conjuncts are discharged by: the off-diagonal lemma for the uniform ledger, definitional reduction of the flat ledger cost to $0$, and rewriting $\mu$ of the two-point complex followed by a numeric check that the result is nonzero.
why it matters
This is the named import for the open measure obligation under Gap 2 (R2): any derivation of GaugeCountingPrinciple that routes through recognition ledgers must bring a canonical encoding from complexes to ledgers, forced rather than chosen. Neither the ledger axioms nor the two-site carrier supplies one.
Downstream, siteSymmetry_is_chosen_by_the_encoding lifts the same moral from the value route on two sites to the symmetry route on three or more sites: the axioms admit both a fully symmetric ledger and a ledger that breaks a given transposition. Together with the site-blindness results of §§3–4, the module closes the shape "read measure off ledger site data" and forces the derivation to import orientation-carrying or simplex-site structure instead.
In the broader RS forcing chain this is scaffolding hygiene around gauge counting in gravity, not a T0–T8 landmark; it constrains how the recognition substrate may feed mass assignments without claiming a positive derivation of $G$ or $\alpha$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.