ParadigmShiftLatticeCert
plain-language theorem explainer
ParadigmShiftLatticeCert packages the cardinalities of five historical paradigm shifts, one future Recognition Science shift, their disjoint union, and the match to the six faces of the recognition cube Q3, plus nonemptiness of the future slot. A researcher applying Recognition Science to the history of science would cite this structure to formalize the 5+1 lattice claim. The definition assembles these properties directly from the inductive enumerations of HistoricalShift and FutureShift together with the constant cubeFaces.
Claim. Let $H$ be the finite set of historical paradigm shifts with elements Copernican, Newtonian, Einsteinian, Quantum, Biological. Let $F$ be the singleton containing the Recognition Science shift. Let $A = H + F$. Then $|H| = 5$, $|F| = 1$, $|A| = 6$, $|A|$ equals the number of faces of the unit cube, and $F$ is nonempty.
background
The module CrossDomain.ParadigmShiftLattice models paradigm shifts as lattice elements whose total count equals the six faces of the recognition cube Q3. HistoricalShift is the inductive type whose five constructors list the completed revolutions. FutureShift is the inductive type whose single constructor reserves the Recognition Science shift. AllParadigmShifts is their disjoint union, whose cardinality is required to equal cubeFaces.
proof idea
As a structure definition with empty proof body, ParadigmShiftLatticeCert simply declares the five required fields. The downstream construction paradigmShiftLatticeCert supplies the concrete values by applying the sibling lemmas historicalCount, futureCount, allShifts_count, shifts_match_cube_faces, and future_slot_realised.
why it matters
This definition certifies the structural claim that five historical shifts plus the RS shift equal the six cube faces, directly supporting the module's wave-62 assertion. It feeds the downstream theorem paradigmShiftLatticeCert. The cube-face match ties to the upstream definition cubeFaces := 6 (twice the spatial dimension D from the forcing chain T8) and to the Freudenthal triangulation's unit-cube count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.