seven_systems_partition
The equality 7 = 5 + 2 encodes the partition of crystal systems into five orthogonal-axis and two oblique classes in three-dimensional crystallography. Recognition Science modelers cite it when populating the CrystalSystemsCert structure that certifies the 14 Bravais lattices. The proof is a one-line decision procedure that verifies the arithmetic identity directly.
claimThe total number of crystal systems in three dimensions satisfies $7 = 5 + 2$, where the five orthogonal systems are those with mutually perpendicular axes (cubic, tetragonal, orthorhombic, trigonal, hexagonal) and the two oblique systems are monoclinic and triclinic.
background
The module Crystal Systems from configDim treats seven crystal systems as the basic partition of 3D crystallography. Five are orthogonal-axis-based and correspond to configDim D = 5: cubic, tetragonal, orthorhombic, trigonal, and hexagonal. The remaining two are oblique: monoclinic and triclinic. This arithmetic split yields 14 Bravais lattices as seven systems each admitting primitive and centered variants.
proof idea
The proof is a one-line term that invokes the decide tactic to confirm the numerical equality 7 = 5 + 2.
why it matters in Recognition Science
This theorem supplies the seven_total field inside the CrystalSystemsCert definition, which certifies the breakdown of Bravais lattices in three dimensions. It aligns with the Recognition Science landmark that D = 3 spatial dimensions forces the eight-tick octave structure underlying lattice classifications. The result closes a small but necessary step in linking configDim to the standard 7-system partition of crystallography.
scope and limits
- Does not derive the seven crystal systems from the Recognition functional equation or J-cost.
- Does not list the explicit names or symmetries of each system.
- Does not address the connection to the phi-ladder or mass formulas.
- Does not prove the existence of 14 Bravais lattices beyond the arithmetic count.
Lean usage
def crystalSystemsCert : CrystalSystemsCert where five_orthogonal := orthogonalSystem_count seven_total := seven_systems_partition bravais_14 := bravais_eqformal statement (Lean)
32theorem seven_systems_partition : (7 : ℕ) = 5 + 2 := by decide
proof body
Term-mode proof.
33
34/-- 14 Bravais lattices. -/