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

papers checked against this theorem

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