CSD

Category: Special (canonical top-level import; explicit module list across LF1 + LF2 + LF3 + Empirical + Mathlib upstream-tracking).

Tests/ is deliberately excluded from this consumer-facing root — build the regression suite separately via lake build CsdLeanTests.

Top-level import file for the Constraint-Surface Dynamics Lean4 project.

This file exports:

• LF1: volume typicality and repeated-trial frequency convergence for deterministic repeated trials.
• LF2: the measure bridge from ontic Liouville volume to projective Fubini–Study measure, and the Born-weight wrapper packaging the finite-dimensional probability assignment under explicit external-theorem inputs.
• LF3: the singlet kernel (1 − st a·b)/4, the operational pointer-sector decomposition (kernel + correlation + marginals + no-signalling + pointer- completeness, with finite-leakage stability), and the LF1↔LF2↔LF3 empirical chain capstone (LF3_singlet_frequency_convergence, LF3_singlet_frequency_convergence_born).
• Empirical: named experimentally-verified predictions — the Bell-family CHSH content (Phase A1–A6) and the no-cloning theorem (Phase B2). The Bell items re-export the LF3 singlet kernel content under empirical-prediction names with experimental provenance; the no-cloning theorem is QM-generic Hilbert-space content.
• Mathlib: project-side patches to Mathlib (currently the Projectivization quotient-topology infrastructure pending upstream).