`five_plus_one_equals_six`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.ParadigmShiftLattice
domain: CrossDomain
line: 45 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.ParadigmShiftLattice on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  42
  43/-- 5 + 1 = 6 = D + 1 (where D = spatial dim 3 has cube Q₃ with 6 faces).
  44    The identity is trivial but the structural match is the content. -/
  45theorem five_plus_one_equals_six : 5 + 1 = cubeFaces := by decide
  46
  47structure ParadigmShiftLatticeCert where
  48  historical_count : Fintype.card HistoricalShift = 5
  49  future_count : Fintype.card FutureShift = 1
  50  total_count : Fintype.card AllParadigmShifts = 6
  51  matches_cube : Fintype.card AllParadigmShifts = cubeFaces
  52  future_realised : Nonempty FutureShift
  53
  54def paradigmShiftLatticeCert : ParadigmShiftLatticeCert where
  55  historical_count := historicalCount
  56  future_count := futureCount
  57  total_count := allShifts_count
  58  matches_cube := shifts_match_cube_faces
  59  future_realised := future_slot_realised
  60
  61end IndisputableMonolith.CrossDomain.ParadigmShiftLattice

papers checked against this theorem

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