historyOfScienceCert
plain-language theorem explainer
The declaration supplies a concrete certificate asserting exactly five scientific paradigm shifts, aligned with the Recognition Science configuration dimension of 5. A sociologist or historian of science working inside the RS framework would cite it to ground the mapping from Kuhnian revolutions to recognition upgrades. The construction is a one-line definition that directly invokes the decidable enumeration of the shifts.
Claim. Let $S$ be the finite type of scientific paradigm shifts. The structure requires that the cardinality of $S$ equals 5. The definition instantiates this structure by setting the cardinality field to the value given by the enumeration theorem.
background
The module treats Kuhn's five canonical paradigm shifts (Copernican, Newtonian, Einsteinian, Quantum, Biological) as the configuration dimension D = 5 in Recognition Science. A paradigm shift is a recognition framework upgrade that occurs when the J-cost exceeds the threshold J(φ), while normal science remains below this threshold. The module imports Mathlib and rests on the structure HistoryOfScienceCert, which encodes the cardinality requirement, together with the upstream theorem that computes this cardinality by exhaustive enumeration.
proof idea
The definition is a one-line wrapper that applies the theorem scientificParadigmShiftCount to populate the five_shifts field of the HistoryOfScienceCert structure.
why it matters
This definition closes the sociological module by supplying an explicit witness for the five-shift count that matches the Recognition Science dimension D = 5. It supports the identification of paradigm shifts with recognition framework restructurings and links to the forcing chain where higher J-threshold capacity appears at specific phi-ladder rungs. No downstream uses are recorded, leaving open whether the certificate will be invoked in larger historical reconstructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.