D08_refuted
plain-language theorem explainer
For carrier bound 2, the named invariance axioms on weight functions admit at least two distinct solutions. Gravity and Gap-2 authors cite this when ruling out uniqueness-from-invariance as a route to the asymmetric insertion rates. The proof is a one-line specialization of the general underdetermination theorem at bound 2.
Claim. There exist distinct real-valued weight functions $w_1,w_2$ on bounded complexes of size at most $2$ such that both satisfy the named invariance axioms: $\mathrm{InvarianceAxioms}(2,w_1)$, $\mathrm{InvarianceAxioms}(2,w_2)$, and $w_1\neq w_2$.
background
Gap-2 Room B is a necessary-reasons census for insertion asymmetry: recognition structure is asked whether it forces the asymmetric carrier-enlarging rate law (one creation opportunity per tick, one deletion choice per existing label), or a counting-equivalent law not baked from a weight. The target is a search directive, never a premise.
D08 packages the claim that invariance-type axioms underdetermine the measure: there are at least two distinct weights on BoundedComplex 2 both satisfying InvarianceAxioms. Upstream, invariance_underdetermines_measure states the same existential for every bound $B\ge 2$, witnessed by the pair (muMeasure B, uniformMeasure B).
In the census, this row is the invariance no-go: if several measures share the axioms, invariance alone cannot select the unit or counting member needed for the asymmetric rates.
proof idea
One-line wrapper. Apply invariance_underdetermines_measure at bound $B=2$, discharging $2\le 2$ by norm_num. That upstream theorem returns the pair muMeasure 2 and uniformMeasure 2 with their satisfaction proofs and the inequality muMeasure_ne_uniformMeasure. No local algebra beyond the specialization.
why it matters
Closes the D08 row in the insertion-asymmetry reasons table: invariance axioms admit distinct measures, so they cannot force a unique weight and therefore cannot by themselves pick the asymmetric counting rates over decoys. Downstream, insertionAsymmetryReasons_certified packages the D10/D11 closures, scored decoys, the D12 wall, D13/D14 ledger work, and later pins; it explicitly does not move the measure flag, consistent with this underdetermination.
In the broader SevenGaps gravity stack this is a negative selection result: measure uniqueness fails at the invariance layer, pushing the census toward rate-sensitive kernels, ledger move multiplicities, and freshness forcing rather than pure symmetry axioms. It sits beside the D12 scoped wall (bare posting reachability is blind to the attached rate law) as a structural limit on what recognition-as-typed can select.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.