module module

`IndisputableMonolith.CrossDomain.ParadigmShiftLattice`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

declarations in this module (12)

inductive HistoricalShift L18
inductive FutureShift L22
theorem historicalCount L26
theorem futureCount L27
abbrev AllParadigmShifts L29
theorem allShifts_count L31
def cubeFaces L35
theorem shifts_match_cube_faces L36
theorem future_slot_realised L40
theorem five_plus_one_equals_six L45
structure ParadigmShiftLatticeCert L47
def paradigmShiftLatticeCert L54