Masses Mass Genesis Majorana Closure From Cube Conj On Boundary Is Antipodal Not

The antipodal conjugation

In the Recognition Science framework, the masses of elementary particles are derived from the structure of a three-dimensional cube. The cube has eight vertices, each labeled by three bits of 0 or 1. Charge conjugation, the operation that turns a particle into its antiparticle, is modeled on this cube as the map that flips every bit: 000 becomes 111, 001 becomes 110, and so on. This is the antipodal map, sending each vertex to the vertex directly opposite it through the cube's center.

This identification has a powerful consequence. The map has no fixed points: no vertex is its own opposite. It is also an involution, meaning applying it twice returns you to the start. A fixed-point-free involution on a finite set always pairs the elements into orbits of size two, so the eight vertices split into four pairs. A Majorana fermion, a particle that is its own antiparticle, keeps exactly one vertex from each pair. The framework's library proves this: the Majorana span has four vertices, exactly half of the cube's eight. This is the origin of the factor one-half that appears in the neutrino mass formula.

The declaration conj_on_boundary_is_antipodal_not_dualDim concerns the boundary of the cube, not its interior. The boundary is made of six square faces. The same conjugation operation on a face flips the face's two coordinates, which is again an antipodal map on that face. The declaration establishes that this face-level conjugation is the antipodal map, not the dual-dimension map. The dual-dimension map sends a face's dimension to its complementary dimension, a different operation. The distinction matters because the framework uses the cube's boundary to count degrees of freedom, and the correct conjugation is the one that pairs opposite faces, not the one that swaps dimensions.

What the declaration does not claim is also precise. It does not claim that the antipodal map is the only possible way to model charge conjugation. It does not claim that the boundary conjugation alone determines particle masses; the full mass derivation requires additional structure, such as the assignment of vertices to particle generations. It also does not claim that the dual-dimension map is irrelevant to physics, only that it is not the conjugation used in this particular closure argument. The declaration is a theorem about a specific mathematical model, not a statement about the physical universe independent of that model.

/-- `conj` is the all-ones sign flip — the maximal-parity element of `(ℤ/2)³`. -/
theorem conj_eq_signFlip : conj = signFlip (1, 1, 1) := by decide

/-- 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

theorem majoranaSpan_card : majoranaSpan.card = 4 := evenClass_card

/-- The induced action of conjugation on faces: it sends the face `(axis, side)` to the OPPOSITE
    face `(axis, side+1)` on the same axis. -/
def conjFace (f : Face) : Face := (f.1, f.2 + 1)

What this page does not claim

The antipodal map is the only possible way to model charge conjugation. The boundary conjugation alone determines particle masses without additional structure. The dual-dimension map is physically irrelevant.

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: