Pith. sign in
module module moderate

IndisputableMonolith.Physics.CrystalSystemsFromConfigDim

show as:
view Lean formalization →

Module that partitions the seven classical crystal systems into five orthogonal and two oblique classes, tying the count to configuration-dimension constraints in Recognition Science. Crystallographers and RS auditors cite it for the forced 7-system / 14-Bravais tally. The argument is mostly definitional enumeration plus equality certificates, not a deep analytic proof.

claimThere are exactly seven crystal systems: five orthogonal and two oblique. The associated Bravais lattice count equals fourteen, matching the classical partition forced by three-dimensional configuration geometry.

background

Classical crystallography lists seven crystal systems (triclinic, monoclinic, orthorhombic, tetragonal, trigonal, hexagonal, cubic) and fourteen Bravais lattices. In Recognition Science the spatial dimension is forced to $D=3$ (forcing step T8), so lattice point-group and centering choices live in a three-dimensional configuration space.

This module imports only Mathlib and the RS constants layer (native tick $\tau_0$). It introduces an orthogonal-versus-oblique split: five systems whose metric tensors can be diagonalized in an orthogonal frame, and two that retain shear (oblique) angles. Sibling definitions name the orthogonal class, count it, state the seven-system partition, and record the Bravais total.

proof idea

Definition-and-certificate module rather than a long derivation. It declares the orthogonal crystal-system type, proves the orthogonal count, states a partition lemma that the seven systems are five orthogonal plus two oblique, fixes the Bravais lattice cardinality at fourteen, and packages the equalities into a small certificate structure. No heavy analysis; the work is enumeration aligned with the $D=3$ configuration constraint.

why it matters in Recognition Science

Places the classical 7-system / 14-Bravais census inside the RS forcing chain: once $D=3$ is fixed (T8), the orthogonal/oblique split and lattice count are no longer empirical accidents but configuration-dimension bookkeeping. Downstream consumers (none linked yet in the graph) would use the certificate when assembling solid-state or condensed-matter claims from RS primitives. The module does not itself derive phonon spectra or selection rules; it only locks the discrete taxonomy.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)