Chemistry Quasicrystal Icosahedral Order

Five-fold order

Quasicrystals are materials whose atoms arrange in a pattern that is ordered but never repeats periodically. Unlike ordinary crystals, which tile space by repeating a single unit cell, quasicrystals use two or more tile shapes in a non-repeating sequence. Their diffraction patterns show sharp spots, a sign of long-range order, yet the pattern lacks translational symmetry. The most famous example is the Penrose tiling, discovered by Roger Penrose in the 1970s, which uses two rhombus shapes whose areas are in the golden ratio φ ≈ 1.618.

Icosahedral quasicrystals, first reported by Dan Shechtman in 1982, have a diffraction pattern with five-fold symmetry axes. Five-fold symmetry is forbidden in ordinary periodic crystals, which is why Shechtman's discovery was initially met with skepticism. The golden ratio appears naturally in this geometry: a regular icosahedron's edge-to-circumradius ratio involves φ, and the ratio of a pentagon's diagonal to its side is also φ. These are classical facts, established long before quasicrystals were known.

In the Recognition Science framework, a machine-checked library of formal theorems, the declaration icosahedral_order is a definition: it sets the value 5 as a natural number. The accompanying theorem icosahedron_involves_phi states that this value equals 5, which is true by definition. The framework models the stability of quasicrystals through an energy proxy: tiling_energy(x) = (x − 1/φ)², which is minimized when x = 1/φ, the golden ratio's inverse. A theorem proves this energy is zero at that point and non-negative everywhere else. This is a mathematical statement about a chosen energy function, not a measurement of any real material.

What the declaration does not claim is important. It does not assert that any physical quasicrystal exists, nor that real quasicrystals are stable because of this energy function. The framework's docstring lists falsification criteria: if stable quasicrystals were found with tile ratios not involving φ, or if other irrational ratios like √2 or √3 produced equally stable structures, the prediction would fail. But the formal theorem itself only proves a property of the defined energy function, not a property of nature. The connection between the formal model and actual materials remains a hypothesis, not a proved result.

The value of icosahedral_order in the framework is as a bridge: it names the five-fold symmetry that characterizes icosahedral quasicrystals and ties that symmetry to the golden ratio through the energy model. It is a definitional choice, not an empirical discovery. The framework's contribution is to make explicit the mathematical structure that connects φ to five-fold order, and to state clearly what would falsify that connection. Whether real quasicrystals follow this model is a question for experiment, not for formal proof.

/-- Icosahedral quasicrystals have 5-fold symmetry.
    5-fold = appearance of φ in vertices. -/
def icosahedral_order : ℕ := 5

/-- 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]

/-- Convex energy proxy minimized at `phi_ratio`. -/
def tiling_energy (x : ℝ) : ℝ := (x - phi_ratio) ^ 2

What this page does not claim

No claim that any physical quasicrystal is stable because of this energy function. No claim that the golden ratio is the only possible ratio for stable quasicrystals. No claim that icosahedral_order proves anything about real materials beyond a definitional link.

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: