cubeGeneratedNativeCost
plain-language theorem explainer
The cube-generated native cost sends each rational orbit q to the native cost of q cubed, the first nontrivial odd-power gauge choice around the canonical J-cost. Uniqueness and gauge-orbit arguments cite it to separate structural ledger axioms from the unit-anchor choice. The body is a one-line specialization of the odd-power family at exponent three (k = 1).
Claim. Define the cube-generated native cost as the map on rational orbits given by the odd-power native cost at $k=1$: it is the cost induced by $q \mapsto q^{3}$. On the orbit of $2$ it charges $J(8)=49/16$, whereas the canonical cost charges $J(2)=1/4$.
background
In the Primitive Recognition Calculus structural ledger, native costs act on rational orbits: a signed integer numerator over a nonzero distinction-natural denominator. The canonical cost is the $k=0$ member of the odd-power family (the identity map on the ratio).
The odd-power generator builds a cost from $q \mapsto q^{2k+1}$. For $k=0$ one recovers the canonical cost; every $k \ge 1$ is a distinct point of the gauge orbit. The cube case is the first nontrivial member ($2\cdot 1+1=3$), so the cost evaluates $J(q^3)$ rather than $J(q)$.
On the orbit of $2$, the cube cost charges $J(8)=49/16$ while the canonical cost charges $J(2)=1/4$. That numerical gap is the explicit separation used later to refute anchor-free uniqueness.
proof idea
One-line definitional wrapper. Specialize the odd-power generated native cost at $k=1$, which itself is the power-generated native cost at exponent $2\cdot 1+1=3$. No proof obligations; the body is pure abbreviation of that family member.
why it matters
This definition is the concrete gauge alternative that shows the structural ledger without an anchor does not force the canonical cost. Downstream, the sans-anchor theorem records that the cube cost satisfies the anchor-free hypotheses; the rationalization theorem identifies its value with $J(q^3)$; and the two-not-canonical theorem proves it disagrees with the canonical cost on the orbit of two.
Those facts feed the refutation of the anchor-free uniqueness target, whose doc-comment states the punchline: the anchor is a genuine unit gauge; everything else in the ledger is structure, and the last field is a choice of unit. In the Recognition Science forcing chain this supports the T5 J-uniqueness story by isolating which axioms pin $J$ itself versus which only pin its gauge class under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.