native_ledger_refutes_the_square_cost
plain-language theorem explainer
The square (λ=2) native cost meets every structural ledger field except orientation reversal, so the free-side structural package without the two-point anchor already excludes it. Continuum uniqueness needs calibration to kill this countermodel; the discrete carrier does not. Cite when separating continuum freedom from carrier stratification. The proof is a two-component pair of even-power lemmas at index 0.
Claim. Let $F$ be the square-generated native cost on ratio orbits (the $\lambda=2$ even-power cost). Then $F$ satisfies the native-cost base package without two-point calibration, is monotone on positive integer orbits, and has doubled-trace zero calibration; yet $F$ fails the structural native-cost package without anchor (equivalently: it is not sign-reversing). Thus the free structural ledger refutes the continuum's square countermodel without any calibration hypothesis.
background
In the Primitive Recognition Calculus, native costs are maps $F$ on ratio orbits. The base package without two-point calibration is the RCL-style structural field set minus the two-point anchor. Monotonicity says that on positive integer orbits, if $a\le b$ in rational value then $(F a)\le(F b)$. Doubled-trace zero calibration constrains the doubled-trace form of $F$ at the identity class.
The structural ledger without anchor packages four fields: that base package, sign-reversal (orientation reversal under ratio inversion), monotonicity, and doubled-trace zero calibration. Sign-reversal is the only field the square cost fails.
Local setting: this module builds a structural stratification certificate for native costs on the carrier. On the continuum every positive real exponent is an admissible cost; the square cost is the exact continuum countermodel that uniqueness theorems cannot exclude without calibration. The carrier analogue is already killed by orientation alone.
proof idea
Term-mode pair proof. The left conjunct is evenPowerGeneratedNativeCost_sans_signReversing 0, which supplies base-sans-two-calibration, monotonicity, and doubled-trace zero calibration for the even-power family at index 0 (the square generator). The right conjunct is evenPowerGeneratedNativeCost_not_sansAnchor 0, which shows the same $F$ fails the structural package without anchor, because sign-reversal fails. No further tactic work: the theorem is the pairing of those two even-power facts.
why it matters
Feeds structuralStratificationCertificate_holds, which assembles uniqueness, slim contraction, positivity, and the fact that the structural package without anchor is inhabited only after the continuum countermodels are cut. The doc-comment states the point cleanly: the free side refutes the continuum's countermodel without calibrating; λ=2 is exactly what continuum uniqueness cannot exclude without calibration, and its carrier analogue is excluded by orientation reversal alone.
Framework role: this is part of forcing the native J-cost shape on the discrete carrier (toward T5 J-uniqueness and the RCL), by showing that even-power continuum freedom does not transport. Related module note: odd powers remain in the gauge orbit; whether anything beyond that orbit exists is the named transcendence wall. Closes a stratification gap rather than an open sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.