phiL
plain-language theorem explainer
Defines the golden ratio on the recovered real line as (1 + √5)/2, transported via fromReal and sqrtL. Downstream RS constants (ħ, J-bit) and numerical φ bounds cite it as the LogicReal stand-in for the self-similar fixed point. The body is a direct algebraic definition, not a proof.
Claim. Let $\varphi_L$ be the element of the recovered real line given by $\varphi_L = \bigl(1 + \sqrt{5}\bigr)/2$, where integers are embedded by the canonical transport from $\mathbb{R}$ and the square root is the transported real square root.
background
LogicRealConstants places Recognition Science constants on LogicReal, the Cauchy completion of the recovered rationals (via the LogicRat ≃ ℚ equivalence and Bourbaki completion). Each constant is written in LogicReal; companion theorems show that LogicReal.toReal recovers the ordinary real from IndisputableMonolith.Constants.
fromReal embeds a Mathlib real into LogicReal. sqrtL is square root on recovered reals, defined by transporting Real.sqrt through toReal/fromReal. The classical golden ratio $\varphi = (1+\sqrt{5})/2$ is the unique positive solution of $x = 1 + 1/x$, and in the forcing chain it is the self-similar fixed point (T6).
This definition is the LogicReal mirror of that constant, so later identities such as $\hbar = \varphi^{-5}$ can be stated entirely inside the recovered line.
proof idea
Not a proof: a three-token definition. Embed 1 and 5 via fromReal, take sqrtL of the image of 5, add, and divide by the image of 2. No lemmas are applied; equality with the classical φ is deferred to toReal_phiL and the numerical bound theorems.
why it matters
φ is the scaling base of the RS ladder (T6) and appears in the native units $\hbar = \varphi^{-5}$, $G = \varphi^5/\pi$. On the recovered line this definition feeds hbarL := rpowL phiL (fromReal (-5)), JbitL := logL phiL, and the positivity/bound lemmas phiL_pos, phiL_gt_one, phiL_gt_onePointFive, phiL_lt_onePointSixTwo, plus the transport identity toReal_phiL.
Without a LogicReal φ, the module cannot state the RS-native constants or prove they match Constants after toReal. It is scaffolding for the constant tower, not a forcing step itself; uniqueness of φ still lives in the T5–T6 chain on ordinary reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.