`HistoricalShift`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.ParadigmShiftLattice on GitHub at line 18.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  15
  16namespace IndisputableMonolith.CrossDomain.ParadigmShiftLattice
  17
  18inductive HistoricalShift where
  19  | copernican | newtonian | einsteinian | quantum | biological
  20  deriving DecidableEq, Repr, BEq, Fintype
  21
  22inductive FutureShift where
  23  | recognitionScience
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem historicalCount : Fintype.card HistoricalShift = 5 := by decide
  27theorem futureCount : Fintype.card FutureShift = 1 := by decide
  28
  29abbrev AllParadigmShifts : Type := HistoricalShift ⊕ FutureShift
  30
  31theorem allShifts_count : Fintype.card AllParadigmShifts = 6 := by
  32  simp only [AllParadigmShifts, Fintype.card_sum, historicalCount, futureCount]
  33
  34/-- Six cube faces of Q₃. -/
  35def cubeFaces : ℕ := 6
  36theorem shifts_match_cube_faces : Fintype.card AllParadigmShifts = cubeFaces := by
  37  rw [allShifts_count]; rfl
  38
  39/-- The future slot is non-empty: at least one shift is claimed. -/
  40theorem future_slot_realised : Nonempty FutureShift :=
  41  ⟨FutureShift.recognitionScience⟩
  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

papers checked against this theorem

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