evenPowerGeneratedNativeCost_sans_signReversing
plain-language theorem explainer
Even-power native costs F(q)=q^{2k+2} satisfy the full anchor-free structural ledger except orientation (sign) reversal: reciprocity and normalization, monotonicity on positive integer orbits, and doubled-trace zero calibration. Cited when isolating the single field that kills the continuum λ=2 countermodel on the carrier. Proof is a three-component term packing the power-generated base, monotone, and zero-calibration lemmas at exponent 2k+2.
Claim. For every natural number $k$, the native cost generated by the even power $q \mapsto q^{2k+2}$ satisfies: (i) the base native-cost hypotheses without the two-point anchor (reciprocity and normalization invariance), (ii) monotonicity on positive integer orbits, and (iii) zero calibration of its doubled-trace character.
background
In the Primitive Recognition Calculus structural ledger, native costs are maps $F$ on ratio orbits. The base pack without the two-point anchor (PRCNativeCostHypothesesSansTwoCalibration) requires reciprocity $F(q)\sim F(q^{-1})$ and invariance under distinction normalization. Monotonicity asks that on positive integer orbits, larger imbalance never lowers cost. Doubled-trace zero calibration pins the character at the identity orbit.
Even-power generators are the special case of power-generated costs at exponent $n=2k+2$: $F(q)=q^{2k+2}$. The continuum countermodel costLambdaTwo (the $\lambda=2$ square cost) is exactly the $k=0$ case; the carrier analogue is squareGeneratedNativeCost. Upstream lemmas already show every power-generated cost (any $n$) meets the base pack and monotonicity, and any nonzero exponent meets zero calibration of the doubled trace.
The local module builds a ledger that separates structural fields so each continuum countermodel can be pinned to a single missing axiom on the discrete carrier.
proof idea
Term-mode triple. Instantiate the three power-generated lemmas at exponent $n=2k+2$:
powerGeneratedNativeCost_base (2*k+2)supplies reciprocity and normalization (the sans-two-calibration pack).powerGeneratedNativeCost_monotone (2*k+2)supplies orbit monotonicity.powerGeneratedNativeCost_zero_calibratedat $n=2k+2$, with the side condition $n\neq 0$ discharged byomega, supplies doubled-trace zero calibration.
The even-power wrapper is definitionally powerGeneratedNativeCost (2*k+2), so no extra rewriting is needed. The whole proof is the triple constructor of the three conjuncts.
why it matters
Feeds native_ledger_refutes_the_square_cost, which shows the free side refutes the continuum's $\lambda=2$ countermodel without any calibration hypothesis: the square cost meets every structural field except orientation reversal. The doc-comment states the point cleanly: even-power costs satisfy the whole anchor-free ledger apart from sign reversal, so exclusion is attributable to exactly one field.
In the Recognition framework this is ledger hygiene for native-cost uniqueness. Continuum J-uniqueness (T5) and the Recognition Composition Law need discrete counterparts that do not smuggle continuum calibration. By exhibiting an infinite family (all even powers) that clears every field except sign reversal, the ledger isolates orientation as the sole remaining filter. That filter is what kills the square-cost countermodel on the carrier and keeps the native cost on the J-track toward the unique continuum cost $J(x)=\cosh(\log x)-1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.