gauge_orbit_contains_every_odd_power
plain-language theorem explainer
Every odd-power native cost satisfies the full anchor-free structural ledger, and distinct odd exponents disagree at the anchor ratio 2. Cited by anyone treating the two-calibration as a genuine unit gauge rather than forced structure. Proof is a term packaging of the sans-anchor satisfaction lemma with anchor injectivity.
Claim. For every natural number $k$, the native cost generated by the odd power indexed by $k$ satisfies the structural native-cost hypotheses with the anchor removed (base sans two-calibration, sign-reversing, monotone, and zero-calibrated doubled trace). Moreover, if $k \neq k'$, those two costs fail cross-equality when evaluated at the ratio orbit of $2$.
background
In the Primitive Recognition Calculus structural ledger, a native cost is a map on ratio orbits. The full structural package asks for several algebraic and order properties; the two-calibration (value at the ratio orbit of 2) is separated out as an anchor. The structure PRCStructuralNativeCostHypothesesSansAnchor is exactly that package with the anchor field deleted: base hypotheses without two-calibration, sign-reversal, monotonicity, and zero-calibration of the doubled trace.
The family oddPowerGeneratedNativeCost k builds candidate costs by odd-power generation. Cross-equality on ratio orbits is the native equality test used throughout the ledger. The surrounding module shows that the anchor-free ledger does not force the canonical cost: everything except the last field is structure, and the last field is a choice of unit.
Upstream cost notions (observer J-cost, multiplicative-recognizer derived cost, rung-coarsen weighted sums) supply the ambient language of recognition cost; this theorem stays inside the native ratio-orbit ledger.
proof idea
Term-mode packaging, no tactics. For each $k$ the proof returns a pair: the first component is oddPowerGeneratedNativeCost_sansAnchor k, which already proves the four sans-anchor structural fields for that odd-power cost; the second is the specialization of oddPowerGeneratedNativeCost_anchor_injective, which turns $k \neq k'$ into failure of cross-equality at the anchor ratio orbit of 2. No further algebraic work is done here.
why it matters
Establishes that the gauge orbit of anchor-free structural native costs is infinite: every odd exponent is an inhabitant, and distinct exponents are separated at the anchor. That is the precise content of the claim that the anchor is a genuine unit gauge rather than forced structure.
Downstream, cubeGeneratedNativeCost_two_not_canonical specializes the injectivity at exponents 1 and 0 to show the cube-generated cost at 2 is not the canonical on-orbit cost. native_ledger_refutes_the_square_cost uses the same orbit picture to exclude the continuum countermodel $\lambda=2$ by orientation reversal alone, without two-calibration. The stratification certificate structuralStratificationCertificate_holds records gauge_inhabited from the refutation of uniqueness for the sans-anchor target, which this infinite orbit underwrites.
In the broader RS forcing chain this sits at the foundation layer that isolates which ledger fields are structural versus unit choice, before J-uniqueness (T5) and $\varphi$-forcing (T6) lock the calibrated cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.