monoclinicConstraint
plain-language theorem explainer
The declaration defines the monoclinic constraint on lattice parameters as the condition that angles alpha and gamma both equal ninety degrees. Crystallographers classifying the seven crystal systems inside the Recognition Science derivation would cite this when enumerating allowed periodic tilings. The definition is a direct conjunction of two angle equalities taken from the LatticeParams structure.
Claim. For lattice parameters $p$ with angles $alpha$, $beta$, $gamma$, the monoclinic constraint holds precisely when $alpha = 90^circ$ and $gamma = 90^circ$.
background
LatticeParams records the three edge lengths a, b, c together with the three interaxial angles: alpha between edges b and c, beta between a and c, and gamma between a and b. The module derives the seven crystal systems from the eight-tick octave that forces three spatial dimensions and restricts rotational symmetries to orders 1, 2, 3, 4, 6 so that identical units tile space periodically without gaps. Upstream results supply the LatticeParams structure itself; the listed constants (fine-structure alpha, Euler-Mascheroni gamma) appear in sibling files but are not invoked here.
proof idea
The definition is a one-line abbreviation that equates the monoclinic constraint to the conjunction of the two angle conditions drawn directly from the LatticeParams fields.
why it matters
This definition supplies the monoclinic case inside the seven crystal systems enumerated in the module documentation. It contributes to the exact count of seven systems that follows from the space-filling rules in three dimensions forced by the eight-tick structure. No downstream uses are recorded, leaving open the integration of these angle constraints with the phi-ladder mass formula or the alpha band predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.