cubeGeneratedNativeCost_toRat
plain-language theorem explainer
The cube-generated native cost of a rational orbit, displayed as a verifier rational, equals the J-cost of the cube of that orbit's rational value. Ledger auditors comparing power-generated costs to the canonical J display cite this identity. The proof is a one-line specialization of the odd-power transport theorem at index one (exponent three).
Claim. For every rational orbit $q$, the verifier-rational image of the cube-generated native cost of $q$ equals $J(r^3)$, where $r$ is the rational value of $q$ and $J(t)=(t+t^{-1})/2-1$.
background
Ratio orbits are the PRC display of rationals: a signed integer-orbit numerator over a nonzero distinction-natural denominator. The verifier map sends such an orbit to an ordinary rational by integer division (spec tag A5: transport wrapper, internal law by cross-multiplication).
The J-display on rationals is $J(t)=(t+t^{-1})/2-1$, the unique cost forced by the Recognition Composition Law. Power-generated native costs evaluate $J$ after raising the orbit to a positive integer power. Odd-power generators use exponents $2k+1$; the cube case is the first nontrivial member, defined as the odd-power generator at index $k=1$.
The upstream odd-power transport theorem states that the verifier image of the $k$-th odd-power-generated cost equals $J$ of the orbit value raised to $2k+1$.
proof idea
One-line wrapper that applies the odd-power transport identity at $k=1$. That identity already reduces to the general power-generated transport at exponent $2k+1$; substituting $k=1$ gives exponent $3$, which is exactly the cube case.
why it matters
Names the cube ledger entry against the canonical J display. Per its definition, the cube cost is the first nontrivial power-generated member: on the orbit of $2$ it charges $J(8)=49/16$, while the canonical cost charges only $J(2)=1/4$. That strict gap is structural evidence that power-generated costs sit above the minimal native cost except at the identity power.
The comparison is meaningful only because T5 forces J-uniqueness via the Recognition Composition Law. The module imports the native-cost minimality certificate, so this specialization is the named cube case those audits can quote. No downstream consumers are recorded yet; the lemma stands ready for ledger comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.