Skip to content

Series-Parallel formalization v1.0.3

Latest

Choose a tag to compare

@iyalice iyalice released this 20 Sep 17:17

Verified Lean 4 formalization and manuscript/report update for Distance and resistance on random series-parallel graphs: logarithmic speeds and near-critical asymptotics.

  • Sole reference manuscript: SeriesParallel.tex, retaining the author's AI contribution and Lean declarations and omitting code availability.
  • Updated source map: 137 active labels and 29 numbered theorem/proposition/lemma results. Theorem 1.3 is explicitly documented as joint coverage by the near-critical theorem and the admissible-halfline identity.
  • All 80 project Lean files are unchanged from the previously audited proof sources. The two documented external mathematical inputs and auxiliary-coverage qualifications remain explicit.
  • Fresh release checks: lake build passed (8,733 jobs); reference LaTeX compilation, manuscript correspondence, lexical audit, and fingerprint checks passed. Existing axiom outputs were reused only after checking all Lean source hashes against the audited sources.
  • Environment: Lean 4.32.1, Lake 5.0.0, mathlib v4.32.1 at 520045ab14e26149ee970e2e617ca04b09bde5d6.
  • Reference manuscript SHA-256 (UTF-8, LF): a5034c47dea2bbe6d47af58dea3154ea9a74db5d165bbd695d6f6fcd5955b677.
  • Public source distribution under Apache-2.0. Package and citation versions are 1.0.3.

Release verification and reproduction instructions.

This release supersedes v1.0.2 for the current manuscript and correspondence tables. The earlier tags and verification records remain unchanged.