evenPowerGeneratedNativeCost
plain-language theorem explainer
Specializes the power-generated native cost to even exponents n = 2k+2 on rational orbits. Anyone comparing continuum λ-family costs to the discrete carrier cites this family as the even-power countermodels. The body is a one-line specialization of the general power generator.
Claim. For each natural number $k$, the even-power native cost is the map on rational orbits sending $q$ to the cost generated by $q \mapsto q^{2k+2}$ (zero when $q=1$).
background
In the primitive recognition calculus, costs act on RatioOrbit: a signed-orbit numerator over a nonzero distinction-nat denominator, the discrete carrier of positive rationals. The general power generator sends an orbit $q$ to the orbit of $q^n$ (or zero at the unit), for every exponent $n \ge 1$.
On the continuum, the $\lambda$-family includes $F_2(x) = (x^2 + x^{-2})/2 - 1$, which satisfies reciprocity, normalization, and the composition law but fails unit calibration (curvature 4 rather than 1). Even powers on the carrier are the discrete analogues of that family.
The structural ledger isolates which native-cost hypotheses survive for each generator. Parity of the exponent decides sign-reversal: odd powers reverse orientation; even powers cannot tell $-q$ from $q$.
proof idea
One-line definitional wrapper: instantiate the general power-generated native cost at exponent $n = 2k+2$. No further proof obligations; all structural properties are inherited from the general power lemmas at that even index.
why it matters
Feeds the ledger theorems that even-power costs satisfy the full anchor-free package except sign reversal, and therefore fail the sans-anchor hypothesis package. Instantiates the square cost ($k=0$), the carrier analogue of continuum $F_2$, used to show the square misses the anchor and is non-canonical at 2.
Supports the headline comparison that the continuum gauge exceeds the native gauge: every positive real exponent is admissible after completion, while even exponents are refuted on the carrier. That gap is exactly what calibration collapses. Ties to J-uniqueness (T5) and the Recognition Composition Law by exhibiting discrete countermodels that match continuum composition but fail orientation, so the native forcing chain is stricter than its completed counterpart.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.