Masses Mass Genesis Majorana Closure From Cube Charge Conjugation Does Not Reali

The charge conjugation theorem

Charge conjugation is the symmetry that flips every internal charge of a particle, turning matter into antimatter. In the Recognition Science framework, the framework models this operation on a three-dimensional cube of eight vertices, where each vertex is a pattern of three binary charges. The framework's library of formal theorems proves that this operation, which flips all three bits, is an involution: applying it twice returns to the start. The library also proves that the operation has no fixed point, meaning every vertex is sent to a different vertex.

The declaration in question establishes a specific negative result. The framework defines a quantity called dual dimension, a count that pairs each dimension of a cube with its opposite: dimension 0 pairs with 2, and dimension 1 pairs with itself. The theorem proves that charge conjugation, the all-bit flip, does not realize this dual dimension pairing. In plain terms, flipping every charge does not swap the roles of the two extreme dimensions. The theorem is a formal statement about the cube's combinatorics, and it is proved by direct computation in the library.

The theorem's importance is what it rules out. A prior line of reasoning in the framework had considered whether charge conjugation could be the mechanism that produces a certain half-factor in neutrino mass ratios. The theorem shows that this particular mechanism fails. The framework instead identifies charge conjugation with a different operation: the antipodal map that sends each vertex to its opposite. That map is a fixed-point-free involution, and the library proves that such an involution always halves a finite set, pairing the eight vertices into four orbits of two. This halving, not the dual dimension pairing, is what the framework uses to derive the half-factor.

The theorem does not claim that charge conjugation is impossible or unphysical. It claims only that one specific mathematical identification fails. The framework's library retains charge conjugation as the antipodal map, and that identification is what supports the later derivation of the Majorana half-factor. The negative result is therefore a cleanup: it removes a wrong turn and leaves the working path intact.

/-- **THEOREM.** The edge dimension `d = 1` is the UNIQUE fixed point of cube duality on the
    three boundary dimensions `{0,1,2}`. -/
theorem dualDim_fixedPoint_unique (d : ℕ) (hd : d ≤ 2) : dualDim d = d ↔ d = 1 := by
  unfold dualDim; omega

/-- Conjugation is an involution. -/
theorem conj_involutive : ∀ v : Cube, conj (conj v) = v := 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

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

What this page does not claim

The theorem does not claim that charge conjugation is impossible or unphysical. The theorem does not claim that the dual dimension pairing is impossible, only that charge conjugation does not realize it. The theorem does not claim that the Majorana half-factor is derived from the dual dimension pairing.

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: