Skip to content

Lean formalization v1.0.0

Choose a tag to compare

View all tags
@iyalice iyalice released this 29 Aug 15:06
v1.0.0
fa2fc71

Frozen Lean 4 formalization accompanying 'Distance and resistance on random series-parallel graphs'.

Verified with Lean 4.32.1, Lake 5.0.0, and mathlib v4.32.1 at commit 520045ab14e26149ee970e2e617ca04b09bde5d6. The full build succeeds (8,733 jobs). The traditional distance and Kirchhoff-Thomson resistance bridges add no project axioms; the two documented external mathematical interfaces and exact theorem fingerprints are recorded in AXIOM_REPORT.md and SEMANTIC_BRIDGE_REPORT.md.

License: Apache-2.0.

Assets 2
Loading