parity_violation
plain-language theorem explainer
Parity violation is established by showing that the left-handed coupling constant differs from the right-handed one in the weak sector. Particle physicists deriving chiral asymmetry from ledger geometry would cite this when building the SU(2)_L structure. The proof reduces to a single decidable equality check on the two Boolean constants.
Claim. Left-handed fermions couple to the weak force while right-handed fermions do not, yielding $L ≠ R$.
background
The Weak Force Emergence module derives the weak interaction from the 3D ledger geometry that produces three SU(2) generators and from the orientation of the eight-tick cycle that selects one chirality. The sibling definitions assign leftHandedCouples the value true and rightHandedCouples the value false, encoding the statement that only left-handed fermions participate. Upstream Lepton inductive types from CubeFaceUniversality and AnomalousMoments supply the fermion species whose couplings are distinguished.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the inequality between the two Boolean constants.
why it matters
This theorem supplies the parity-violation claim listed in the module documentation for weak-force emergence. It realizes the framework prediction that chirality arises from the eight-tick cycle orientation and feeds the broader ledger-based account of SU(2)_L. No downstream theorems are recorded yet, leaving the result as a foundational but isolated step toward quantitative weak-interaction predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.