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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND