All-graph Laplacian strong Chollet — complete Lean formalization (v2)

This version supplies the complete Lean formalization of the all-graph Laplacian strong Chollet theorem released in mathematical v1, together with a fresh independent compilation and empty-kernel replay.

For every finite simple unweighted graph G and every vertex subset S, let A be the principal submatrix of the real graph Laplacian on S. The formal theorem proves per(A ∘ A) ≤ per(A) · ∏_{v∈S} degree_G(v), with degrees taken in the original graph. It includes empty subsets, isolated vertices, disconnected graphs and singular Laplacians. The accompanying theorem covers the full graph Laplacian plus any entrywise nonnegative real diagonal addition.

• Main theorem: Chollet.strongChollet_all_graphs.
• Diagonal addition: Chollet.laplacianDiagonalStrong_all.
• Frozen PR #10 head: 4d2eefd40ee930216ccd8fc0f51e4bf694251967.
• Release/tag source: merge commit 7b7ac8da240aba15fb4af5d7d37c97458057e07e.
• Exact package: formalizations/laplacian-chollet-all-graphs-progress/, 124 files, including 83 fresh proof modules. All package blobs equal the frozen head; files outside the package equal the merge first parent.

Independent verification completed on 2026-10-09 with the pinned Lean 4.34.1 toolchain and nine pinned dependencies: all 83 modules compiled; all 168 recorded commands exited successfully; all 985 owned declarations and their 44,173-declaration dependency closure replayed in an initially empty kernel at trust level zero. The main theorem closure has 42,988 declarations. The only axioms are the three pinned standard axioms propext, Classical.choice and Quot.sound; an invalid proof of False was rejected by the negative kernel control. A separately compiled literal interface check confirms the original-degree principal-submatrix statement and the nonnegative diagonal extension. Dependency-cache fingerprints were unchanged during the replay.

The independent replay archive contains the fresh sources, complete command logs, declaration inventory, dependency closure, kernel audit, standard-axiom signatures, negative control and literal semantic check. The source archive retains the complete reproduction driver, pinned configuration, written proof, provenance records and licenses, including the attributed OpenAI PerfectMatching components and their Apache 2.0 license. Thirty-eight pinned upstream source files were independently checked.

Five assets:

• laplacian-chollet-general-v2-lean-source.tar.gz
• laplacian-chollet-general-v2-lean-independent-replay.tar.gz
• replay-summary.json
• RELEASE_BINDING.json
• SHA256SUMS_ASSETS

RELEASE_BINDING.json binds the exact source commits, source-package checksums, toolchain, dependencies and asset hashes. SHA256SUMS_ASSETS covers the other four assets. Extract the source archive and follow its README and reproduce.py instructions to reproduce the checks.

GitHub Actions had no runs, checks or commit statuses for the frozen head or merge commit at the post-merge check; no CI pass is claimed. This release records independent source, semantic-interface and kernel verification, without an external human peer-review certificate or a global priority claim.