Featured Dataset
Lean 4 Formalized Proof Artifacts for Local Softmax and Global Weights in Non-Boolean Event Structures
This supplement records the Lean 4 formalization used to verify the finite claims about gluing, generalized-softmax coordinates, and the pentagon half-weight. The project was checked with Lean v4.30.0 and mathlib v4.30
File Size7.7 KB
Data TypeDataset
Published2026
Licensecc-by-4.0
Total Views25
Total Downloads2
This supplement records the Lean 4 formalization used to verify the finite claims about gluing, generalized-softmax coordinates, and the pentagon half-weight. The project was checked with Lean v4.30.0 and mathlib v4.30.0; the command
lake build completed successfully, and the source contains no sorry, admit, or axiom.The formalization separates three layers:
- First (Core.lean) defines finite event structures, admissible weights, positive coordinates, and the representation theorem for scaled link-function preimages.
- Second (Gluing.lean) formalizes local context-wise distributions, single-valuedness, the normalizer-ratio calculation, and the theorem that single-valued local distributions glue to a global admissible weight.
- Third (Pentagon.lean) formalizes the pentagon example: the half-weight is admissible, every two-valued state and every finite classical mixture obeys the cyclic bound 2, the half-weight has cyclic sum 5/2, and 5/2 > √5. The same file also verifies the positive softmax-coordinate path and its boundary endpoint at the half-weight.
📤 Share this page
Found this useful? Share it with your network.
Files are hosted on the source repository. Click download to access the full dataset.
Svozil, Karl (2026). Lean 4 Formalized Proof Artifacts for Local Softmax and Global Weights in Non-Boolean Event Structures. https://doi.org/10.5281/zenodo.20479152