Encyclopedia Masses Masses Mass Genesis Majorana Closure From Cube Coupling Dimension Not Through Pa
ARTICLE 3 claims 3 theorems
Masses Mass Genesis Majorana Closure From Cube Coupling Dimension Not Through Pa
A combinatorial fact about a cube, that its eight vertices split evenly by parity, forces the half that separates Majorana from Dirac particles.
The closure keystone
A cube has eight corners. Color them by the parity of their coordinates: four have an even number of 1s, four have an odd number. Every edge of the cube connects a corner of one color to a corner of the other. This is the classical fact of bipartiteness, and it is the entire engine behind a recent result in the Recognition Science framework about why a Majorana particle carries half the degrees of freedom of a Dirac particle.
In particle physics, a Dirac fermion is described by two independent two-component spinors, one for each chirality, left and right. A Majorana fermion is its own antiparticle and needs only one such component. The framework's library of machine-checked theorems models this distinction on the recognition 3-cube, the set of eight binary triples. The two chiralities are identified with the two parity classes of the cube, and a Dirac closure spans all eight vertices while a Majorana closure spans only the four of one class. The closure factor, the fraction of the cube's vertices that a particle's description occupies, is therefore 1 for Dirac and 1/2 for Majorana.
The half is not put in by hand. The library proves, by direct computation, that the cube has eight vertices, that each parity class has exactly four, and that the two classes are disjoint and cover the cube. It also proves that the map flipping all three bits, the natural reading of charge conjugation, has no fixed point and swaps the two classes. A fixed-point-free involution on a finite set always pairs its elements, so the eight vertices fall into four orbits of two, and a self-conjugate closure keeps one per orbit. Both routes, the parity split and the conjugation pairing, arrive at the same 4/8.
What the declaration does not claim is that this combinatorial half, by itself, produces the measured neutrino mass ratios. The library is explicit that the full agreement with the observed splittings rests on two further inputs that remain hypotheses: the size of the solar step and the choice of which cube cells the neutral sector counts. The proved half improves the clean ratio from 18 percent high to 7 percent low, but the sub-percent fit is achieved within the framework only with those additional assumptions.
THEOREM cube_card · evenClass_card · oddClass_card · classes_disjoint · classes_cover · IndisputableMonolith/Masses/MassGenesis/MajoranaClosureFromCube.lean
/-- `V = 8` vertices. -/
theorem cube_card : (Finset.univ : Finset Cube).card = 8 := by decide
/-- Bipartite, even class: `V/2 = 4` vertices. -/
theorem evenClass_card : evenClass.card = 4 := by decide
/-- Bipartite, odd class: `V/2 = 4` vertices. -/
theorem oddClass_card : oddClass.card = 4 := by decide
/-- The two parity classes are disjoint. -/
theorem classes_disjoint : Disjoint evenClass oddClass := by decide
/-- The two parity classes cover the cube. -/
theorem classes_cover : evenClass ∪ oddClass = Finset.univ := by decide
THEOREM conj_no_fixedPoint · conj_even_eq_odd · IndisputableMonolith/Masses/MassGenesis/MajoranaClosureFromCube.lean
/-- Conjugation has **no fixed point** (you can never have `v = v̄`). This is what
forces orbits of size `2` and hence the exact halving. -/
theorem conj_no_fixedPoint : ∀ v : Cube, conj v ≠ v := by decide
/-- Conjugation carries the even class bijectively onto the odd class: every
conjugation orbit holds exactly one even and one odd vertex. -/
theorem conj_even_eq_odd : evenClass.image conj = oddClass := by decide
THEOREM diracSpan_card · majoranaSpan_card · IndisputableMonolith/Masses/MassGenesis/MajoranaClosureFromCube.lean
theorem diracSpan_card : diracSpan.card = 8 := cube_card
theorem majoranaSpan_card : majoranaSpan.card = 4 := evenClass_card
What this page does not claim
The declaration does not derive the full neutrino mass spectrum from the half alone. It does not prove that the solar step of 2 is forced rather than chosen. It does not establish which cube cells the neutral sector counts.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Masses/MassGenesis/MajoranaClosureFromCube.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What physical mechanism selects the solar step of 2 in the neutrino sector?
- Why does the neutral atmospheric step count the cube's vertices rather than its faces?
- How does the chirality-to-parity identification arise from the recognition dynamics?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM cube_card · evenClass_card · oddClass_card · classes_disjoint · classes_cover · IndisputableMonolith/Masses/MassGenesis/MajoranaClosureFromCube.lean
/-- `V = 8` vertices. -/ theorem cube_card : (Finset.univ : Finset Cube).card = 8 := by decide/-- Bipartite, even class: `V/2 = 4` vertices. -/ theorem evenClass_card : evenClass.card = 4 := by decide/-- Bipartite, odd class: `V/2 = 4` vertices. -/ theorem oddClass_card : oddClass.card = 4 := by decide/-- The two parity classes are disjoint. -/ theorem classes_disjoint : Disjoint evenClass oddClass := by decide/-- The two parity classes cover the cube. -/ theorem classes_cover : evenClass ∪ oddClass = Finset.univ := by decideThe cube has eight vertices, each parity class has exactly four, and the two classes are disjoint and cover the cube. cube_card · evenClass_card · oddClass_card · classes_disjoint · classes_cover · IndisputableMonolith/Masses/MassGenesis/MajoranaClosureFromCube.leanTHEOREM conj_no_fixedPoint · conj_even_eq_odd · IndisputableMonolith/Masses/MassGenesis/MajoranaClosureFromCube.lean
/-- Conjugation has **no fixed point** (you can never have `v = v̄`). This is what forces orbits of size `2` and hence the exact halving. -/ theorem conj_no_fixedPoint : ∀ v : Cube, conj v ≠ v := by decide/-- Conjugation carries the even class bijectively onto the odd class: every conjugation orbit holds exactly one even and one odd vertex. -/ theorem conj_even_eq_odd : evenClass.image conj = oddClass := by decideThe map flipping all three bits has no fixed point and swaps the two parity classes. conj_no_fixedPoint · conj_even_eq_odd · IndisputableMonolith/Masses/MassGenesis/MajoranaClosureFromCube.leanTHEOREM diracSpan_card · majoranaSpan_card · IndisputableMonolith/Masses/MassGenesis/MajoranaClosureFromCube.lean
theorem diracSpan_card : diracSpan.card = 8 := cube_cardtheorem majoranaSpan_card : majoranaSpan.card = 4 := evenClass_cardA Dirac closure spans all eight vertices and a Majorana closure spans only the four of one class. diracSpan_card · majoranaSpan_card · IndisputableMonolith/Masses/MassGenesis/MajoranaClosureFromCube.lean