Encyclopedia Masses Masses Sector Dependent Torsion

ARTICLE 5 claims 4 theorems 1 hypothesis

Masses Sector Dependent Torsion

The integers 13, 11, 6, and 8 appear as cell counts on a cube, and a machine-checked library proves they form a unique chain that maps onto particle generations.

Verify this page

Sector-dependent generation torsion

In the Recognition Science framework, recognition (a discrete ledger of events) forces a small set of integers to appear as cell counts on a cube. For a cube in three dimensions, the counts are 8 vertices, 12 edges, 6 faces, and 1 body. The module SectorDependentTorsion studies the four integers 13, 11, 6, and 8, which arise as sums of these cube counts: 13 = 8 + 6 − 1, 11 = 6 + 6 − 1, 6 = 6, and 8 = 8. The framework's machine-checked library of formal theorems proves that these four integers, taken in the order [13, 11, 6, 8], satisfy a unique algebraic chain: the adjacent sums (13+11, 11+6, 6+8) partition the number 55, and no other ordering of the four integers meets the same constraints.

The chain's significance is that the framework models particle generations as steps along this chain. The lepton sector is assigned the pair {11, 6}, and that assignment is derived from the framework's forcing argument. The up-quark pair {13, 11} and the down-quark pair {6, 8} are hypotheses supported by particle-data tables, not derived from first principles. The module proves the mathematical properties of these integers, but it does not prove why each physical sector uses its particular pair.

A later closure derivation removes the last unforced step. The framework's recognition orbit is a 1-cycle, so closed loops live at loop dimension 1. Only the vertex coupling dimension 0 lies below that, so it must borrow its dual face, producing the excess V + F − C = 13 − 11 = 2. The threshold sits at the self-dual fixed point 1 = 2 − 1, which makes the rule duality-breaking yet not free. Once the loop dimension is fixed, the generation ladder is forced; only the ℤ/2 name "up" versus "down" remains conventional.

The module also derives a dimension-forcing condition: the relation W = 2V + 1 = N₀ holds only for D = 3, where V = 8 and N₀ = 17. This is a genuine derivation with no data used, and it provides a new condition that forces three spatial dimensions.

THEOREM sector_chain_assignment_forced · forced_chain_windows · IndisputableMonolith/Masses/SectorDependentTorsion.lean
sector_chain_assignment_forced · IndisputableMonolith/Masses/SectorDependentTorsion.lean:360 
/-- **THEOREM (assignment forcing).** Any ordering `[a,b,c,d]` of the four cube
step values `{13,11,6,8}` whose three generation spans `a+b, b+c, c+d` partition
`N₃ = 55` and are pairwise distinct equals the chain `[13,11,6,8]` or its reverse
`[8,6,11,13]`. So the sector→window assignment (up `={13,11}`, lepton `={11,6}`,
down `={6,8}`) is forced by the (derived) N₃ partition plus distinct spans — not
freely fitted to data. Kernel axioms only (no `native_decide`). -/
theorem sector_chain_assignment_forced
    (a b c d : ℕ)
    (hperm : List.Perm [a, b, c, d] [13, 11, 6, 8])
    (hpart : (a + b) + (b + c) + (c + d) = 55)
    (hab_bc : a + b ≠ b + c)
    (hbc_cd : b + c ≠ c + d)
    (hab_cd : a + b ≠ c + d) :
    [a, b, c, d] = [13, 11, 6, 8] ∨ [a, b, c, d] = [8, 6, 11, 13] := by
  have hsum := hperm.sum_eq
  simp only [List.sum_cons, List.sum_nil] at hsum
  have ha : a = 13 ∨ a = 11 ∨ a = 6 ∨ a = 8 := by
    have hmem : a ∈ [13, 11, 6, 8] := (hperm.mem_iff).mp (by simp)
    simpa using hmem
  have hb : b = 13 ∨ b = 11 ∨ b = 6 ∨ b = 8 := by
    have hmem : b ∈ [13, 11, 6, 8] := (hperm.mem_iff).mp (by simp)
    simpa using hmem
  have hc : c = 13 ∨ c = 11 ∨ c = 6 ∨ c = 8 := by
    have hmem : c ∈ [13, 11, 6, 8] := (hperm.mem_iff).mp (by simp)
    simpa using hmem
  have hd : d = 13 ∨ d = 11 ∨ d = 6 ∨ d = 8 := by
    have hmem : d ∈ [13, 11, 6, 8] := (hperm.mem_iff).mp (by simp)
    simpa using hmem
  rcases ha with rfl | rfl | rfl | rfl <;>
    rcases hb with rfl | rfl | rfl | rfl <;>
      rcases hc with rfl | rfl | rfl | rfl <;>
        rcases hd with rfl | rfl | rfl | rfl <;>
          first
            | (left; rfl)
            | (right; rfl)
            | omega
forced_chain_windows · IndisputableMonolith/Masses/SectorDependentTorsion.lean:397 
/-- The forced chain's three windows are exactly the up / lepton / down sector
step-pairs. Reads the chain `[13,11,6,8]` off as (up, lepton, down). Kernel
axioms only. -/
theorem forced_chain_windows :
    (13, 11) = (up_step_12, up_step_23) ∧
      (11, 6) = (lepton_step_12, lepton_step_23) ∧
      (6, 8) = (down_step_12, down_step_23) := by
  refine ⟨?_, ?_, ?_⟩ <;> (apply Prod.ext <;> decide)
THEOREM forced_chain_windows · IndisputableMonolith/Masses/SectorDependentTorsion.lean
forced_chain_windows · IndisputableMonolith/Masses/SectorDependentTorsion.lean:397 
/-- The forced chain's three windows are exactly the up / lepton / down sector
step-pairs. Reads the chain `[13,11,6,8]` off as (up, lepton, down). Kernel
axioms only. -/
theorem forced_chain_windows :
    (13, 11) = (up_step_12, up_step_23) ∧
      (11, 6) = (lepton_step_12, lepton_step_23) ∧
      (6, 8) = (down_step_12, down_step_23) := by
  refine ⟨?_, ?_, ?_⟩ <;> (apply Prod.ext <;> decide)
HYPOTHESIS forced_chain_windows · IndisputableMonolith/Masses/SectorDependentTorsion.lean
forced_chain_windows · IndisputableMonolith/Masses/SectorDependentTorsion.lean:397 
/-- The forced chain's three windows are exactly the up / lepton / down sector
step-pairs. Reads the chain `[13,11,6,8]` off as (up, lepton, down). Kernel
axioms only. -/
theorem forced_chain_windows :
    (13, 11) = (up_step_12, up_step_23) ∧
      (11, 6) = (lepton_step_12, lepton_step_23) ∧
      (6, 8) = (down_step_12, down_step_23) := by
  refine ⟨?_, ?_, ?_⟩ <;> (apply Prod.ext <;> decide)
THEOREM N0_at_D3 · IndisputableMonolith/Masses/SectorDependentTorsion.lean
N0_at_D3 · IndisputableMonolith/Masses/SectorDependentTorsion.lean:98 
theorem N0_at_D3 : N0 3 = 17 := by native_decide
THEOREM generationLadderClosureForcedCert · IndisputableMonolith/Masses/SectorDependentTorsion.lean
generationLadderClosureForcedCert · IndisputableMonolith/Masses/SectorDependentTorsion.lean:906 
/-- The refined closure certificate holds: the generation step ladder is forced by the closure
principle plus the structural 1-cycle dimension of the recognition orbit. Kernel axioms only. -/
def generationLadderClosureForcedCert : GenerationLadderClosureForcedCert where
  ladder_from_closure := generation_ladder_from_closure
  leading_reproduced := closureLeadingStep_reproduces_leading
  excess_is_borrow := up_excess_is_loop_hosting_borrow
  breaks_duality_as_required := (closureLeadingStep_breaks_duality_as_required).1
  threshold_self_dual := loopDimension_self_dual

What this page does not claim

The module does not derive the physical assignment of quark sectors from first principles. The framework does not claim that the integers 13, 11, 6, 8 are the only possible cell counts in all dimensions. The closure derivation does not remove the conventional ℤ/2 label of up versus down.

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