squareGeneratedNativeCost
plain-language theorem explainer
The square-generated native cost is the discrete carrier analogue of the continuum λ=2 countermodel cost. It is the map on ratio orbits obtained by specializing the even-power generator at index 0. Structural-ledger theorems cite it to show that orientation reversal alone excludes this cost without continuum-style calibration. The body is a one-line abbreviation of that generator.
Claim. Define the square-generated native cost as the map $\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ equal to the even-power generated native cost at power index $0$. It is the carrier analogue of the continuum countermodel cost at $\lambda=2$ (the square cost).
background
In the primitive recognition calculus, costs act on ratio orbits: equivalence classes of positive rational ratios under the discrete recognition group. The native J-cost on orbits is the discrete stand-in for the continuum cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law and T5 uniqueness.
The continuum side admits a one-parameter family of countermodels; the $\lambda=2$ member (square cost) satisfies every structural axiom except a calibration hypothesis that pins the second derivative at the identity. This definition packages the matching free-side object so the ledger can test those axioms on the carrier without importing continuum calibration.
Upstream, even-power generators build orbit maps from character powers; index 0 yields the square case. Sibling facts record nonnegativity and closed-form values of the orbit J-cost used when comparing anchors.
proof idea
Pure definitional abbreviation: the map is defined to be evenPowerGeneratedNativeCost evaluated at power index $0$. No proof obligations; downstream theorems unfold this equality and reduce via the power-generator evaluation lemmas and the orbit J-cost closed form.
why it matters
This object is the free-side witness that the continuum $\lambda=2$ countermodel is already killed by orientation (sign) reversal on the carrier. The parent theorem native_ledger_refutes_the_square_cost shows the square-generated cost meets every structural native-cost hypothesis except the anchor package, and fails orientation reversal alone, so the free ledger refutes the continuum countermodel without calibrating.
A second parent, squareGeneratedNativeCost_two_not_canonical, records the redundant anchor miss $J(4)\neq J(2)$ that the paper also states. Together they tighten the forcing path toward unique native J (T5 landmark) by exhibiting an explicit non-canonical cost that structural axioms exclude before any continuum limit is taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.