t6_bridge
plain-language theorem explainer
The unique positive golden root built inside ℤ[φ] evaluates under the real embedding to the classical golden ratio (1+√5)/2, is strictly positive, and satisfies φ² = φ+1 over ℝ. Anyone citing the T6 forcing step who needs the continuum presentation of φ uses this bridge. The proof is a three-conjunct refine through the already-proved evaluation and positivity lemmas of the embedding.
Claim. Under the ring evaluation $\mathbb{Z}[\varphi]\to\mathbb{R}$, the golden integer $\varphi$ maps to $(1+\sqrt{5})/2$, that image is strictly positive, and it satisfies $\varphi_{\mathbb{R}}^2=\varphi_{\mathbb{R}}+1$.
background
Recognition Science forces φ as the unique positive golden root (forcing-chain step T6) entirely inside the integer ring ℤ[φ], with axiom closure limited to propext and Quot.sound (the sigma0 layer). That algebraic object is GoldenInt.phi, characterized by the relation φ² = φ+1 and a decidable positivity predicate IsPos, without ever mentioning √5 or ℝ.
This module is the sigma1 display boundary: it pays the continuum tax once by defining the evaluation map toReal : GoldenInt → ℝ sending a+b·φ to a+b·φ_ℝ. The map is a ring embedding (additive, multiplicative via the golden relation, injective by irrationality descent). Sibling lemmas record the images of 0, 1, φ, and the conjugate, and prove that IsPos is exactly real positivity under toReal.
The classical continuum presentation of φ lives in PhiForcing as (1+√5)/2. The present theorem is the identification that the sigma0 root, once evaluated, is that classical number and still obeys the golden equation over ℝ.
proof idea
A single refine splits the conjunction into three goals.
- Equality with (1+√5)/2: rewrite by the sibling lemma toReal_phi (which unfolds the evaluation on the generator) and close by rfl against the classical definition.
- Strict positivity: apply the sibling equivalence isPos_iff_toReal_pos in the forward direction to the already-proved sigma0 fact that GoldenInt.phi is positive under IsPos.
- Golden equation over ℝ: rewrite the left-hand product via toReal_mul, replace the product in GoldenInt by GoldenInt.phi_sq, then push the sum and the unit across the embedding with toReal_add and toReal_one.
No new analysis is done; every step is transport along the embedding.
why it matters
T6 in the UnifiedForcingChain forces φ as the self-similar fixed point of the recognition cost. That forcing is completed at sigma0 inside ℤ[φ]. Downstream continuum arguments (PhiForcing, mass ladder, J-cost evaluations, alpha-band numerics) speak the classical language (1+√5)/2 and real order. This theorem is the single certified bridge between those two presentations: uniqueness, positivity, and the two roots were already proved algebraically; only the display into ℝ remains.
The module doc is explicit that derivation is delta-forced and only display costs Classical.choice (via Real.sqrt and real arithmetic). The theorem therefore lets any later development cite the classical golden ratio while retaining the sigma0 uniqueness pedigree. No used_by edges are recorded yet; the natural consumers are continuum T5/T6 display lemmas in the same file (trace and Jdouble matching 2·cosh and 2·Jcost) and any PhiForcing client that needs the identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.