Chemistry Quasicrystal Pentagon Diagonal Ratio

The pentagon diagonal ratio

In a regular pentagon, the ratio of a diagonal to a side is the golden ratio φ ≈ 1.618. The ratio of the shorter diagonal to the longer diagonal is the inverse, 1/φ ≈ 0.618. This is a classical fact of Euclidean geometry, tied to the pentagon's fivefold symmetry.

The Recognition Science framework's machine-checked library of formal theorems defines this ratio explicitly. The declaration pentagon_diagonal_ratio sets the short-to-long diagonal ratio equal to the framework's constant phi_ratio, which is 1/φ. The library proves that 1/φ = φ - 1, and that this value lies between 0.6 and 0.65. It also proves a simple energy model: the function (x - 1/φ)² is minimized exactly when x = 1/φ, and that minimum energy is zero.

This energy statement is a definitional choice, not a physical law. The framework models quasicrystal stability by choosing this convex energy proxy, then proves that the golden ratio inverse minimizes it. The proof is a theorem about that chosen model, not a derivation from atomic forces. The library also defines the Penrose tiling thick-to-thin rhombus area ratio as φ, and records that the regular icosahedron has 5-fold symmetry, where φ appears in vertex geometry.

What the declaration does not claim is broader. It does not prove that real quasicrystals are stable because of this energy proxy. It does not claim that the golden ratio is the only possible stable ratio; the library explicitly lists falsification criteria: stable quasicrystals with tile ratios not involving φ, or alternative irrational ratios like √2 or √3 producing equally stable structures, would contradict the prediction. The declaration establishes a formal identity and a model's internal consistency, not an empirical fact about materials.

/-- The ratio of short to long diagonal in a pentagon = 1/φ. -/
def pentagon_diagonal_ratio : ℝ := phi_ratio

/-- 1/φ = φ - 1 (fundamental φ identity). -/
theorem phi_ratio_identity : phi_ratio = Constants.phi - 1 := by
  rw [phi_ratio]
  have hphi_sq := Constants.phi_sq_eq
  have hphi_pos := Constants.phi_pos
  -- φ² = φ + 1 implies φ(φ-1) = 1, so 1/φ = φ - 1
  have h : Constants.phi * (Constants.phi - 1) = 1 := by
    calc Constants.phi * (Constants.phi - 1)
        = Constants.phi^2 - Constants.phi := by ring
      _ = (Constants.phi + 1) - Constants.phi := by rw [hphi_sq]
      _ = 1 := by ring
  field_simp
  linarith [h]

/-- φ ≈ 1.618, so 1/φ ≈ 0.618. -/
theorem phi_ratio_bounds : 0.6 < phi_ratio ∧ phi_ratio < 0.65 := by
  rw [phi_ratio_identity]
  constructor
  · have h := Constants.phi_gt_onePointSixOne
    linarith
  · have h := Constants.phi_lt_onePointSixTwo
    linarith

/-- Stability: energy is minimized at the golden ratio ratio. -/
theorem quasicrystal_stable (x : ℝ) : tiling_energy phi_ratio ≤ tiling_energy x := by
  dsimp [tiling_energy, phi_ratio]
  have : (0 : ℝ) ≤ (x - (1 / Constants.phi)) ^ 2 := sq_nonneg _
  simpa using this

/-- The minimum energy is exactly zero. -/
theorem min_energy_zero : tiling_energy phi_ratio = 0 := by
  simp only [tiling_energy, phi_ratio, sub_self, sq, mul_zero]

What this page does not claim

The declaration does not prove that real quasicrystals are stable because of this energy proxy. The declaration does not claim that the golden ratio is the only possible stable ratio. The energy model is a definitional choice, not a derived physical law.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/Quasicrystal.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: