feat(Mathematics): add Physlib/Mathematics/GoldenRatio.lean

[gHashTag]

Summary

This PR adds Physlib/Mathematics/GoldenRatio.lean, a Lean 4 module that provides a Physlib-namespace wrapper around Mathlib's Mathlib.NumberTheory.Real.GoldenRatio, extended with physics-flavoured derived identities that Mathlib does not state.

Motivation

The constant φ = (1 + √5)/2 appears throughout physics:

• Quasicrystals: Penrose tilings, icosahedral viral capsids, metallic alloys
• Coxeter geometry: H₄ root system underlying the 600-cell and the binary icosahedral group 2I ⊂ SU(2)
• KAM theory: 1/φ is the "most irrational" rotation number
• Icosian Coxeter program: coupling-constant relations

Mathlib already proves the purely algebraic facts (golden equation, positivity, irrationality, Binet's formula). Physlib downstream code needs both a namespace shortcut and a handful of derived results.

Contents

Section	Declarations
§1 Shortcuts	phi, psi (abbrevs)
§2 Mathlib re-exports	phi_sq, phi_pos, phi_ne_zero, one_lt_phi, phi_lt_two, psi_neg, psi_ne_zero, psi_sq, phi_psi_sum, phi_psi_prod, phi_inv_eq_neg_psi, psi_inv_eq_neg_phi
§3 Physics-flavoured identities	phi_inv_pos, phi_inv_lt_one, phi_continued_fraction (φ = 1 + 1/φ), phi_two_cos_pi_div_five (φ = 2 cos π/5), phi_quadratic, psi_quadratic, phi_psi_vieta
§4 Numerical bounds	phi_lower_bound, phi_upper_bound, phi_bounds (1.6 < φ < 1.7)
§5 Powers of φ	phi_pow_three, phi_pow_four, phi_pow_five (Fibonacci-coefficient pattern)
§6 Irrationality	phi_irrational, psi_irrational (re-export)

Total: 226 lines, 33 declarations (31 theorems + 2 abbrevs), 0 sorry, 0 axiom.

Aggregator

Added public import Physlib.Mathematics.GoldenRatio to Physlib.lean alphabetically between Geometry.Metric.Riemannian.Defs and InnerProductSpace.Adjoint.

Lean / Mathlib version

• leanprover/lean4:v4.29.1
• Mathlib v4.29.1 (the rev currently pinned in lakefile.lean)

Origin

Contributed by the trinity-s3ai project, Wave 7 task W7.3. All proofs use standard Mathlib tactics (linarith, ring, nlinarith, norm_num, Real.sqrt_lt_sqrt, Real.cos_pi_div_five).

[zhikaip]

I don't think this is a good idea, there are many uses of phi throughout physics (most notably as a phase, or as a potential) and dedicating it to golden ratio doesn't seem right to me. Maybe you could use local notation here for Real.goldenRatio, and add the API directly around that?

[gHashTag]

@zhikaip: dropped the phi/psi abbrevs entirely. The module now builds the API directly on Real.goldenRatio / Real.goldenConj and uses mathlib's own scoped[goldenRatio] notation via open scoped goldenRatio, so φ/ψ stay file-local and are never exported globally -- no collision with φ-as-phase / φ-as-potential. I also removed the thin re-export lemmas that only wrapped mathlib; what remains is just the handful of identities mathlib does not state.

[jstoobysmith]

Maybe I can ask where the direction of this PR is heading in terms of physics, do you have plans to do something which uses this?

[gHashTag]

Maybe I can ask where the direction of this PR is heading in terms of physics, do you have plans to do something which uses this?

@jstoobysmith: on direction -- the physics use is the H4 / icosahedral thread: φ = 2 cos(π/5) as the bridge from the algebraic golden ratio to the 5-fold symmetry of the pentagon, the 600-cell and the binary icosahedral group 2I ⊂ SU(2), plus the 1/φ "most irrational" rotation number for KAM / quasicrystal contexts. If you'd prefer this not live as a dedicated module, I'm happy to either trim it to just φ = 2 cos(π/5) + the φ^n closed forms, or upstream the genuinely-missing lemmas straight to Mathlib.NumberTheory.Real.GoldenRatio. Whichever fits Physlib better.