allShifts_count
plain-language theorem explainer
allShifts_count establishes that the set of all paradigm shifts has cardinality six by combining five historical shifts with one future shift. Workers on the cross-domain lattice cite it to confirm the six-face cube geometry. The proof proceeds by a direct simplification that invokes the sum cardinality rule on the disjoint union together with the separate historical and future counts.
Claim. $ |AllParadigmShifts| = 6 $ where $AllParadigmShifts := HistoricalShift ⊔ FutureShift$.
background
The Paradigm Shift Lattice module formalizes the claim that the history of science comprises five completed paradigm shifts together with one reserved slot for the Recognition Science shift. These are collected into the type AllParadigmShifts defined as the disjoint union HistoricalShift ⊕ FutureShift. The module states that this total must equal the number of faces on the recognition cube Q₃.
proof idea
The proof applies the simp tactic to expand AllParadigmShifts as the sum type and then uses the Fintype.card_sum lemma along with the values supplied by historicalCount and futureCount.
why it matters
It provides the total_count field inside the ParadigmShiftLatticeCert definition and is invoked by the shifts_match_cube_faces theorem to equate the shift count with the cube face count. The result realizes the module's 5 + 1 = 6 claim, anchoring the lattice to the three-dimensional cube geometry that arises from the forcing chain. No open questions remain at this counting level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.