jq_inj_ge_one
plain-language theorem explainer
On rationals at least one, the native J-display is injective: equal costs force equal arguments. Anyone proving gauge rigidity or uniqueness of character-factored monotone costs on positive orbits cites this. The proof is a two-line antisymmetry sandwich through the order-reflection lemma for J.
Claim. Let $s,t\in\mathbb{Q}$ with $s\ge 1$ and $t\ge 1$. If $J(s)=J(t)$, where $J(x)=(x+x^{-1})/2-1$, then $s=t$.
background
The native cost display on rationals is $J_q(t)=(t+t^{-1})/2-1$, the same functional form forced at T5 in the unified forcing chain (also written $\cosh(\log t)-1$). It is nonnegative for $t>0$, vanishes only at the unit $t=1$, and is strictly monotone on $[1,\infty)$.
Order reflection is the companion fact: if $s,t\ge 1$ and $J_q(s)\le J_q(t)$, then $s\le t$. That lemma is proved by contraposing the strict monotonicity of $J_q$ above the unit. The present statement upgrades reflection of $\le$ to injectivity of $J_q$ on the same half-line.
The surrounding module builds a structural ledger for primitive recognition costs: characters on ratio orbits, cross-displays, and monotone factorizations through those characters. Injectivity of $J_q$ above one is the elementary real-arithmetic hinge that later turns agreement of costs into agreement of gauges.
proof idea
Term-mode proof by antisymmetry of $\le$ on $\mathbb{Q}$. From $J_q(s)=J_q(t)$ one gets both $J_q(s)\le J_q(t)$ and $J_q(t)\le J_q(s)$. Apply the order-reflection lemma jq_le_reflect in each direction (hypotheses $s\ge 1$, $t\ge 1$ are exactly its domain) to obtain $s\le t$ and $t\le s$. Conclude $s=t$ by le_antisymm. No case splits and no expansion of the formula for $J_q$ are needed at this layer.
why it matters
Immediate parent is structural_gauge_rigidity in the same ledger: two monotone costs that factor through ratio characters and agree at the single orbit $2$ agree on every positive integer orbit. Combined with the cube witness, that forces the free-side stratification (form forced, unit free). The other consumer, signedPowerNativeCost_one_not_oddPower, uses the same injectivity to separate the identity character cost from odd-power generated costs.
In the Recognition framework this is a local arithmetic face of T5 J-uniqueness: once $J$ is the forced cost, equal $J$-values on the region above the unit pin the underlying scale. Without injectivity above one, agreement of character-factored costs at a single orbit would not propagate to full gauge rigidity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.