Pith. sign in
module module moderate

IndisputableMonolith.Chemistry.Quasicrystal

show as:
view Lean formalization →

The Chemistry.Quasicrystal module assembles definitions and lemmas for quasicrystal tilings and stability expressed through golden ratio relations in Recognition Science. Chemists modeling aperiodic order would cite it when deriving energy minima from phi-based structures. The module consists of a sequence of supporting definitions and bounds with no central theorem.

claimThe module centers on the identity $1/\phi = \phi - 1$ together with predicates for tiling energy and the condition that quasicrystal energy reaches its minimum.

background

The module sits inside the Recognition Science framework and imports the Constants module, whose sole documented object is the time quantum $\tau_0 = 1$ tick. It introduces phi_ratio as the inverse golden ratio, tiling_energy as the structural cost of a tiling, quasicrystal_stable as the predicate that this cost is minimal, and several auxiliary ratios (penrose_ratio, pentagon_diagonal_ratio) that quantify icosahedral order. These objects rest on the self-similar fixed point phi forced at step T6 of the UnifiedForcingChain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the quasicrystal primitives that feed the stability claims appearing among its sibling declarations (quasicrystal_stable, min_energy_zero). It connects the chemistry domain to the phi-ladder and the Recognition Composition Law without recorded downstream theorems.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)