shifts_match_cube_faces
plain-language theorem explainer
The cardinality of the disjoint union of historical and future paradigm shifts equals the face count of the recognition cube. Cross-domain lattice work cites this to close the five-plus-one structural match. The proof rewrites via the all-shifts count theorem and finishes by reflexivity.
Claim. Let $A$ denote the disjoint union of the set of historical paradigm shifts and the set of future paradigm shifts. Then the cardinality of $A$ equals 6, where 6 is the number of faces of the unit cube $Q_3$.
background
The Paradigm Shift Lattice module defines AllParadigmShifts as the disjoint union HistoricalShift ⊕ FutureShift. cubeFaces is the constant 6, obtained as twice the spatial dimension D from the forcing chain T8. The module states that five completed historical shifts plus one reserved RS shift total six to match the faces of Q₃.
proof idea
One-line wrapper that rewrites the left-hand side by the allShifts_count theorem, which itself expands the sum cardinality via historicalCount and futureCount, then closes by reflexivity against the local cubeFaces definition.
why it matters
This supplies the matches_cube field inside the ParadigmShiftLatticeCert record. It realizes the C10 claim that five historical shifts plus the RS shift equal the six faces of Q₃. The result sits downstream of the cardinality spectrum and Freudenthal triangulation cubeFaces definitions and feeds the lattice certificate used for cross-domain verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.