phiInv_eq_phi_minus_one
The identity 1/φ = φ - 1 holds for the golden ratio φ. Researchers modeling decay rates, target ratios, and mixing angles across domains cite this result to unify negative-rung quantities. The proof is a short algebraic reduction that invokes φ² = φ + 1 to establish the product φ(φ - 1) = 1 and then rewrites the division definition.
claimLet φ denote the golden ratio. Then 1/φ = φ - 1.
background
The module establishes invariants for the quantity 1/φ across domains, with phiInv defined as the real number 1/φ. The upstream lemma phi_sq_eq states that φ² = φ + 1, the defining quadratic equation of the golden ratio. The local setting is the C22 structural claim that 1/φ ≈ 0.618 acts as the canonical attractor for decay rates, dampings, target ratios, and optimal share fractions in independent domains.
proof idea
The tactic proof first obtains φ ≠ 0 from positivity. It applies the upstream identity φ² = φ + 1 to derive φ(φ - 1) = 1 via nlinarith. After unfolding the definition of phiInv as 1/φ, it rewrites the target equality using eq_div_iff and closes with linarith.
why it matters in Recognition Science
This theorem supplies the fib_identity field to the downstream certificate phiInverseInvariantsCert that collects all 1/φ properties. It anchors the cross-domain convergence on 1/φ as the negative-rung value, consistent with the phi-ladder and the self-similar fixed point in the Recognition framework.
scope and limits
- Does not establish the numerical value or closed-form expression of φ itself.
- Does not extend the identity to complex numbers or other fields.
- Does not derive higher powers or additional invariants such as 1/φ².
- Does not connect directly to spatial dimensions or the forcing chain T0-T8.
Lean usage
example : phiInv = phi - 1 := phiInv_eq_phi_minus_oneformal statement (Lean)
50theorem phiInv_eq_phi_minus_one : phiInv = phi - 1 := by
proof body
Tactic-mode proof.
51 have hpos : phi ≠ 0 := ne_of_gt phi_pos
52 have h2 : phi^2 = phi + 1 := phi_sq_eq
53 have hkey : phi * (phi - 1) = 1 := by nlinarith [h2]
54 -- 1/φ = (φ-1) iff φ·(φ-1) = 1
55 unfold phiInv
56 rw [eq_comm, eq_div_iff hpos]
57 linarith [hkey]
58
59/-- 1/φ² = 2 - φ. Proof: φ²·(2-φ) = 2φ² - φ³ = 2(φ+1) - (2φ+1) = 1. -/