pith. sign in
module module high

IndisputableMonolith.Physics.CrystalSystemsFromConfigDim

show as:
view Lean formalization →

The module derives the classification of crystal systems from configuration dimension in Recognition Science, asserting a total of seven systems partitioned into five orthogonal and two oblique. Condensed matter physicists modeling lattices under RS constraints would cite the partition for its direct count. It is a definition module containing no proofs.

claimThere exist seven crystal systems in total, with five orthogonal and two oblique: $5 + 2 = 7$.

background

The module imports Constants, whose fundamental object is the RS time quantum τ₀ = 1 tick. It introduces sibling definitions including OrthogonalCrystalSystem, seven_systems_partition, bravaisLatticeCount, and CrystalSystemsCert. The local theoretical setting is the extraction of crystal systems from config dim, with the module doc stating the partition directly.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the seven-system partition that feeds CrystalSystemsCert and bravais_eq inside the same file. It fills the classification step required for lattice models in the Recognition Science physics layer.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)