historicalCount
The theorem states that the inductive type enumerating completed paradigm shifts in science has cardinality exactly five. Lattice modelers cite this count to fix the historical base before adjoining the reserved sixth slot for the Recognition Science shift. The proof is a one-line decision procedure that computes the cardinality of the finite inductive type directly.
claimLet $H$ be the inductive type whose constructors are the Copernican, Newtonian, Einsteinian, Quantum, and Biological shifts. Then $|H| = 5$.
background
The module establishes a structural claim for the paradigm shift lattice: history contains five completed shifts, with the sixth slot reserved, so that five historical shifts plus the RS shift match the six faces of the recognition cube $Q_3$. HistoricalShift is the inductive type whose five constructors are copernican, newtonian, einsteinian, quantum, and biological, equipped with DecidableEq, Repr, BEq, and Fintype instances. The upstream result is precisely this inductive definition, which supplies the finite set whose cardinality is asserted.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic evaluates the Fintype.card computation on the inductive type with exactly five constructors and confirms the equality holds by exhaustive enumeration.
why it matters in Recognition Science
The result is invoked by allShifts_count to obtain the total cardinality six via Fintype.card_sum and by paradigmShiftLatticeCert to populate the historical_count field of the lattice certificate. It thereby realizes the five-plus-one-equals-six relation for the cube faces of $Q_3$ inside the Recognition Science framework. No open scaffolding remains; the declaration is fully proved.
scope and limits
- Does not enumerate shifts outside the five listed constructors.
- Does not prove existence or properties of the sixth future shift.
- Does not derive the shifts from the J-function or forcing chain.
- Does not address whether additional shifts could be added to the type.
Lean usage
theorem total_six : Fintype.card AllParadigmShifts = 6 := by simp only [AllParadigmShifts, Fintype.card_sum, historicalCount, futureCount]formal statement (Lean)
26theorem historicalCount : Fintype.card HistoricalShift = 5 := by decide