structural_character_calibrated_on_positive_integers
plain-language theorem explainer
A structural native cost that factors through a ratio character forces that character to act as the identity, up to global reciprocal, on every positive integer orbit in J-display. Uniqueness proofs for the canonical recognition cost from the structural ledger cite this as the round-5 engine. The argument builds a monotone multiplicative map on the naturals from the character, pins its value at 2 by the orbit-2 calibration, and applies the monotone-multiplicative pinning lemma.
Claim. Let $F,\chi$ map ratio orbits to ratio orbits. Assume $F$ obeys the structural native-cost ledger (base native hypotheses, sign reversal, monotonicity, and zero-orbit calibration), $\chi$ is a ratio character, and $F(q)$ is cross-equal to the cost reconstructed from $\chi$ at every orbit $q$. Then for every integer $n\ge 1$, $J\bigl((\chi(\mathrm{natOrbit}\,n))^{\mathrm{toRat}}\bigr)=J(n)$, where $J$ is the rational recognition-cost display (so identity and global reciprocal are indistinguishable under $J$).
background
Ratio orbits package positive rational scales up to the equivalences the recognition engine treats as identical. The display map toRat extracts a rational representative; natOrbit n is the orbit of the positive integer $n$, with display exactly $n$. The function $J$ (written jq on rationals) is the standard recognition cost $J(x)=(x+x^{-1})/2-1$, which is blind to $x\mapsto x^{-1}$.
A ratio character $\chi$ is a multiplicative, unit-preserving, nonzero-preserving map on orbits. Cost-from-character rebuilds a native cost by composing $\chi$ with $J$. The structural ledger on $F$ is the round-5 package: the slim native base (reciprocity, normalization invariance, nonzero composition, unit-zero, single orbit-2 anchor), plus sign reversal, monotonicity on positive-integer orbits, and zero-orbit calibration. Compared with earlier ledgers, prime-pair product families and signed-unit calibrations that named the canonical cost are absent.
Cross-equality identifies orbits that agree in rational display. The hypothesis that $F$ is cross-equal to cost-from-character of $\chi$ means $F$ is the $J$-display of $\chi$ at every orbit.
proof idea
Classical mode. First, character respect for cross-equality is obtained from the proved normalize-ratio canonical target, so $\chi$ depends only on rational display. Define $g(n)=(\chi(\mathrm{natOrbit},n))^{\mathrm{toRat}}$. The structural factorization hypothesis plus cost-from-character display rewrites $(F q)^{\mathrm{toRat}}$ as $J((\chi q)^{\mathrm{toRat}})$.
Unit preservation gives $g(1)=1$. Multiplicativity of $\chi$ and of natOrbit give $g(mn)=g(m)g(n)$. Nonzero-preservation keeps $g(n)\ne 0$ for $n\ge 1$. Monotonicity of $F$ on positive-integer orbits, transported through the display rewrite, yields monotonicity of $J\circ g$.
The native two-calibration forces $J(g(2))=J(2)$, hence $g(2)\in{2,2^{-1}}$ by the two-cases lemma for $J$. Package $g$ (and pointwise $g^{-1}$) as monotone-multiplicative data. On the $g(2)=2$ branch, the monotone-multiplicative pinning lemma gives $J(g(n))=J(n)$ directly. On the reciprocal branch the same lemma applied to $g^{-1}$ plus $J(x)=J(x^{-1})$ closes the claim.
why it matters
This is the round-5 engine named in the doc-comment: the character attached to a structural cost is the identity in $J$-display on every positive integer orbit, up to the reciprocal orientation the cost cannot see. The sole downstream consumer is the round-5 terminal PRCStructuralNativeCostUniquenessTarget_proved, whose doc-comment states that the structural ledger forces the canonical cost. That terminal factors $F$ through a character via the zero-calibrated native factorization target, then invokes this calibration on integer orbits to pin the cost.
In the broader Recognition framework the result sits under T5 $J$-uniqueness ($J(x)=\cosh(\log x)-1$) and the Recognition Composition Law: once integer orbits are forced to the identity display, the structural axioms leave no room for a non-canonical native cost. It closes the countable integer skeleton without reintroducing prime-pair product families or signed-unit calibrations that previously named the canonical cost by hand. No open scaffold remains on this path; the claim status is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.