Encyclopedia Masses Masses Mass Genesis T10 Hypercube Substrate Substrate Graph Forced By Atomicity

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Hypercube Substrate Substrate Graph Forced By Atomicity

A machine-checked library proves that the ledger of recognition events forces a hypercube graph, and it does not predict which masses exist.

Verify this page

The substrate graph

A hypercube is a graph built from binary strings: each vertex is a sequence of bits, and two vertices are connected when their strings differ in exactly one position. A 3-dimensional hypercube is a cube, with 8 vertices and 12 edges. The framework's machine-checked library of formal theorems proves that the graph of legal recognition events, called the substrate graph, must be a hypercube. The proof starts from ledger atomicity, the rule that each recognition event changes exactly one bit of a pattern, and derives the graph structure rather than assuming it.

The library proves the edge count: a d-dimensional hypercube has d times 2 to the power (d minus 1) undirected edges. It proves that a single vertex has d edges leaving it, and that the largest possible cut, the number of edges crossing a division of vertices into two groups, equals that same total. These are theorems about the hypercube, checked by the machine, with no gaps and no extra axioms beyond the standard logical ones.

In Recognition Science, the framework models particle masses as arising from a ledger, a discrete record of recognition events. The graph result is a structural fact about that ledger. The framework proves the graph is a hypercube, but it does not derive the dimension d. The dimension is left open; the library only proves that if the measured lepton ratios are supported, then d must be at least 13 for the tau and at least 9 for the muon. These are lower bounds from measured values, not predictions of a specific dimension.

The wall, the maximum number of edges crossing a division of the hypercube, is an upper bound on what the substrate can support. It does not say which masses exist. The mass-genesis modules use d equals 3, giving a wall of 12, but whether dimensions above 3 are legitimate in this framework remains an open target. The theorem establishes the graph shape; it does not establish the physics of which masses appear.

What the result changes is the starting point for mass theory: the substrate is not a free choice but a forced structure. A reader can now see that the hypercube is not an assumption but a consequence of atomicity. The open question is which dimension is real, and that question is not settled by this declaration.

THEOREM t10HypercubeSubstrateCert · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean
t10HypercubeSubstrateCert · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean:1031 
theorem t10HypercubeSubstrateCert : T10HypercubeSubstrateCert where
  oneBitDiff_iff_adj := oneBitDiff_iff_hypercubeAdj
  legal_tick_is_hypercube_edge := legalAtomicTick_hypercubeAdj
  post_realizes_flip := post_hypercubeAdj
  bipartite := hypercubeAdj_hammingWeight_parity
  xor_preserves_adj := xorBy_hypercubeAdj
  xor_transitive := xorBy_transitive
  evenClass_attains_maxcut := fun _ hd => hypercubeCut_evenClass hd
  singleton_cut_eq_degree := hypercubeCut_singleton
  connectivity_three := hypercubeEdgeConnectivity_three
  wall_three := hypercube_wall_three_ratio
  muon_forces_d := fun _ h => muon_ratio_forces_accounts h
  tau_forces_d := fun _ h => tau_ratio_forces_accounts h
  muon_forces_cells := fun _ h => muon_ratio_forces_three_cells h
  tau_forces_cells := fun _ h => tau_ratio_forces_five_cells h
  posting_witness := posting_realizes_named_hypercube_edge
  scope_does_not_derive_d := trivial
  scope_wall_is_capacity_not_prediction := trivial
  scope_d_gt_three_is_open := trivial
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_le_total · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean
hypercubeCut_le_total · IndisputableMonolith/Masses/MassGenesis/T10HypercubeSubstrate.lean:414 
/-- H5 ceiling. -/
theorem hypercubeCut_le_total {d : Nat} (A : Finset (Pattern d)) :
    hypercubeCut A ≤ d * 2 ^ (d - 1) := by
  classical
  cases d with
  | zero =>
      have hz : hypercubeCut A = 0 := by
        unfold hypercubeCut
        refine Finset.card_eq_zero.mpr ?_
        ext e
        simp only [Finset.notMem_empty, iff_false, Finset.mem_filter,
          Finset.mem_univ, true_and, HypercubeAdj]
        intro h
        -- no edges when there are no coordinates
        have : (Finset.univ : Finset (Fin 0)).card = 0 := by simp
        have hle := Finset.card_filter_le
          (s := (Finset.univ : Finset (Fin 0)))
          (p := fun i => e.1 i ≠ e.2 i)
        omega
      simp [hz]
  | succ d' =>
    have hdir := card_directedHypercubeEdges (d' + 1)
    -- cut A ≤ half of directed edges via cut A = cut Aᶜ
    let Cut := Finset.univ.filter fun e : Pattern (d'+1) × Pattern (d'+1) =>
      HypercubeAdj e.1 e.2 ∧ e.1 ∈ A ∧ e.2 ∉ A
    let Cut' := Finset.univ.filter fun e : Pattern (d'+1) × Pattern (d'+1) =>
      HypercubeAdj e.1 e.2 ∧ e.1 ∉ A ∧ e.2 ∈ A
    let swapE := fun e : Pattern (d'+1) × Pattern (d'+1) => (e.2, e.1)
    have himage : Cut.image swapE = Cut' := by
      ext e
      constructor
      · intro he
        rcases Finset.mem_image.mp he with ⟨e', he', rfl⟩
        rcases Finset.mem_filter.mp he' with ⟨_, hadj, hA, hnA⟩
        exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, hypercubeAdj_symm hadj, hnA, hA⟩
      · intro he
        rcases Finset.mem_filter.mp he with ⟨_, hadj, hnA, hA⟩
        exact Finset.mem_image.mpr
          ⟨(e.2, e.1),
            Finset.mem_filter.mpr ⟨Finset.mem_univ _, hypercubeAdj_symm hadj, hA, hnA⟩, rfl⟩
    have hinj : Set.InjOn swapE Cut := by
      intro x _ y _ h; exact Prod.ext (Prod.mk.inj h).2 (Prod.mk.inj h).1
    have hcuts : Cut.card = Cut'.card := by
      have := congrArg Finset.card himage
      rwa [Finset.card_image_of_injOn hinj] at this
    have hdisj : Disjoint Cut Cut' := by
      refine Finset.disjoint_left.mpr ?_
      intro e he1 he2
      exact (Finset.mem_filter.mp he2).2.2.1 (Finset.mem_filter.mp he1).2.2.1
    have hsub : Cut ∪ Cut' ⊆ directedHypercubeEdges (d'+1) := by
      intro e he
      simp only [Finset.mem_union, Cut, Cut', Finset.mem_filter,
        directedHypercubeEdges] at he ⊢
      rcases he with ⟨_, hadj, _, _⟩ | ⟨_, hadj, _, _⟩ <;>
        exact ⟨Finset.mem_univ _, hadj⟩
    have hle : 2 * Cut.card ≤ (directedHypercubeEdges (d'+1)).card := by
      have := Finset.card_le_card hsub
      have hu := Finset.card_union_of_disjoint hdisj
      have : Cut.card + Cut'.card ≤ (directedHypercubeEdges (d'+1)).card := by
        simpa [hu] using this
      simpa [two_mul, hcuts] using this
    have : Cut.card ≤ (d'+1) * 2 ^ d' := by
      have h2 : 2 * Cut.card ≤ (d'+1) * 2 ^ (d'+1) := by simpa [hdir] using hle
      have hpow : (d'+1) * 2 ^ (d'+1) = 2 * ((d'+1) * 2 ^ d') := by
        rw [pow_succ]; ring
      have h2' : 2 * Cut.card ≤ 2 * ((d'+1) * 2 ^ d') := by simpa [hpow] using h2
      exact Nat.le_of_mul_le_mul_left h2' (by decide : 0 < 2)
    simpa [hypercubeCut, Cut] using this
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 declaration does not claim that any particular mass exists. The declaration does not claim that d equals 3 is the physically correct dimension. The declaration does not claim that the substrate graph is the only structure in mass genesis.

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