Popular repositories Loading

1. csd-lean4 csd-lean4 Public

   Lean 4 formalisation of a deterministic reconstruction of finite-dimensional quantum mechanics: the Born rule as a Liouville volume ratio

   Lean 6

2. gleason-finite-lean gleason-finite-lean Public

   Gleason's theorem in finite dimensions, machine-checked in Lean 4 (Palomar layout)

   Lean 2 1

3. fc-poisson-2 fc-poisson-2 Public

   Lean 4 proof that the Poisson conjecture fails for two canonical pairs and every n >= 2, against Formal Conjectures' math/0608009 statements, following C. D. Long (2026)

   Lean 2 1

4. lie-trotter-lean lie-trotter-lean Public

   Lean 4 proof of the Lie-Trotter product formula in a Banach algebra with a commutator-scaling error bound, laid out for the Palomar registry

   Lean 2 1

5. csd-lean4-docs csd-lean4-docs Public

   Builds and publishes the csd-lean4 API documentation to docs.constraintsurfacedynamics.com. Mathlib's mathlib4_docs pattern; no built output committed.

   1

6. csd-qit-bridge csd-qit-bridge Public

   physlib's unconditional strong subadditivity and relative-entropy data processing, read in csd-lean4's vocabulary; both libraries pinned by revision

   Lean 1