squareGeneratedNativeCost_two_not_canonical
plain-language theorem explainer
The square-generated native cost at the ratio orbit 2 is not cross-equivalent to the canonical PRC J-cost J(2). Anyone auditing the structural native-cost ledger or the stratification certificate cites this. The proof rewrites cross-equality to rational equality, unfolds the square/even-power generators, and finishes by numeric evaluation of J.
Claim. The square-generated native cost at the ratio orbit $2$ is not cross-equivalent (under the PRC cross-multiplication relation) to the canonical $J$-cost on that orbit, $J(2)=((2+2^{-1})/2)-1$. Equivalently their rational displays differ, since the square construction yields a value matching $J(4)$ rather than $J(2)$.
background
In the Primitive Recognition Calculus, a RatioOrbit is an integer numerator over a nonzero orbit denominator: the internal rational display. Two such orbits are related by crossEq when cross-multiplication balances as signed orbits (K4.10); that relation agrees with equality of the verifier rationals via crossEq_iff_toRat_eq.
The canonical cost is PRC's rational $J$-object on a ratio orbit: $J(q)=((q+q^{-1})/2)-1$, written onRatioOrbit. The anchor point two is the ratio orbit with display $2$. The square-generated native cost is the even-power generator specialized to exponent $2$: it effectively evaluates a $J$-shaped cost at $q^2$ rather than at $q$.
This module builds a structural ledger of candidate native costs and records which constructions miss the anchor. The doc-comment states the content directly: the square cost misses because $J(4)\neq J(2)$; sign reversal already refutes the family, so this is a redundant second failure kept because the paper states it.
proof idea
Term/tactic hybrid, fully computational. Rewrite the goal with crossEq_iff_toRat_eq so the claim becomes inequality of rational displays. Unfold jq_onRatioOrbit, squareGeneratedNativeCost, evenPowerGeneratedNativeCost, and powerGeneratedNativeCost_toRat, then simplify the anchor with two_toRat. The resulting rational identity is discharged by norm_num on the closed-form jq evaluator: both sides become concrete rationals and fail to match.
why it matters
Feeds structuralStratificationCertificate_holds, which packages uniqueness, slim contraction, positivity, and the refutation that the structural family without the anchor is inhabited but non-unique. Recording that the square generator misses $J(2)$ is part of the gauge-rigidity story: among power-generated native costs, only the canonical $J$ sits on the anchor.
In the broader Recognition forcing chain this is local evidence toward T5 ($J$-uniqueness): alternative algebraic generators (here squares / even powers) produce a different cost surface. The paper states the $J(4)\neq J(2)$ miss explicitly; this lemma is the machine-checked ledger entry for that claim, even though sign reversal already kills the family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.