phiInv_mul_phi
plain-language theorem explainer
The product of the golden reciprocal and φ equals the ring unit in ℤ[φ]. Anyone building the unit group of the golden integers or the discrete φ-ladder cites this kernel identity. The proof is a one-line `decide` on the pair representation ⟨−1,1⟩·⟨0,1⟩.
Claim. In the golden integers $\mathbb{Z}[\varphi]$, with $\varphi^{-1}$ represented by the pair $\langle -1, 1\rangle$ (i.e. $\varphi-1$), one has $\varphi^{-1}\cdot\varphi = 1$.
background
CostUniqueness re-derives the T5 J-cost uniqueness node on the discrete carrier forced by T6: the φ-ladder inside GoldenInt = ℤ[φ]. Continuum pathologies that force Classical.choice on ℝ cannot appear once the domain is {φⁿ : n ∈ ℤ}.
Elements of ℤ[φ] are pairs ⟨a,b⟩ standing for a + bφ. The golden ratio satisfies φ² = φ + 1, so its multiplicative inverse is the exact ring element φ − 1, coded as phiInv = ⟨−1, 1⟩ — no field division. The companion identity φ · φ⁻¹ = 1 is the other kernel fact.
These two products equip φ with left and right inverses, so it becomes a unit of ℤ[φ]. Negative ladder rungs are then ordinary ring multiplications by powers of that unit, not inverses in a fraction field.
proof idea
One-line kernel computation. With phiInv = ⟨−1, 1⟩ and phi = ⟨0, 1⟩, the ring multiplication of GoldenInt is evaluated by decide, which checks the resulting pair equals the multiplicative identity ⟨1, 0⟩. No lemmas are invoked beyond the definitional arithmetic of the pair representation.
why it matters
Feeds directly into phiUnit, which packages φ as an element of GoldenIntˣ via the pair of products (φ · φ⁻¹ and φ⁻¹ · φ). That unit is the generator of phiZpow n = φⁿ for n ∈ ℤ, the discrete carrier on which the module runs the choice-free T5 argument: d'Alembert recurrence for traceZ, uniqueness by two-step induction, and the discrete RCL for Jdouble.
In the forcing chain this sits under T5 (J-uniqueness) and T6 (φ as self-similar fixed point). The identity is the multiplicative reading of φ² = φ + 1, exactly as the sibling doc-comment states for φ⁻¹ = φ − 1. Downstream, Algebra.PhiRing.PhiInt reuses the same pair model of ℤ[φ]. Without both inverse products the unit group and the negative ladder rungs do not exist inside the ring.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.