From 33ab3bbc3e920b20cf267cbf638e8e4f2b946110 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 23 May 2026 05:24:17 +0000 Subject: [PATCH 1/4] feat(Mathematics): add public import for Physlib.Mathematics.GoldenRatio --- Physlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Physlib.lean b/Physlib.lean index 7fbdd8b9a..eba62b283 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -62,6 +62,7 @@ public import Physlib.Mathematics.Fin public import Physlib.Mathematics.Fin.Involutions public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs public import Physlib.Mathematics.Geometry.Metric.Riemannian.Defs +public import Physlib.Mathematics.GoldenRatio public import Physlib.Mathematics.InnerProductSpace.Adjoint public import Physlib.Mathematics.InnerProductSpace.Basic public import Physlib.Mathematics.InnerProductSpace.Calculus From c2919f1a4f88a7e5a891ea5e3a7e77010ff253b7 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 23 May 2026 05:24:47 +0000 Subject: [PATCH 2/4] feat(Mathematics): add Physlib/Mathematics/GoldenRatio.lean Adds a thin Physlib-namespace wrapper around mathlib's Mathlib.NumberTheory.Real.GoldenRatio plus physics-flavoured derived identities that mathlib does not state. 33 declarations (31 theorems + 2 abbrevs), 0 sorry, 0 axiom. Contributed by gHashTag/trinity-s3ai Wave 7, W7.3. https://github.com/gHashTag/trinity-s3ai --- Physlib/Mathematics/GoldenRatio.lean | 226 +++++++++++++++++++++++++++ 1 file changed, 226 insertions(+) create mode 100644 Physlib/Mathematics/GoldenRatio.lean diff --git a/Physlib/Mathematics/GoldenRatio.lean b/Physlib/Mathematics/GoldenRatio.lean new file mode 100644 index 000000000..b6e60f649 --- /dev/null +++ b/Physlib/Mathematics/GoldenRatio.lean @@ -0,0 +1,226 @@ +/- +Copyright (c) 2026 Trinity-S3AI contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Trinity-S3AI contributors +-/ +module + +public import Mathlib.NumberTheory.Real.GoldenRatio +public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic +public import Mathlib.Tactic +/-! + +# The golden ratio for physics + +The constant `φ = (1 + √5) / 2` and its algebraic conjugate `ψ = (1 - √5) / 2` +appear throughout physics: in the quasicrystal literature (Penrose tilings, +icosahedral symmetry of viral capsids and metallic alloys), in the H₄ root +system underlying the 600-cell and the binary icosahedral group `2I ⊂ SU(2)`, +in continuous-spectrum analyses where the irrational rotation number `1/φ` +plays the role of "most irrational" frequency, and in coupling-constant +relations of the icosian Coxeter program. + +The bulk of the basic algebra is already in mathlib (`Mathlib.NumberTheory. +Real.GoldenRatio` defines `Real.goldenRatio`, `Real.goldenConj`, the `φ` +and `ψ` notations and proves the golden equation, positivity, irrationality +and Binet's formula). This module re-exports that API into the `Physlib` +namespace and adds the physics-flavoured derived identities that mathlib +does not state: + +* `phi`, `psi` — `Physlib`-level shortcuts. +* `phi_continued_fraction` — the fixed-point identity `φ = 1 + 1/φ`, the + entry point to the continued-fraction description used in KAM theory. +* `phi_inv_pos`, `phi_inv_lt_one` — explicit positivity of `1/φ`. +* `phi_two_cos_pi_div_five` — the icosian identity `φ = 2 cos(π/5)`, + the bridge between the algebraic and the H₄/geometric descriptions. +* `phi_quadratic` and `psi_quadratic` — both roots of `X² - X - 1 = 0` + in a form ready for substitution arguments. +* `phi_lower_bound`, `phi_upper_bound` — explicit numerical envelopes. +* `phi_pow_three`, `phi_pow_four`, `phi_pow_five` — closed forms with + Fibonacci-coefficient pattern. + +All proofs are by `Qed` (no `sorry`, no `axiom`). +-/ + +@[expose] public section + +namespace Physlib + +open Real goldenRatio + +/-! ## Section 1: `Physlib`-level shortcuts -/ + +/-- The golden ratio `φ := (1 + √5) / 2`. Re-export of `Real.goldenRatio`. -/ +abbrev phi : ℝ := Real.goldenRatio + +/-- The conjugate of the golden ratio `ψ := (1 - √5) / 2`. +Re-export of `Real.goldenConj`. -/ +abbrev psi : ℝ := Real.goldenConj + +theorem phi_eq_goldenRatio : phi = φ := rfl + +theorem psi_eq_goldenConj : psi = ψ := rfl + +/-! ## Section 2: Re-export of the mathlib basic identities + +These re-statements simply repackage the mathlib lemmas under the `Physlib` +namespace so downstream Physlib files do not have to know the mathlib path. +The mathlib originals are: `Real.goldenRatio_sq`, `Real.goldenRatio_pos`, +`Real.one_lt_goldenRatio`, `Real.goldenRatio_lt_two`, +`Real.goldenRatio_mul_goldenConj`, `Real.goldenRatio_add_goldenConj`, +`Real.inv_goldenRatio`. -/ + +theorem phi_sq : phi ^ 2 = phi + 1 := Real.goldenRatio_sq + +theorem phi_pos : 0 < phi := Real.goldenRatio_pos + +theorem phi_ne_zero : phi ≠ 0 := Real.goldenRatio_ne_zero + +theorem one_lt_phi : 1 < phi := Real.one_lt_goldenRatio + +theorem phi_lt_two : phi < 2 := Real.goldenRatio_lt_two + +theorem psi_neg : psi < 0 := Real.goldenConj_neg + +theorem psi_ne_zero : psi ≠ 0 := Real.goldenConj_ne_zero + +theorem phi_psi_sum : phi + psi = 1 := Real.goldenRatio_add_goldenConj + +theorem phi_psi_prod : phi * psi = -1 := Real.goldenRatio_mul_goldenConj + +theorem phi_inv_eq_neg_psi : phi⁻¹ = -psi := Real.inv_goldenRatio + +theorem psi_inv_eq_neg_phi : psi⁻¹ = -phi := Real.inv_goldenConj + +theorem psi_sq : psi ^ 2 = psi + 1 := Real.goldenConj_sq + +/-! ## Section 3: Derived physics-flavoured identities + +These results are not in mathlib but are useful for physical applications. +They connect φ to its continued-fraction description, to the 5-fold +symmetry of the icosian Coxeter group, and to explicit positivity bounds. -/ + +/-- `1/φ > 0`. -/ +theorem phi_inv_pos : 0 < phi⁻¹ := + inv_pos.mpr phi_pos + +/-- `1/φ < 1`. -/ +theorem phi_inv_lt_one : phi⁻¹ < 1 := + inv_lt_one_of_one_lt₀ one_lt_phi + +/-- `1/φ ≠ 0`. -/ +theorem phi_inv_ne_zero : phi⁻¹ ≠ 0 := + inv_ne_zero phi_ne_zero + +/-- The fixed-point identity `φ = 1 + 1/φ` — the key relation behind the +continued-fraction expansion `φ = [1; 1, 1, ...]`. + +Proof: combine `φ + ψ = 1` (Viète) with `1/φ = -ψ` to get +`1 + 1/φ = 1 - ψ = φ`. -/ +theorem phi_continued_fraction : phi = 1 + phi⁻¹ := by + rw [phi_inv_eq_neg_psi] + have : phi + psi = 1 := phi_psi_sum + linarith + +/-- Equivalent form of the fixed-point identity: `φ - 1 = 1/φ`. -/ +theorem phi_sub_one_eq_inv : phi - 1 = phi⁻¹ := by + have := phi_continued_fraction; linarith + +/-- The icosian / Coxeter identity `φ = 2 cos(π / 5)`. This is the bridge +between the algebraic description of φ and the geometric description through +the 5-fold rotational symmetry of the regular pentagon (H₂ Coxeter group) +and, by extension, of the 600-cell and the binary icosahedral group `2I`. + +Proof: `cos(π/5) = (1 + √5)/4` (mathlib's `Real.cos_pi_div_five`); doubling +gives `2 cos(π/5) = (1 + √5)/2 = φ`. -/ +theorem phi_two_cos_pi_div_five : phi = 2 * Real.cos (Real.pi / 5) := by + rw [Real.cos_pi_div_five] + show Real.goldenRatio = 2 * ((1 + Real.sqrt 5) / 4) + unfold Real.goldenRatio + ring + +/-- φ is a root of the quadratic `X² - X - 1`. -/ +theorem phi_quadratic : phi ^ 2 - phi - 1 = 0 := by + have := phi_sq; linarith + +/-- ψ is a root of the quadratic `X² - X - 1`. -/ +theorem psi_quadratic : psi ^ 2 - psi - 1 = 0 := by + have := psi_sq; linarith + +/-- Both roots of `X² - X - 1 = 0` satisfy the Viète relations. -/ +theorem phi_psi_vieta : + phi + psi = 1 ∧ phi * psi = -1 := + ⟨phi_psi_sum, phi_psi_prod⟩ + +/-! ## Section 4: Explicit numerical bounds + +Useful for interval arithmetic and physical estimation. -/ + +/-- Lower bound: `1.6 < φ`. -/ +theorem phi_lower_bound : (1.6 : ℝ) < phi := by + have h₁ : (2.2 : ℝ) < Real.sqrt 5 := by + have heq : (2.2 : ℝ) = Real.sqrt (2.2 ^ 2) := by + rw [Real.sqrt_sq] <;> norm_num + rw [heq] + exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num) + show (1.6 : ℝ) < (1 + Real.sqrt 5) / 2 + linarith + +/-- Upper bound: `φ < 1.7`. -/ +theorem phi_upper_bound : phi < (1.7 : ℝ) := by + have h₁ : Real.sqrt 5 < (2.4 : ℝ) := by + have heq : (2.4 : ℝ) = Real.sqrt (2.4 ^ 2) := by + rw [Real.sqrt_sq] <;> norm_num + rw [heq] + exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num) + show (1 + Real.sqrt 5) / 2 < (1.7 : ℝ) + linarith + +/-- Joint numerical envelope: `1.6 < φ < 1.7`. -/ +theorem phi_bounds : (1.6 : ℝ) < phi ∧ phi < (1.7 : ℝ) := + ⟨phi_lower_bound, phi_upper_bound⟩ + +/-! ## Section 5: Powers of φ + +Closed forms for low integer powers of φ obtained by iterating the golden +equation `φ² = φ + 1`. The coefficients are Fibonacci numbers, reflecting +Binet's formula. + +The mathlib lemma `Real.goldenRatio_pow_sub_goldenRatio_pow` states +`φ^(n+2) - φ^(n+1) = φ^n`, i.e. `φ^(n+2) = φ^(n+1) + φ^n`. -/ + +/-- `φ ^ 3 = 2 φ + 1`. -/ +theorem phi_pow_three : phi ^ 3 = 2 * phi + 1 := by + have h := phi_sq + have : phi ^ 3 = phi * phi ^ 2 := by ring + rw [this, h]; ring + +/-- `φ ^ 4 = 3 φ + 2`. -/ +theorem phi_pow_four : phi ^ 4 = 3 * phi + 2 := by + have h := phi_sq + have h3 := phi_pow_three + have : phi ^ 4 = phi * phi ^ 3 := by ring + rw [this, h3] + have : phi * (2 * phi + 1) = 2 * phi ^ 2 + phi := by ring + rw [this, h]; ring + +/-- `φ ^ 5 = 5 φ + 3`. The general Fibonacci-coefficient pattern: +`φ ^ n = F_n · φ + F_{n-1}`, where `F_n` is the n-th Fibonacci number. -/ +theorem phi_pow_five : phi ^ 5 = 5 * phi + 3 := by + have h := phi_sq + have h4 := phi_pow_four + have : phi ^ 5 = phi * phi ^ 4 := by ring + rw [this, h4] + have : phi * (3 * phi + 2) = 3 * phi ^ 2 + 2 * phi := by ring + rw [this, h]; ring + +/-! ## Section 6: Irrationality (re-export) + +`φ` and `ψ` are irrational; this is `Real.goldenRatio_irrational` and +`Real.goldenConj_irrational` in mathlib. -/ + +theorem phi_irrational : Irrational phi := Real.goldenRatio_irrational + +theorem psi_irrational : Irrational psi := Real.goldenConj_irrational + +end Physlib \ No newline at end of file From 71c3e7599b0005885951dd64d0db3d7a3aa4b756 Mon Sep 17 00:00:00 2001 From: gHashTag Date: Thu, 18 Jun 2026 14:10:57 +0000 Subject: [PATCH 3/4] review: drop phi/psi abbrevs, build API directly on Real.goldenRatio Per reviewer guidance (@zhikaip): do not introduce new phi/psi names that could collide with phi-as-phase / phi-as-potential elsewhere in physics. - Remove abbrev phi/psi and the thin re-export lemmas that only wrapped mathlib (goldenRatio_sq, _pos, _add_goldenConj, etc.). - Use mathlib's own scoped notation phi/psi via 'open scoped goldenRatio' (scoped[goldenRatio], file-local, not exported globally). - Move the module into namespace Physlib.GoldenRatio. - Keep only the lemmas not in mathlib: continued-fraction fixed point, phi = 2 cos(pi/5) (icosian/H4 bridge), pow_three/four/five closed forms, and explicit numerical bounds. Proofs unchanged apart from renaming. --- Physlib/Mathematics/GoldenRatio.lean | 214 ++++++++++----------------- 1 file changed, 81 insertions(+), 133 deletions(-) diff --git a/Physlib/Mathematics/GoldenRatio.lean b/Physlib/Mathematics/GoldenRatio.lean index b6e60f649..0363979c4 100644 --- a/Physlib/Mathematics/GoldenRatio.lean +++ b/Physlib/Mathematics/GoldenRatio.lean @@ -10,154 +10,111 @@ public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic public import Mathlib.Tactic /-! -# The golden ratio for physics - -The constant `φ = (1 + √5) / 2` and its algebraic conjugate `ψ = (1 - √5) / 2` -appear throughout physics: in the quasicrystal literature (Penrose tilings, -icosahedral symmetry of viral capsids and metallic alloys), in the H₄ root -system underlying the 600-cell and the binary icosahedral group `2I ⊂ SU(2)`, -in continuous-spectrum analyses where the irrational rotation number `1/φ` -plays the role of "most irrational" frequency, and in coupling-constant -relations of the icosian Coxeter program. - -The bulk of the basic algebra is already in mathlib (`Mathlib.NumberTheory. -Real.GoldenRatio` defines `Real.goldenRatio`, `Real.goldenConj`, the `φ` -and `ψ` notations and proves the golden equation, positivity, irrationality -and Binet's formula). This module re-exports that API into the `Physlib` -namespace and adds the physics-flavoured derived identities that mathlib -does not state: - -* `phi`, `psi` — `Physlib`-level shortcuts. -* `phi_continued_fraction` — the fixed-point identity `φ = 1 + 1/φ`, the - entry point to the continued-fraction description used in KAM theory. -* `phi_inv_pos`, `phi_inv_lt_one` — explicit positivity of `1/φ`. -* `phi_two_cos_pi_div_five` — the icosian identity `φ = 2 cos(π/5)`, - the bridge between the algebraic and the H₄/geometric descriptions. -* `phi_quadratic` and `psi_quadratic` — both roots of `X² - X - 1 = 0` - in a form ready for substitution arguments. -* `phi_lower_bound`, `phi_upper_bound` — explicit numerical envelopes. -* `phi_pow_three`, `phi_pow_four`, `phi_pow_five` — closed forms with - Fibonacci-coefficient pattern. - -All proofs are by `Qed` (no `sorry`, no `axiom`). +# Golden-ratio identities for physics + +This module collects the few derived identities about the golden ratio +`φ = (1 + √5) / 2` and its conjugate `ψ = (1 - √5) / 2` that are useful in +physical applications but are not (yet) stated in mathlib. + +The basic algebra already lives in `Mathlib.NumberTheory.Real.GoldenRatio`, +which defines `Real.goldenRatio`, `Real.goldenConj` and the `scoped[goldenRatio]` +notations `φ`, `ψ`, and proves the golden equation, the Viète relations, +positivity, irrationality and Binet's formula. Per reviewer guidance, this +module does **not** introduce any new `phi`/`psi` names: it works directly on +`Real.goldenRatio` / `Real.goldenConj` and uses mathlib's own `φ` / `ψ` +notation, made available file-locally via `open scoped goldenRatio` (so the +single-letter `φ` is never exported globally and does not collide with `φ` +used elsewhere in physics as a phase or a potential). + +What this module adds on top of mathlib: + +* `goldenRatio_continued_fraction` — the fixed-point identity `φ = 1 + 1/φ`, + the entry point to the continued-fraction expansion `φ = [1; 1, 1, …]` used + in KAM theory and the "most irrational" rotation number. +* `goldenRatio_two_cos_pi_div_five` — the icosian identity `φ = 2 cos(π/5)`, + the bridge from the algebraic golden ratio to the 5-fold symmetry of the + pentagon (H₂), the 600-cell and the binary icosahedral group `2I ⊂ SU(2)`. +* `goldenRatio_inv_pos`, `goldenRatio_inv_lt_one` — explicit bounds on `1/φ`. +* `goldenRatio_quadratic`, `goldenConj_quadratic` — both roots of + `X² - X - 1 = 0` in a form ready for substitution arguments. +* `goldenRatio_lower_bound`, `goldenRatio_upper_bound` — numerical envelopes. +* `goldenRatio_pow_three`, `_four`, `_five` — closed forms with the + Fibonacci-coefficient pattern `φ^n = F_n · φ + F_{n-1}`. + +All proofs are complete (no `sorry`, no `axiom`). -/ @[expose] public section -namespace Physlib +namespace Physlib.GoldenRatio -open Real goldenRatio +open Real +open scoped goldenRatio -/-! ## Section 1: `Physlib`-level shortcuts -/ - -/-- The golden ratio `φ := (1 + √5) / 2`. Re-export of `Real.goldenRatio`. -/ -abbrev phi : ℝ := Real.goldenRatio - -/-- The conjugate of the golden ratio `ψ := (1 - √5) / 2`. -Re-export of `Real.goldenConj`. -/ -abbrev psi : ℝ := Real.goldenConj - -theorem phi_eq_goldenRatio : phi = φ := rfl - -theorem psi_eq_goldenConj : psi = ψ := rfl - -/-! ## Section 2: Re-export of the mathlib basic identities - -These re-statements simply repackage the mathlib lemmas under the `Physlib` -namespace so downstream Physlib files do not have to know the mathlib path. -The mathlib originals are: `Real.goldenRatio_sq`, `Real.goldenRatio_pos`, -`Real.one_lt_goldenRatio`, `Real.goldenRatio_lt_two`, -`Real.goldenRatio_mul_goldenConj`, `Real.goldenRatio_add_goldenConj`, -`Real.inv_goldenRatio`. -/ - -theorem phi_sq : phi ^ 2 = phi + 1 := Real.goldenRatio_sq - -theorem phi_pos : 0 < phi := Real.goldenRatio_pos - -theorem phi_ne_zero : phi ≠ 0 := Real.goldenRatio_ne_zero - -theorem one_lt_phi : 1 < phi := Real.one_lt_goldenRatio - -theorem phi_lt_two : phi < 2 := Real.goldenRatio_lt_two - -theorem psi_neg : psi < 0 := Real.goldenConj_neg - -theorem psi_ne_zero : psi ≠ 0 := Real.goldenConj_ne_zero - -theorem phi_psi_sum : phi + psi = 1 := Real.goldenRatio_add_goldenConj - -theorem phi_psi_prod : phi * psi = -1 := Real.goldenRatio_mul_goldenConj - -theorem phi_inv_eq_neg_psi : phi⁻¹ = -psi := Real.inv_goldenRatio - -theorem psi_inv_eq_neg_phi : psi⁻¹ = -phi := Real.inv_goldenConj - -theorem psi_sq : psi ^ 2 = psi + 1 := Real.goldenConj_sq - -/-! ## Section 3: Derived physics-flavoured identities +/-! ## Section 1: Derived physics-flavoured identities These results are not in mathlib but are useful for physical applications. -They connect φ to its continued-fraction description, to the 5-fold +They connect `φ` to its continued-fraction description, to the 5-fold symmetry of the icosian Coxeter group, and to explicit positivity bounds. -/ /-- `1/φ > 0`. -/ -theorem phi_inv_pos : 0 < phi⁻¹ := - inv_pos.mpr phi_pos +theorem goldenRatio_inv_pos : 0 < φ⁻¹ := + inv_pos.mpr goldenRatio_pos /-- `1/φ < 1`. -/ -theorem phi_inv_lt_one : phi⁻¹ < 1 := - inv_lt_one_of_one_lt₀ one_lt_phi +theorem goldenRatio_inv_lt_one : φ⁻¹ < 1 := + inv_lt_one_of_one_lt₀ one_lt_goldenRatio /-- `1/φ ≠ 0`. -/ -theorem phi_inv_ne_zero : phi⁻¹ ≠ 0 := - inv_ne_zero phi_ne_zero +theorem goldenRatio_inv_ne_zero : φ⁻¹ ≠ 0 := + inv_ne_zero goldenRatio_ne_zero /-- The fixed-point identity `φ = 1 + 1/φ` — the key relation behind the -continued-fraction expansion `φ = [1; 1, 1, ...]`. +continued-fraction expansion `φ = [1; 1, 1, …]`. Proof: combine `φ + ψ = 1` (Viète) with `1/φ = -ψ` to get `1 + 1/φ = 1 - ψ = φ`. -/ -theorem phi_continued_fraction : phi = 1 + phi⁻¹ := by - rw [phi_inv_eq_neg_psi] - have : phi + psi = 1 := phi_psi_sum +theorem goldenRatio_continued_fraction : φ = 1 + φ⁻¹ := by + rw [inv_goldenRatio] + have : φ + ψ = 1 := goldenRatio_add_goldenConj linarith /-- Equivalent form of the fixed-point identity: `φ - 1 = 1/φ`. -/ -theorem phi_sub_one_eq_inv : phi - 1 = phi⁻¹ := by - have := phi_continued_fraction; linarith +theorem goldenRatio_sub_one_eq_inv : φ - 1 = φ⁻¹ := by + have := goldenRatio_continued_fraction; linarith /-- The icosian / Coxeter identity `φ = 2 cos(π / 5)`. This is the bridge -between the algebraic description of φ and the geometric description through +between the algebraic description of `φ` and the geometric description through the 5-fold rotational symmetry of the regular pentagon (H₂ Coxeter group) and, by extension, of the 600-cell and the binary icosahedral group `2I`. Proof: `cos(π/5) = (1 + √5)/4` (mathlib's `Real.cos_pi_div_five`); doubling gives `2 cos(π/5) = (1 + √5)/2 = φ`. -/ -theorem phi_two_cos_pi_div_five : phi = 2 * Real.cos (Real.pi / 5) := by +theorem goldenRatio_two_cos_pi_div_five : φ = 2 * Real.cos (Real.pi / 5) := by rw [Real.cos_pi_div_five] show Real.goldenRatio = 2 * ((1 + Real.sqrt 5) / 4) unfold Real.goldenRatio ring -/-- φ is a root of the quadratic `X² - X - 1`. -/ -theorem phi_quadratic : phi ^ 2 - phi - 1 = 0 := by - have := phi_sq; linarith +/-- `φ` is a root of the quadratic `X² - X - 1`. -/ +theorem goldenRatio_quadratic : φ ^ 2 - φ - 1 = 0 := by + have := goldenRatio_sq; linarith -/-- ψ is a root of the quadratic `X² - X - 1`. -/ -theorem psi_quadratic : psi ^ 2 - psi - 1 = 0 := by - have := psi_sq; linarith +/-- `ψ` is a root of the quadratic `X² - X - 1`. -/ +theorem goldenConj_quadratic : ψ ^ 2 - ψ - 1 = 0 := by + have := goldenConj_sq; linarith /-- Both roots of `X² - X - 1 = 0` satisfy the Viète relations. -/ -theorem phi_psi_vieta : - phi + psi = 1 ∧ phi * psi = -1 := - ⟨phi_psi_sum, phi_psi_prod⟩ +theorem goldenRatio_goldenConj_vieta : + φ + ψ = 1 ∧ φ * ψ = -1 := + ⟨goldenRatio_add_goldenConj, goldenRatio_mul_goldenConj⟩ -/-! ## Section 4: Explicit numerical bounds +/-! ## Section 2: Explicit numerical bounds Useful for interval arithmetic and physical estimation. -/ /-- Lower bound: `1.6 < φ`. -/ -theorem phi_lower_bound : (1.6 : ℝ) < phi := by +theorem goldenRatio_lower_bound : (1.6 : ℝ) < φ := by have h₁ : (2.2 : ℝ) < Real.sqrt 5 := by have heq : (2.2 : ℝ) = Real.sqrt (2.2 ^ 2) := by rw [Real.sqrt_sq] <;> norm_num @@ -167,7 +124,7 @@ theorem phi_lower_bound : (1.6 : ℝ) < phi := by linarith /-- Upper bound: `φ < 1.7`. -/ -theorem phi_upper_bound : phi < (1.7 : ℝ) := by +theorem goldenRatio_upper_bound : φ < (1.7 : ℝ) := by have h₁ : Real.sqrt 5 < (2.4 : ℝ) := by have heq : (2.4 : ℝ) = Real.sqrt (2.4 ^ 2) := by rw [Real.sqrt_sq] <;> norm_num @@ -177,12 +134,12 @@ theorem phi_upper_bound : phi < (1.7 : ℝ) := by linarith /-- Joint numerical envelope: `1.6 < φ < 1.7`. -/ -theorem phi_bounds : (1.6 : ℝ) < phi ∧ phi < (1.7 : ℝ) := - ⟨phi_lower_bound, phi_upper_bound⟩ +theorem goldenRatio_bounds : (1.6 : ℝ) < φ ∧ φ < (1.7 : ℝ) := + ⟨goldenRatio_lower_bound, goldenRatio_upper_bound⟩ -/-! ## Section 5: Powers of φ +/-! ## Section 3: Powers of `φ` -Closed forms for low integer powers of φ obtained by iterating the golden +Closed forms for low integer powers of `φ` obtained by iterating the golden equation `φ² = φ + 1`. The coefficients are Fibonacci numbers, reflecting Binet's formula. @@ -190,37 +147,28 @@ The mathlib lemma `Real.goldenRatio_pow_sub_goldenRatio_pow` states `φ^(n+2) - φ^(n+1) = φ^n`, i.e. `φ^(n+2) = φ^(n+1) + φ^n`. -/ /-- `φ ^ 3 = 2 φ + 1`. -/ -theorem phi_pow_three : phi ^ 3 = 2 * phi + 1 := by - have h := phi_sq - have : phi ^ 3 = phi * phi ^ 2 := by ring +theorem goldenRatio_pow_three : φ ^ 3 = 2 * φ + 1 := by + have h := goldenRatio_sq + have : φ ^ 3 = φ * φ ^ 2 := by ring rw [this, h]; ring /-- `φ ^ 4 = 3 φ + 2`. -/ -theorem phi_pow_four : phi ^ 4 = 3 * phi + 2 := by - have h := phi_sq - have h3 := phi_pow_three - have : phi ^ 4 = phi * phi ^ 3 := by ring +theorem goldenRatio_pow_four : φ ^ 4 = 3 * φ + 2 := by + have h := goldenRatio_sq + have h3 := goldenRatio_pow_three + have : φ ^ 4 = φ * φ ^ 3 := by ring rw [this, h3] - have : phi * (2 * phi + 1) = 2 * phi ^ 2 + phi := by ring + have : φ * (2 * φ + 1) = 2 * φ ^ 2 + φ := by ring rw [this, h]; ring /-- `φ ^ 5 = 5 φ + 3`. The general Fibonacci-coefficient pattern: `φ ^ n = F_n · φ + F_{n-1}`, where `F_n` is the n-th Fibonacci number. -/ -theorem phi_pow_five : phi ^ 5 = 5 * phi + 3 := by - have h := phi_sq - have h4 := phi_pow_four - have : phi ^ 5 = phi * phi ^ 4 := by ring +theorem goldenRatio_pow_five : φ ^ 5 = 5 * φ + 3 := by + have h := goldenRatio_sq + have h4 := goldenRatio_pow_four + have : φ ^ 5 = φ * φ ^ 4 := by ring rw [this, h4] - have : phi * (3 * phi + 2) = 3 * phi ^ 2 + 2 * phi := by ring + have : φ * (3 * φ + 2) = 3 * φ ^ 2 + 2 * φ := by ring rw [this, h]; ring -/-! ## Section 6: Irrationality (re-export) - -`φ` and `ψ` are irrational; this is `Real.goldenRatio_irrational` and -`Real.goldenConj_irrational` in mathlib. -/ - -theorem phi_irrational : Irrational phi := Real.goldenRatio_irrational - -theorem psi_irrational : Irrational psi := Real.goldenConj_irrational - -end Physlib \ No newline at end of file +end Physlib.GoldenRatio From 1eb96d13d159b1d1dda8231d3c5d3dc4f888b338 Mon Sep 17 00:00:00 2001 From: gHashTag Date: Thu, 18 Jun 2026 14:19:03 +0000 Subject: [PATCH 4/4] proof: avoid fragile 'unfold' on abbrev goldenRatio Real.goldenRatio is an abbrev for (1+sqrt 5)/2, so reduce via 'show' on the unfolded form plus 'ring' instead of 'unfold Real.goldenRatio', which can be brittle on abbrevs across mathlib versions. --- Physlib/Mathematics/GoldenRatio.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/Mathematics/GoldenRatio.lean b/Physlib/Mathematics/GoldenRatio.lean index 0363979c4..a0ac0121d 100644 --- a/Physlib/Mathematics/GoldenRatio.lean +++ b/Physlib/Mathematics/GoldenRatio.lean @@ -92,8 +92,8 @@ Proof: `cos(π/5) = (1 + √5)/4` (mathlib's `Real.cos_pi_div_five`); doubling gives `2 cos(π/5) = (1 + √5)/2 = φ`. -/ theorem goldenRatio_two_cos_pi_div_five : φ = 2 * Real.cos (Real.pi / 5) := by rw [Real.cos_pi_div_five] - show Real.goldenRatio = 2 * ((1 + Real.sqrt 5) / 4) - unfold Real.goldenRatio + -- `Real.goldenRatio` is an `abbrev` for `(1 + √5)/2`, so this is defeq: + show (1 + Real.sqrt 5) / 2 = 2 * ((1 + Real.sqrt 5) / 4) ring /-- `φ` is a root of the quadratic `X² - X - 1`. -/