phi_is_term
plain-language theorem explainer
The atomic F_RS term for the golden ratio evaluates exactly to ℝ's goldenRatio. Anyone assembling the countable RS carrier or citing the Phase 3 headline needs this inventory fact. The proof is pure reflexivity: the evaluator is defined to send the phi constructor to Real.goldenRatio.
Claim. Evaluating the atomic $F_{RS}$ expression for the golden ratio yields $\varphi = \frac{1+\sqrt{5}}{2}$ in $\mathbb{R}$.
background
The module builds an explicit finite-description carrier for Recognition Science constants. FRSExpr is an inductive syntax of finite terms over the rationals together with a fixed inventory (φ, π, e, α⁻¹), closed under negation, addition, multiplication, and inversion.
A recursive evaluator eval interprets each constructor into ℝ. By definition the phi leaf is sent to Mathlib's Real.goldenRatio. The surrounding development shows every such term lands in the countable minimal field rsField, so the framework never needs the full continuum as a computational carrier.
This sits inside Primitive Recognition Calculus: the carrier the framework actually computes on is finite generation over a fixed inventory, not uncountable ℝ.
proof idea
One-line reflexivity. The evaluator clause for the phi constructor is definitionally Real.goldenRatio, so rfl closes the equality.
why it matters
Feeds the Phase 3 headline frs_carrier, which packages soundness (every term lands in rsField), the four inventory identities (φ, π, e, α⁻¹), countability, proper-subset status, and protocol display in the ℝδ interface. Downstream quotes: "the constant inventory (φ, π, e, α⁻¹) and the rationals are terms" and "the carrier the framework actually computes on is finite generation over a fixed inventory, not the uncountable continuum."
In the broader RS chain, φ is the self-similar fixed point forced at T6 and the base of the mass ladder and the native units (ħ = φ⁻⁵, G = φ⁵/π). Pinning the syntax leaf to Mathlib's golden ratio makes that identification machine-checkable rather than notational.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.