pith. machine review for the scientific record. sign in
theorem proved term proof high

face_pairs_at_D3

show as:
view Lean formalization →

The result shows that a cube in three dimensions has exactly three pairs of opposite faces. This grounds the three fermion generations in Recognition Science via the forced spatial dimension. The proof is immediate by reflexivity from the definition of the face-pair count.

claimA cube in three spatial dimensions possesses exactly three pairs of opposite faces.

background

The ParticleGenerations module formalizes P-001 on three fermion generations. It starts from the dimension-forcing result that spatial dimensions equal three and considers the geometry of a three-dimensional cube. Each pair of opposite faces maps to one independent coherence mode in the ledger structure, producing three generations total.

proof idea

The proof is a one-line term wrapper that applies reflexivity. It reduces directly to the definitional equality that the face-pair count equals the dimension value when the argument is three.

why it matters in Recognition Science

This declaration completes the P-001 resolution by confirming the face-pair count for D=3. It connects to the framework landmark that D=3 is forced by the eight-tick octave and linking structure, yielding the unique three-generation outcome. The module notes that this count distinguishes the framework from two or four generations; downstream siblings such as three_generations_from_dimension and no_fourth_generation build on the same geometric step.

scope and limits

formal statement (Lean)

  34theorem face_pairs_at_D3 : face_pairs 3 = 3 := rfl

proof body

Term-mode proof.

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

depends on (29)

Lean names referenced from this declaration's body.