no_rat_golden_scale
plain-language theorem explainer
No positive rational satisfies the golden fixed-point equation $1 + t^{-1} = t$. Anyone ruling out a rational self-similar scale (the $\varphi$ root of $x^2-x-1$) cites this. The proof clears denominators to $a^2=a+1$ in lowest terms, forces denominator $1$, then checks the two remaining positive integers by hand.
Claim. For every positive rational $t>0$, one has $1 + t^{-1} \neq t$. Equivalently, the quadratic $x^2 - x - 1 = 0$ has no positive rational root.
background
In Recognition Science the self-similar scale is the unique positive fixed point of $x \mapsto 1 + x^{-1}$, i.e. the golden ratio $\varphi$ solving $x^2 = x + 1$. Forcing step T6 identifies $\varphi$ as that fixed point. A $\delta$-native (rational) carrier would mean some positive rational already sits at that scale.
This lemma works entirely inside $\mathbb{Q}_{>0}$. It is the arithmetic engine under the carrier statement that no ratio-orbit realizes the golden scale. The module builds a structural ledger for primitive recognition cost; the present fact is the elementary number-theoretic obstruction before one lifts from rationals to orbits.
Upstream scaffolding only supplies positivity and coprimality language (reduced fraction data, gcd). No cost functional or continuum limit is used here.
proof idea
Assume $1 + t^{-1} = t$ with $t>0$. Field simplification yields $t^2 = t + 1$. Write $t = a/b$ in lowest terms ($a = t.\mathrm{num}$, $b = t.\mathrm{den}$). Clearing denominators produces the integer identity $a^2 = a b + b^2$, so $b \mid a^2$. Coprimality of $b$ with $a$ (hence with $a^2$) forces $b = 1$. The equation collapses to $a^2 = a + 1$ with $a > 0$. The bound $a \le 2$ (from $a^2 - a - 1 = 0$ and nonnegativity of $(a-1)^2$) leaves only $a \in {1,2}$, both of which fail by direct arithmetic.
why it matters
Feeds the carrier theorem no_native_golden_scale: no ratio-orbit $q$ satisfies $0 < q.\mathrm{toRat}$ and $1 + (q.\mathrm{toRat})^{-1} = q.\mathrm{toRat}$. That carrier is the discrete half of the $\varphi$ split in the primitive recognition calculus: the self-similar scale is forced off the rational lattice.
In the forcing chain this is the elementary witness that T6's fixed point $\varphi$ is irrational, so the native cost ledger cannot place a golden rung on a rational orbit. Downstream cost and mass formulae that sit on the $\varphi$-ladder therefore inherit an irrational yardstick rather than a rational one. The argument is choice-free and uses only reduced-fraction arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.