GaugeOrbitIsOddPowerFamily
plain-language theorem explainer
The proposition asserts that every map on ratio orbits satisfying the anchor-free structural native-cost ledger is cross-equivalent to the cost generated by some odd power q ↦ q^(2k+1). Classification workers cite it as the first candidate shape of the gauge orbit. It is a pure Prop definition packaging that universal claim; the claim itself is false and has a dedicated refutation.
Claim. Every $F : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$ that satisfies the anchor-free structural native-cost hypotheses is, for some $k \in \mathbb{N}$, cross-multiplication equivalent at every ratio orbit $q$ to the native cost generated by the odd power $q \mapsto q^{2k+1}$.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator: the internal display of a rational. Two ratio orbits are identified by cross-equivalence when the scaled numerators balance as signed orbits (the PRC stand-in for ordinary rational equality).
The structural ledger without the anchor collects the base hypotheses minus two-calibration, plus sign-reversal, monotonicity, and zero-calibration of the doubled trace. Maps $F$ obeying that ledger form the anchor-free gauge orbit of native costs.
Odd-power generated native cost at index $k$ is the cost of $q \mapsto q^{2k+1}$. The case $k=0$ is the canonical cost; every $k \ge 1$ is a distinct gauge-orbit point. The present definition asks whether those odd powers exhaust the whole anchor-free ledger.
proof idea
No proof: this is a Prop definition. The body is the single quantified statement that every ledger map $F$ admits some $k$ such that $F$ and the odd-power cost at $k$ agree under cross-equivalence on all ratio orbits. Downstream work treats the name as a claim to refute or replace, not as a lemma to apply.
why it matters
This is the first proposed classification of the anchor-free gauge orbit. It is false: the zero-exponent sign member sits in the ledger and is not any odd-power cost, as shown by the dedicated refutation in Cost.GaugeOrbitFromRealCharacter. A first correction (sign or odd power) also fails; the proved replacement is the signed-power family, one inhabitant per nonnegative exponent with character $\mathrm{sgn}(x)\cdot|x|^c$, obtained from the six-exponentials input alone.
Locally it feeds the refutation that the anchor-free uniqueness target fails (the cube-generated cost at two is not canonical), which establishes that the anchor is a genuine unit gauge: structure alone does not force the canonical cost. In the Recognition forcing chain this sits under native-cost uniqueness and the J-cost story (T5), clarifying which residual freedom remains once the structural ledger is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.