HistoricalShift
plain-language theorem explainer
The inductive type enumerates the five completed paradigm shifts in the history of science as Copernican, Newtonian, Einsteinian, quantum, and biological. Researchers formalizing the paradigm shift lattice or certifying its cube-face cardinality would cite this enumeration. The definition proceeds by direct listing of the five constructors together with automatic derivation of Fintype for downstream cardinality theorems.
Claim. Let $H$ be the inductive type whose constructors are the Copernican, Newtonian, Einsteinian, quantum, and biological paradigm shifts.
background
The CrossDomain.ParadigmShiftLattice module presents a structural claim that the history of science consists of five completed paradigm shifts plus one reserved slot, yielding six elements to match the faces of the recognition cube $Q_3$. HistoricalShift supplies the inductive type for the five past shifts. This type is combined via disjoint union with FutureShift to obtain AllParadigmShifts, whose cardinality is later shown to equal both 6 and cubeFaces.
proof idea
The declaration is a direct inductive definition that introduces exactly five constructors and derives DecidableEq, Repr, BEq, and Fintype in a single line.
why it matters
This definition supplies the historical component required by AllParadigmShifts, historicalCount (which establishes cardinality 5), and ParadigmShiftLatticeCert (which verifies that the total of six shifts matches cubeFaces and that the future slot is nonempty). It realizes the module claim that five historical shifts plus the RS shift correspond to the six faces of the recognition cube, consistent with the framework's use of discrete lattice structures to encode paradigm transitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.