constantWeight
plain-language theorem explainer
The constant unit weight assigns mass 1 to every carrier size n. It is the baseline decoy measure in the Gap-2 label-insertion census: equal per-slot birth and death rates put it in detailed balance, yet it fails InsertionStationarity (hence fails the gluing law). Downstream D02/D03/D06 and the composite certificate cite it as the symmetric counterexample. The definition is the constant function n ↦ 1.
Claim. Define the constant unit weight $w:\mathbb{N}\to\mathbb{R}$ by $w(n)=1$ for every carrier size $n$.
background
Gap-2 asks whether an explicit carrier-enlarging label-insertion/removal dynamics can force InsertionStationarity (equivalently the GluingLaw), and thereby inverse factorials and the GaugeCountingPrinciple, without smuggling in $\mu$, Aut, unit fugacity, or stationarity under another name.
In that setting a weight is a map $w:\mathbb{N}\to\mathbb{R}$ on carrier size. Detailed balance relates consecutive weights to birth and death rates. InsertionStationarity is the structural fixed-point condition that selects the factorial (gluing) weights. The constant unit weight is the simplest size-blind measure: every $n$ carries mass 1.
The module runs a necessary-reasons census: each candidate rate law is proved, left open, recorded as model, or refuted. Symmetric equal-per-slot rates are the first decoy; they balance this constant weight and therefore cannot force the gluing law.
proof idea
One-line definition: the function sending every natural number to the real $1$. No proof obligations.
why it matters
This decoy weight is the reference object for the refuted selectors in the Gap-2 census. D02 shows equal-per-slot rates put it in detailed balance; D03 packages that with the failure of InsertionStationarity at $n=1$, so counting insertion slots and deletion choices the same way does not force the gluing law. D06 uses the same failure against baked-from-weight rates. The composite certificate labelInsertionDynamics_certified and the corrected floor plans list it explicitly, and the InsertionAsymmetryInevitableReasons module reuses D02/D03.
Framework role: Gap-2 sits in the gravity/gluing stack that aims at measure structure without assuming stationarity. The constant weight makes precise why a size-symmetric dynamics is insufficient; the still-open item is a recognition-derived asymmetry (size-blind birth vs per-label death, or equivalent $\mu_{n+1}=(n+1)\lambda_n$ from move counts). The measure flag gap2_measure_derived remains unmoved until that asymmetry is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.