structural_gauge_rigidity
plain-language theorem explainer
Two monotone native costs that factor through ratio characters and agree at the orbit of 2 agree on every positive-integer orbit. Cited by anyone proving free-side cost stratification: form forced, only the unit free. Proof extracts multiplicative orientations from each character factorization, equates them at 2 via the anchor, then applies gauge uniqueness of monotone multipliers.
Claim. Let $F_1,F_2$ be monotone maps on ratio orbits, each equal (cross-display) to the native cost built from a ratio character $\chi_1$ resp. $\chi_2$. If $F_1$ and $F_2$ agree at the orbit of $2$, then $F_1(a)=F_2(a)$ (cross-display) for every orbit $a$ that displays a positive integer.
background
The module builds a structural ledger for the primitive recognition calculus (PRC) native cost on ratio orbits. A ratio orbit is an equivalence class of positive rationals under the recognition identification; toRat picks a canonical display. An orbit is a positive-integer orbit when that display equals some $n\in\mathbb{N}$ with $n\ge 1$.
Monotonicity means cost is nondecreasing along positive-integer orbits as the rational display grows. A ratio character is a multiplicative map on orbits; the native cost of a character is the closed-form $J$-cost $j_q$ of the character's rational display (the same $J(x)=(x+x^{-1})/2-1$ forced at T5). Factorization hypotheses say each $F_i$ is cross-equal to that character cost.
Upstream, monotone character factorizations yield oriented multiplicative gauges (monoMult_of_character), and those gauges are rigid once they agree at a single integer $\ge 1$ (monoMult_gauge with injectivity of $j_q$ on $[1,\infty)$).
proof idea
Rewrite each $F_i$ display as $j_q$ of the character value via crossDisp and costFromCharacter_jq. From each monotone character factorization obtain an oriented mono-multiplier $(k_i,H_{k_i})$ with $j_q\circ k_i$ matching the character on natural orbits.
The anchor $F_1(2)\sim F_2(2)$, transported through character display at natOrbit 2, gives $j_q(k_1(2))=j_q(k_2(2))$. Injectivity of $j_q$ on values $\ge 1$ plus monoMult_gauge forces $k_1=k_2$ on all $n\ge 1$.
For a general positive-integer orbit $a$ with display $n$, reduce cross-equality of $F_1(a)$ and $F_2(a)$ to equality of $j_q(k_i(n))$ and finish by the equated multipliers.
why it matters
This is the gauge half of free-side stratification: once the cost factors through a character and is monotone, a single real anchor at the orbit of 2 fixes the unit; the functional form is already forced by arithmetic. The module doc states the slogan directly: form forced by arithmetic alone, residual freedom only the size of the unit.
Downstream it is consumed by structuralStratificationCertificate_holds, which packages uniqueness, slim contracts, positivity, and inhabited gauge into the round-6 structural certificate. In the broader RS chain this sits under T5 $J$-uniqueness and the Recognition Composition Law: the ledger shows the countable carrier admits no second independent cost shape, only a calibration choice, matching the "cube witness / anchor is the only free parameter" claim in the doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.