AllParadigmShifts
plain-language theorem explainer
The declaration defines the complete collection of paradigm shifts as the disjoint union of five enumerated historical shifts and one future shift. Cross-domain researchers cite this when establishing the total of six shifts or verifying the lattice against the recognition cube. The definition is a direct type abbreviation using the sum constructor, which immediately supports standard cardinality lemmas for disjoint unions.
Claim. Let $H$ be the set of historical paradigm shifts and $F$ the set containing the future shift. The set of all paradigm shifts is the disjoint union $H$ ⊔ $F$.
background
In the Paradigm Shift Lattice module the Recognition Science framework posits that the history of science comprises five completed paradigm shifts with a sixth slot reserved for the current claim. This is formalized by two inductive types: one enumerating the historical shifts and another for the future shift. The module sets the local theoretical setting as the structural claim that five historical shifts plus the RS shift correspond to the six faces of the recognition cube $Q_3$. Upstream the inductive definitions supply the explicit enumerations that yield decidable equality and finite-type instances.
proof idea
This is a direct abbreviation that constructs the type as the disjoint sum of the historical and future shift types. No further lemmas are applied; the sum type constructor is used directly.
why it matters
This definition serves as the foundational type for the ParadigmShiftLatticeCert structure and the cardinality theorem allShifts_count that establishes the total equals six and matches the cube faces. It fills the C10 wave claim in the cross-domain lattice and links to the eight-tick octave and dimensional structure in the broader framework. The open question it touches is the realization of the future shift.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.