`face_pairs`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ParticleGenerations
domain: Foundation
line: 31 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ParticleGenerations on GitHub at line 31.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  28
  29/-- Number of pairs of opposite faces on a D-dimensional cube.
  30    For a cube, opposite faces come in pairs: D pairs total. -/
  31def face_pairs (D : ℕ) : ℕ := D
  32
  33/-- For D = 3, there are exactly 3 pairs of opposite faces. -/
  34theorem face_pairs_at_D3 : face_pairs 3 = 3 := rfl
  35
  36/-! ## Three Generations from D=3 -/
  37
  38/-- **P-001 Resolution**: Three generations follow from D = 3.
  39
  40    In the RS framework:
  41    1. DimensionForcing proves D = 3 is the unique spatial dimension
  42       (linking, 8-tick, spinor structure).
  43    2. A D-cube has D pairs of opposite faces.
  44    3. Each face-pair corresponds to one fermion generation in the
  45       ledger's mode-counting (one independent "direction" of
  46       coherence per pair).
  47    4. Thus: 3 generations.
  48
  49    This is not a coincidence — it is forced by the same dimension
  50    argument that gives linking and spinors. -/
  51theorem three_generations_from_dimension :
  52    face_pairs Foundation.DimensionForcing.D_physical = 3 := by
  53  unfold face_pairs Foundation.DimensionForcing.D_physical
  54  rfl
  55
  56/-! ## No Fourth Generation -/
  57
  58/-- For D = 3, there cannot be 4 face-pairs (by definition). -/
  59theorem no_fourth_generation :
  60    face_pairs 3 ≠ 4 := by
  61  norm_num [face_pairs]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.