-- QLF_BorromeanAngles.lean -- Structural derivation of the 5-angle count in the proton's chirality- -- hiding configuration space. -- -- The Lenz factor m_p/m_e = |S_3| · π⁵ = 6π⁵ (Lean-anchored in -- QLF_LenzMassRatio.lean) uses `hidden_chirality_angles = 5` as a -- named substrate constant. This module structurally decomposes the -- 5 into two substrate origins: -- -- 5 = (Jacobi internal DOF of 3 quarks in 3D) + (chirality-mixing -- angles per gauge-fold) -- = 3 + 2 -- = 5 -- -- with each summand derived from explicit substrate principles: -- -- Jacobi internal DOF (3): -- 3 quarks × 3 spatial dimensions = 9 total spatial DOF -- − 3 CM translation DOF = 6 -- − 3 overall rotation DOF = 3 -- Standard 3-body QM reduction; rigorous group-theoretic fact. -- Each of the 3 internal DOF integrates over an angular range -- contributing π in the spherical-harmonic-style measure. -- -- Chirality-mixing DOF (2): -- The QLF gauge-fold has a 2-axis (real/imaginary) chirality- -- mixing structure per Hermitian-conjugate pair. Each pair -- contributes 2 angular freedoms — one for the real-part phase, -- one for the imaginary-part phase. The proton has 1 unifying -- gauge-fold (the overall +/- closure of the 3-quark Borromean -- state), giving 1 pair × 2 = 2 chirality-mixing angles. -- -- This rests on the QLF reading that the Pauli scalar group -- {+I, -I, +iI, -iI} (proven in QLF_Pauli.lean) decomposes as -- a 2-axis (sign × i-power) group with 2 independent binary -- orientations per Hermitian-conjugate pair. Promoting these -- discrete orientations to continuous angles for the chirality- -- mixing integration gives 2 angles per pair. This part is -- plausible but is the remaining open sub-target — see -- Proton_Resonance_R_e.md §6 for the honest scoping. -- -- The decomposition into 3 + 2 makes the 5-angle count explicit and -- shows precisely where the remaining open piece sits (the "2" -- chirality-mixing-per-pair claim). -- -- Combined with QLF_LenzMassRatio.lean, this gives: -- -- m_p / m_e = |S_3| · π^total_angular_DOF -- = 6 · π^5 -- -- with `total_angular_DOF = 5` now structurally decomposed. Closing -- the chirality-mixing count rigorously from QLF_Pauli.lean would -- close the m_p/m_e derivation chain end-to-end. -- -- Companion to: -- • Proton_Resonance_R_e.md §6 — 5-angle scoping -- • lean/QLF_LenzMassRatio.lean — uses hidden_chirality_angles = 5 -- • lean/QLF_Pauli.lean — Pauli scalar group structure -- • lean/QLF_TwistAlphabet.lean — gauge twist structure -- • lean/QLF_FineStructureSubstrate.lean — α-substrate sibling module import Mathlib.Analysis.SpecialFunctions.Pow.Real import QLF_LenzMassRatio namespace QLF /-- **Number of quarks in the proton's Borromean closure**. Standard particle physics; QLF reads the proton as a 3-component Borromean link (Hadrons_Markov_Blankets.md), where each quark is one component and the topology of the closure makes individual quarks unobservable in low-energy probes. -/ def quark_count : ℕ := 3 /-- **Number of spatial dimensions** in the QLF substrate. Derived in Magic_numbers.md from the 8-twist alphabet's 6+2 split (6 spatial twists organised into 3 axis-pairs), and used in QLF_FineStructureSubstrate.lean as `substrate_spatial_dimension`. -/ def spatial_dimension : ℕ := 3 /-- **Total spatial DOF of 3 quarks**: `3 × 3 = 9`. -/ def total_spatial_DOF : ℕ := quark_count * spatial_dimension /-- **Centre-of-mass translation DOF**: 3 (one per spatial dimension). Removed when working in the CM frame; the overall position of the proton is unphysical for chirality-hiding considerations. -/ def cm_translation_DOF : ℕ := 3 /-- **Overall rotation DOF**: 3 (the SO(3) Euler angles). Removed when working with the proton's internal configuration only; the overall orientation in space is unphysical for chirality-hiding considerations. -/ def overall_rotation_DOF : ℕ := 3 /-- **Internal Jacobi DOF**: `9 − 3 − 3 = 3`. The standard 3-body QM reduction: 9 spatial coordinates minus 3 CM translation minus 3 overall rotation = 3 internal DOF. Rigorous group-theoretic fact. -/ def internal_jacobi_DOF : ℕ := total_spatial_DOF - cm_translation_DOF - overall_rotation_DOF /-- **Chirality-mixing angles per gauge-fold Hermitian-conjugate pair**: 2. The QLF gauge-fold (`+`/`-` axis) has the Pauli scalar group `{+I, -I, +iI, -iI}` (Lean-verified in QLF_Pauli.lean) as its structural symmetry. This group decomposes as a 2-axis structure: • Sign axis (`+I` vs `-I`): binary orientation • Phase axis (`+1` vs `+i` factor): binary orientation Promoting these 2 discrete binary orientations to continuous angular freedoms for the chirality-mixing integration gives 2 angles per Hermitian-conjugate pair. **Open sub-target**: the precise mapping from the 4-element discrete Pauli scalar group to 2 continuous chirality-mixing angles requires rigorous derivation from the Pauli algebra and the gauge-fold's role in the Borromean closure topology. Stated here as a structural input matching Proton_Resonance_R_e.md §6. -/ def chirality_mixing_per_gauge_fold : ℕ := 2 /-- **Number of gauge-fold Hermitian-conjugate pairs in the proton**: 1. The proton's 3-quark Borromean closure is bound by a single unifying gauge-fold (the overall `+`/`-` closure that makes the composite state Pauli-closed). Individual quarks have their own sub-folds, but the chirality-hiding integration is over the OUTER gauge-fold's chirality-mixing freedoms, of which there is 1 per proton. -/ def gauge_fold_pair_count : ℕ := 1 /-- **Total chirality-mixing DOF**: `gauge_fold_pair_count × chirality_mixing_per_gauge_fold = 1 × 2 = 2`. -/ def chirality_mixing_DOF : ℕ := gauge_fold_pair_count * chirality_mixing_per_gauge_fold /-- **Total angular DOF in the chirality-hiding configuration space**: `internal_jacobi_DOF + chirality_mixing_DOF = 3 + 2 = 5`. -/ def total_angular_DOF : ℕ := internal_jacobi_DOF + chirality_mixing_DOF /-- **Internal Jacobi DOF equals 3** — rigorous 3-body QM reduction. -/ theorem internal_jacobi_DOF_eq_three : internal_jacobi_DOF = 3 := by unfold internal_jacobi_DOF total_spatial_DOF quark_count spatial_dimension cm_translation_DOF overall_rotation_DOF norm_num /-- **Chirality-mixing DOF equals 2** — from 1 gauge-fold × 2 angles per pair. -/ theorem chirality_mixing_DOF_eq_two : chirality_mixing_DOF = 2 := by unfold chirality_mixing_DOF gauge_fold_pair_count chirality_mixing_per_gauge_fold norm_num /-- **Total angular DOF equals 5** — structural decomposition `3 + 2 = 5`. This Lean-verifies the structural arithmetic underlying the `hidden_chirality_angles = 5` constant in QLF_LenzMassRatio.lean. -/ theorem total_angular_DOF_eq_five : total_angular_DOF = 5 := by unfold total_angular_DOF rw [internal_jacobi_DOF_eq_three, chirality_mixing_DOF_eq_two] /-- **Bridge to QLF_LenzMassRatio**: the structurally-decomposed `total_angular_DOF` equals the `hidden_chirality_angles` constant used in the Lenz mass-ratio derivation. This closes the structural decomposition of the 5-angle count against the named constant used in the m_p/m_e Lean theorem. The chirality-mixing-per-pair claim (= 2) remains the open sub-target requiring derivation from QLF_Pauli's scalar group. -/ theorem matches_lenz_hidden_chirality_angles : total_angular_DOF = hidden_chirality_angles := by rw [total_angular_DOF_eq_five] unfold hidden_chirality_angles rfl /-- **Counterfactual: 2-quark composite would give a different angular count**. A 2-quark composite (which doesn't actually form a stable Borromean closure — Borromean links require ≥ 3 components) would have: 2 × 3 − 3 − 3 = 0 internal DOF plus the 2 chirality-mixing DOF = 2 total angular DOF, giving `m_p_2q / m_e ≈ |S_2| · π² ≈ 2π² ≈ 19.7`. Off by a factor of 93 from the observed 1836; the 3-quark structure is essential. -/ def total_angular_DOF_2_quark_counterfactual : ℕ := (2 * spatial_dimension - cm_translation_DOF - overall_rotation_DOF) + chirality_mixing_DOF theorem total_angular_DOF_2_quark_eq : total_angular_DOF_2_quark_counterfactual = 2 := by unfold total_angular_DOF_2_quark_counterfactual spatial_dimension cm_translation_DOF overall_rotation_DOF chirality_mixing_DOF gauge_fold_pair_count chirality_mixing_per_gauge_fold norm_num /-- **Counterfactual: 4-quark composite would give 4 internal Jacobi DOF**. A 4-quark composite would have: 4 × 3 − 3 − 3 = 6 internal DOF plus 2 chirality-mixing DOF = 8 total angular DOF, giving `m_4q / m_e ~ |S_4| · π⁸ ≈ 24 · π⁸ ≈ 227,000`. Off by a factor of 124 from the observed; the 3-quark Borromean is the minimum- complexity structure that matches PDG. -/ def total_angular_DOF_4_quark_counterfactual : ℕ := (4 * spatial_dimension - cm_translation_DOF - overall_rotation_DOF) + chirality_mixing_DOF theorem total_angular_DOF_4_quark_eq : total_angular_DOF_4_quark_counterfactual = 8 := by unfold total_angular_DOF_4_quark_counterfactual spatial_dimension cm_translation_DOF overall_rotation_DOF chirality_mixing_DOF gauge_fold_pair_count chirality_mixing_per_gauge_fold norm_num /-- **Counterfactual summary**: only the 3-quark composite (with its Borromean closure) gives 5 angular DOF and matches `m_p/m_e = 6π⁵`. -/ theorem only_3_quark_gives_five_angles : total_angular_DOF = 5 ∧ total_angular_DOF_2_quark_counterfactual = 2 ∧ total_angular_DOF_4_quark_counterfactual = 8 := by exact ⟨total_angular_DOF_eq_five, total_angular_DOF_2_quark_eq, total_angular_DOF_4_quark_eq⟩ end QLF