Encyclopedia Masses Masses Mass Genesis T10 Hypercube Substrate

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Hypercube Substrate

The framework derives the graph on which particle masses live from a single atomicity rule, and the graph turns out to be a hypercube.

Verify this page

The mass substrate

A hypercube is the shape you get by taking all strings of d bits and connecting any two strings that differ in exactly one bit. For d=3, this is an ordinary cube: eight corners, each joined to three neighbors. The framework's T10 module proves that the graph of possible mass states is exactly this hypercube, and that this shape is forced by the rule that a ledger (a discrete record of events) can only be posted to atomically, one bit flip at a time.

The proof starts with a simple observation. If each state is a pattern of d bits, and a legal move flips exactly one bit, then the reachable states from any starting point form a hypercube. The module proves this directly: the adjacency relation, defined as differing in exactly one bit, is equivalent to the existence of a single bit flip. This is the theorem oneBitDiff_iff_hypercubeAdj, and it is the core of the derivation.

From this, the module proves several structural facts about the hypercube. The number of edges in a d-dimensional hypercube is d times 2^(d-1). A cut, the set of edges leaving any subset of vertices, is at most this total. For the special subset of even-parity states, the cut equals the full total, meaning that half the hypercube has all its edges leaving it. These are not assumptions; they are consequences of the atomicity rule.

In Recognition Science, this hypercube is the substrate on which particle masses are placed. The module does not derive the dimension d; that remains OPEN. It does prove that if the measured lepton mass ratios are to be supported, the wall (the cut size) must be large enough. The muon ratio forces d to be at least 9, and the tau ratio forces d to be at least 13. For the three-dimensional cell used in mass-genesis modules, the wall is 4 times 3, and the muon and tau ratios force at least 3 and 5 such cells respectively.

The consequence is that the framework's mass story has a firm geometric footing. The graph is not chosen to fit the data; it is derived from the atomicity of ledger posts. The dimension remains a target, but the shape is proved.

THEOREM oneBitDiff_iff_hypercubeAdj · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean
oneBitDiff_iff_hypercubeAdj · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean:156 
/-- H1. -/
theorem oneBitDiff_iff_hypercubeAdj {d : Nat} (p q : Pattern d) :
    OneBitDiff p q ↔ HypercubeAdj p q := by
  constructor
  · intro h
    rcases h with ⟨k, hk, huniq⟩
    apply (hypercubeAdjExists_iff_hypercubeAdj p q).mp
    refine ⟨k, ?_⟩
    funext i
    by_cases hi : i = k
    · simp [flipAt, hi, (bool_ne_iff_eq_not).mp hk]
    · have heq : p i = q i := by
        by_contra hne; exact hi (huniq i hne)
      simp [flipAt, hi, heq]
  · intro h
    rcases (hypercubeAdjExists_iff_hypercubeAdj p q).mpr h with ⟨k, rfl⟩
    refine ⟨k, ?_, ?_⟩
    · intro heq
      have : (!p k) = p k := by simpa [flipAt] using heq
      exact Bool.not_ne_self (p k) this
    · intro k' hk'
      by_contra hne
      have : flipAt p k k' = p k' := by simp [flipAt, hne]
      exact hk' (by simp [this])
THEOREM card_directedHypercubeEdges · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean
card_directedHypercubeEdges · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean:378 
lemma card_directedHypercubeEdges (d : Nat) :
    (directedHypercubeEdges d).card = d * 2 ^ d := by
  classical
  have hpart :
      (directedHypercubeEdges d).card =
        ∑ p : Pattern d,
          ((directedHypercubeEdges d).filter (fun e => e.1 = p)).card := by
    simpa [directedHypercubeEdges] using
      (Finset.card_eq_sum_card_fiberwise
        (s := directedHypercubeEdges d) (f := Prod.fst) (t := Finset.univ)
        (fun _ _ => Finset.mem_univ _))
  refine hpart.trans ?_
  have hfiber (p : Pattern d) :
      ((directedHypercubeEdges d).filter (fun e => e.1 = p)).card = d := by
    let N := Finset.univ.filter (fun q : Pattern d => HypercubeAdj p q)
    have hset :
        (directedHypercubeEdges d).filter (fun e => e.1 = p) =
          N.image (fun q => (p, q)) := by
      ext e
      constructor
      · intro he
        rcases Finset.mem_filter.mp he with ⟨he', hp⟩
        rcases Finset.mem_filter.mp he' with ⟨_, hadj⟩
        exact Finset.mem_image.mpr
          ⟨e.2, by simp [N, hp ▸ hadj], Prod.ext hp.symm rfl⟩
      · intro he
        rcases Finset.mem_image.mp he with ⟨q, hq, rfl⟩
        simp only [Finset.mem_filter, Finset.mem_univ, true_and, N] at hq
        exact Finset.mem_filter.mpr
          ⟨Finset.mem_filter.mpr ⟨Finset.mem_univ _, hq⟩, rfl⟩
    have hinj : Set.InjOn (fun q : Pattern d => (p, q)) N := by
      intro _ _ _ _ h; exact (Prod.mk.inj h).2
    rw [hset, Finset.card_image_of_injOn hinj, card_neighbors]
  simp_rw [hfiber]
  simp [Finset.sum_const, Patterns.card_pattern, Nat.mul_comm]
THEOREM hypercubeCut_evenClass · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean
hypercubeCut_evenClass · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean:537 
/-- H5. Even class attains total edge count. -/
theorem hypercubeCut_evenClass {d : Nat} (hd : 0 < d) :
    hypercubeCut (evenClass d) = d * 2 ^ (d - 1) := by
  classical
  haveI : NeZero d := ⟨Nat.pos_iff_ne_zero.mp hd⟩
  have hout (p : Pattern d) (hp : p ∈ evenClass d) (q : Pattern d)
      (hq : HypercubeAdj p q) : q ∉ evenClass d := by
    intro hqeven
    have hp0 : hammingWeight p % 2 = 0 := by simpa [evenClass] using hp
    have hq0 : hammingWeight q % 2 = 0 := by simpa [evenClass] using hqeven
    exact (hypercubeAdj_hammingWeight_parity hq) (by simp [hp0, hq0])
  let S := (evenClass d).biUnion fun p =>
    (Finset.univ : Finset (Fin d)).image fun k => (p, flipAt p k)
  have hset :
      Finset.univ.filter (fun e : Pattern d × Pattern d =>
          HypercubeAdj e.1 e.2 ∧ e.1 ∈ evenClass d ∧ e.2 ∉ evenClass d) = S := by
    ext e
    constructor
    · intro he
      rcases Finset.mem_filter.mp he with ⟨_, hadj, hA, _⟩
      rcases (hypercubeAdjExists_iff_hypercubeAdj e.1 e.2).mpr hadj with ⟨k, hk⟩
      exact Finset.mem_biUnion.mpr
        ⟨e.1, hA, Finset.mem_image.mpr ⟨k, Finset.mem_univ k, Prod.ext rfl hk.symm⟩⟩
    · intro he
      rcases Finset.mem_biUnion.mp he with ⟨p, hp, he'⟩
      rcases Finset.mem_image.mp he' with ⟨k, _, rfl⟩
      exact Finset.mem_filter.mpr
        ⟨Finset.mem_univ _, hypercubeAdj_flipAt p k, hp,
          hout p hp _ (hypercubeAdj_flipAt p k)⟩
  have hdisj :
      ∀ x ∈ evenClass d, ∀ y ∈ evenClass d, x ≠ y →
        Disjoint
          ((Finset.univ : Finset (Fin d)).image fun k => (x, flipAt x k))
          ((Finset.univ : Finset (Fin d)).image fun k => (y, flipAt y k)) := by
    intro x _ y _ hne
    refine Finset.disjoint_left.mpr ?_
    intro e hx hy
    rcases Finset.mem_image.mp hx with ⟨_, _, rfl⟩
    rcases Finset.mem_image.mp hy with ⟨_, _, hxy⟩
    exact hne (Prod.mk.inj hxy).1.symm
  have hterm (p : Pattern d) :
      ((Finset.univ : Finset (Fin d)).image fun k => (p, flipAt p k)).card = d := by
    rw [Finset.card_image_of_injective]
    · simp [Fintype.card_fin]
    · intro a b hab; exact flipAt_inj_left p (Prod.mk.inj hab).2
  have hcardS : S.card = (evenClass d).card * d := by
    rw [Finset.card_biUnion hdisj]
    simp [hterm, Finset.sum_const]
  have heven := card_evenClass_of_pos d
  have hcutS : hypercubeCut (evenClass d) = S.card := by
    unfold hypercubeCut; exact congrArg Finset.card hset
  calc
    hypercubeCut (evenClass d) = S.card := hcutS
    _ = (evenClass d).card * d := hcardS
    _ = 2 ^ (d - 1) * d := by rw [heven]
    _ = d * 2 ^ (d - 1) := by ring
THEOREM muon_ratio_forces_accounts · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean
muon_ratio_forces_accounts · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean:938 
theorem muon_ratio_forces_accounts {d : Nat}
    (h : (206768 : ℚ) / 1000 ≤ (2 : ℚ) ^ (d - 1)) : 9 ≤ d := by
  by_contra hlt; push_neg at hlt; interval_cases d <;> norm_num at h
THEOREM tau_ratio_forces_accounts · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean
tau_ratio_forces_accounts · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean:942 
theorem tau_ratio_forces_accounts {d : Nat}
    (h : (347723 : ℚ) / 100 ≤ (2 : ℚ) ^ (d - 1)) : 13 ≤ d := by
  by_contra hlt; push_neg at hlt; interval_cases d <;> norm_num at h

What this page does not claim

The dimension d of the hypercube is not derived by this module; it remains OPEN. The wall size is an upper bound on what the substrate can support; it does not predict any particular mass value. The module does not establish that d=3 is the legitimate physical dimension for all mass states.

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