pith. sign in
module module high

IndisputableMonolith.Physics.CrystalSystemsFromConfigDim

show as:
view Lean formalization →

The module establishes that Recognition Science yields exactly seven crystal systems in total, five orthogonal and two oblique. Physicists classifying lattices in discrete spacetime models cite this partition. The module achieves the result by importing the base time quantum and enumerating configurations via sibling definitions for orthogonal cases and the overall partition.

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

background

The module sits inside the Recognition Science framework, where structures derive from the forcing chain and the phi-ladder built on the fundamental time quantum. It imports τ₀ = 1 tick from IndisputableMonolith.Constants. Local definitions include OrthogonalCrystalSystem for axis-orthogonal lattices, seven_systems_partition for the complete enumeration, and CrystalSystemsCert for certification of the count.

proof idea

This is a definition module, no proofs. It introduces the sibling declarations OrthogonalCrystalSystem, orthogonalSystem_count, seven_systems_partition, bravaisLatticeCount, bravais_eq, and CrystalSystemsCert to formalize the classification from configuration dimension.

why it matters in Recognition Science

The module supplies the crystal-systems classification that anchors lattice derivations in the Recognition Science physics layer. It connects the imported time quantum τ₀ directly to the seven-system partition, consistent with the eight-tick octave and D = 3 spatial dimensions in the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)