evenPowerGeneratedNativeCost_not_sansAnchor
plain-language theorem explainer
Every even-power native cost on ratio orbits fails the structural ledger once the anchor is dropped: it cannot be sign-reversing. Anyone comparing continuum reciprocal costs (especially the λ=2 countermodel) to the carrier ledger cites this. The proof is a one-line reduction to the general even-exponent non-sign-reversal lemma with exponent 2k+2.
Claim. For every natural number $k$, the native cost generated by the even power map $q \mapsto q^{2k+2}$ on ratio orbits does not satisfy the structural native-cost hypotheses with the anchor removed (base axioms without two-calibration, sign-reversal, monotonicity, and doubled-trace zero-calibration).
background
In the primitive recognition calculus, native costs are maps on ratio orbits induced by power generators. The even-power family is q ↦ q^(2k+2), the carrier analogue of the continuum countermodel cost with exponent λ=2 (and its even powers). The structural ledger without anchor packages four properties: the base native-cost axioms minus two-calibration, sign-reversal (orientation flip under reciprocal ratios), monotonicity, and zero-calibration of the doubled trace.
On the continuum side, every positive real exponent yields a reciprocal cost obeying the composition law; excluding λ=2 needs an extra calibration hypothesis. On the carrier, the even-power generators are candidates for that countermodel. The sibling fact that power-generated native costs fail sign-reversal precisely when the exponent is even and at least 2 is the upstream lever used here.
Local setting: the structural ledger module that separates which continuum gauge freedoms survive on the discrete carrier without invoking the two-calibration anchor.
proof idea
Assume for contradiction that the even-power native cost at $k$ meets the sans-anchor structural hypotheses. Extract the sign_reversing field. Apply the general lemma that power-generated native costs are not sign-reversing whenever the exponent is even and positive: instantiate that lemma at $n = 2k+2$, witnessing evenness by $n = 2(k+1)$, and feed it the extracted sign-reversal hypothesis. Contradiction. Pure term-mode reduction; no extra arithmetic beyond the ring witness for evenness.
why it matters
This is the uniform even-power obstruction that lets the free carrier refute continuum countermodels without calibration. Downstream, native_ledger_refutes_the_square_cost specializes to the square ($k=0$) case: the λ=2 cost "is the exact function the continuum theorem cannot exclude without the calibration hypothesis" and "is excluded by orientation reversal alone." The same fact feeds continuum_gauge_exceeds_native_gauge, which records that the continuum scale family does not transport: even exponents admissible on the line are absent from the carrier orbit, while odd exponents remain.
In Recognition terms this sharpens the gap between the continuum J-cost orbit (forced by T5 uniqueness and the Recognition Composition Law after calibration) and the native ledger on ratio orbits. Part of what calibration collapses is freedom that exists only after completion to the reals. It does not itself force φ or the eight-tick structure; it clears a structural false friend of the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.