Series-Parallel formalization v1.0.3

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.

Series-Parallel formalization v1.0.2

Frozen Lean 4 formalization archive for Distance and resistance on random series-parallel graphs.

• Release tree: exactly 94 tracked paths, including 79 Lean source files.
• Unique manuscript source: Distance_and_resistance_arxiv_amsart.tex.
• Lean 4.32.1; Lake 5.0.0; mathlib v4.32.1 at 520045ab14e26149ee970e2e617ca04b09bde5d6.
• License: Apache-2.0.
• Verification: the complete Lean build passed (8,733 jobs); placeholder, project-axiom, graph-semantics, and source-map audits passed.
• Declared project axioms: distanceGamma_half_eq_zero and MI01_global_peano_on_compact_interval.

The repository is private and no DOI has been assigned.

Lean formalization v1.0.1

Frozen Lean 4 formalization with traditional finite-multigraph distance and Thomson-resistance semantics, samplewise bridges, graph-facing versions of the three principal theorems, exact source maps, and publication audit reports.

• Commit: a661859
• Lean: 4.32.1
• Lake: 5.0.0
• mathlib: v4.32.1 at 520045ab14e26149ee970e2e617ca04b09bde5d6
• Full lake build: 8,733 jobs
• Placeholder audit: 80 Lean files, exactly 2 documented project axioms
• License: Apache-2.0

Lean formalization v1.0.0

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.

SPA submission package v1.0.0

SPA/CAS 2.4 submission package containing the 35-page blue-marked and clean TeX/PDF manuscripts, the detailed manuscript audit report, the revision report, highlights, exact source maps, and the proposition-by-proposition manuscript-Lean correspondence.

• Commit: baf5cb1
• Formalization release: v1.0.1
• Repository access: private/access-controlled
• DOI: not assigned