no_native_golden_scale
plain-language theorem explainer
No rational orbit realizes the golden-ratio fixed-point equation $1+r^{-1}=r$. Cited by the native reciprocal-generator split (as the "scale is a purchase" clause) and by the structural stratification certificate. Proof is a one-line reduction to the ordinary rational no-golden-scale lemma.
Claim. There is no rational orbit $q$ whose positive rational value $r=q.{\mathrm{toRat}}$ satisfies the self-similar scale equation $1 + r^{-1} = r$.
background
In the primitive recognition calculus, a RatioOrbit is a rational display: signed-orbit numerator over a nonzero distinction-nat denominator, with toRat the induced positive or signed rational. The native cost ledger works only with such orbits and with the reciprocal automorphism on recognition events (swap source/target, invert the ratio).
The golden scale is the unique positive solution of $1+x^{-1}=x$, i.e. the self-similar fixed point $\varphi$ of the Recognition Composition Law / T6 forcing step. The module's structural ledger asks which cost facts are truly native (forced by reciprocal symmetry and orbit arithmetic) and which must be imported as an external purchase.
Upstream, the ordinary rational statement no_rat_golden_scale already rules out any positive rational root of that equation. The present theorem is the orbit-level carrier of the same fact.
proof idea
Term-mode one-liner. Unpack the existential witness $\langle q, h_q, h\rangle$ (orbit, positivity of toRat, and the fixed-point equation), then apply no_rat_golden_scale to the rational value. No new arithmetic is done at the orbit layer.
why it matters
This is the carrier half of the $\varphi$ split: everything the reciprocal generator says about cost is $\delta$-native; only the fixed point is bought. It discharges the field scale_is_a_purchase in nativeReciprocalGeneratorSplit_holds, which packages involutivity, cost symmetry, unit-cost-zero, and this non-existence. That split in turn feeds structuralStratificationCertificate_holds (uniqueness, slim contracts, positivity, gauge inhabited).
Framework landmark: T6 forces $\varphi$ as the self-similar fixed point of $J$; the present result says $\varphi$ is not a native rational orbit, so the ladder scale is an external purchase rather than an orbit identity. Downstream non-canonicity facts such as cubeGeneratedNativeCost_two_not_canonical sit in the same ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.