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).

Co-authored-by: gHashTag uniwatisit79@gmail.com

[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?

[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?