Skip to main content
TheoremPath

FormalSLT public status

Public v0.3 proof surface is green on main.

This legacy route has been refreshed from the old v0.1 snapshot to the current v0.3 proof surface: sharp McDiarmid, a two-sided iid product theorem, downstream constant propagation, and a finite PAC-Bayes Bernstein margin shell, all tied to public PR #6 and the public README.

Public FormalSLT repoVille boundary context

public main green

Public sharp additive McDiarmid specialization

The public repository checks `mcdiarmid_additive_independent`, with the sharp exponent written in the Lean type itself.

FormalSLT/Concentration/SharpMcDiarmid.lean:244

public main green

Two-sided iid product theorem

PR #6 adds `mcdiarmid_twoSided_of_hasBoundedDifferences_sharp` over a homogeneous product measure.

FormalSLT/Concentration/SharpMcDiarmid.lean:171

public main green

PAC-Bayes Bernstein margin shell

PR #6 adds `finitePACBayesBernsteinMargin_badEventMass_le_delta` with supplied variance-proxy and prior-moment certificates.

FormalSLT/PACBayesBernstein.lean:521

adjacent checked result

Ville inequality boundary

Ville's inequality is checked in the related Pythia and martingale work, not inside FormalSLT itself. This page keeps that boundary explicit while showing why FormalSLT connects naturally to anytime-valid statistics.

related theorem page

proof evidence

Each headline claim now points to a theorem name and source path.

The public CI badge verifies the FormalSLT repository. The same public main build now covers the two-sided product theorem and the finite PAC-Bayes Bernstein supplied-proxy shell.

The axiom profile below follows the public README target: propext, Classical.choice, and Quot.sound.

Signature excerpts show the theorem head and bound shape. The listed source path is the full hypothesis record.

Sharp additive independent McDiarmid

public main CI green at 108a1394c25172e12584e14c54d68768a82e43db
declaration
FormalSLT.Concentration.mcdiarmid_additive_independent
confidence
high for the public theorem
axiom trace
#print axioms reports [propext, Classical.choice, Quot.sound] for this theorem.
challenge tested
Tested against overclaim: the block says this is additive independent only, not the full two-sided arbitrary bounded-differences theorem.
source
FormalSLT/Concentration/SharpMcDiarmid.lean:244
signature excerpt
theorem mcdiarmid_additive_independent ... :
  μ.real {ω | t ≤ ∑ i ∈ s, (X i ω - ∫ x, X i x ∂μ)}
    ≤ Real.exp (-2 * t ^ 2 / ∑ i ∈ s, (b i - a i) ^ 2)
does not claim
This public theorem is the additive independent specialization, not the full two-sided arbitrary bounded-differences theorem.
retraction condition
Retract if public CI fails, the theorem signature changes, or a later axiom trace adds a nonstandard dependency.

Two-sided product McDiarmid

public main CI green at 108a1394c25172e12584e14c54d68768a82e43db
declaration
FormalSLT.Concentration.mcdiarmid_twoSided_of_hasBoundedDifferences_sharp
confidence
high for the public theorem
axiom trace
#print axioms reports [propext, Classical.choice, Quot.sound] for this theorem.
challenge tested
Tested against scope overclaim: the block says homogeneous product measure, not arbitrary non-iid product spaces.
source
FormalSLT/Concentration/SharpMcDiarmid.lean:171
signature excerpt
theorem mcdiarmid_twoSided_of_hasBoundedDifferences_sharp ... :
  (Measure.pi (fun _ : Fin n => μ)).real
    {S | ε ≤ |f S - ∫ s, f s ∂(Measure.pi (fun _ : Fin n => μ))|}
    ≤ 2 * Real.exp (-2 * ε ^ 2 / ∑ k : Fin n, (c k) ^ 2)
does not claim
This theorem is not stated for arbitrary non-iid product spaces.
retraction condition
Retract if public CI fails, the theorem signature changes, or a later axiom trace adds a nonstandard dependency.

Downstream sharp constant propagation

public main CI green at 108a1394c25172e12584e14c54d68768a82e43db
declaration
FormalSLT.AlgorithmicStability.bousquet_elisseeff_centered_tail
confidence
high for the public theorem
axiom trace
#print axioms reports [propext, Classical.choice, Quot.sound] for this theorem.
challenge tested
Tested against PR-title-only evidence: the block quotes the downstream stability theorem signature carrying the sharp exponent.
source
FormalSLT/Stability/BousquetElisseeff.lean:144
signature excerpt
theorem bousquet_elisseeff_centered_tail ... :
  (Measure.pi (fun _ : Fin n => μ)).real
    {S | ∫ s, (∫ z, ℓ (A s) z ∂μ - trainingLoss A ℓ s) ∂(Measure.pi (fun _ : Fin n => μ)) + ε
      ≤ ∫ z, ℓ (A S) z ∂μ - trainingLoss A ℓ S}
    ≤ Real.exp (-2 * ε ^ 2 / ((n : ℝ) * (2 * β + 2 * B / n) ^ 2))
does not claim
This does not claim the localized-Rademacher wrapper has moved off the older Azuma constant.
retraction condition
Retract if public CI fails, the sharp constant is not preserved in public source, or a later axiom trace adds a nonstandard dependency.

PAC-Bayes Bernstein margin shell

public main CI green at 108a1394c25172e12584e14c54d68768a82e43db
declaration
FormalSLT.PACBayesBernstein.finitePACBayesBernsteinMargin_badEventMass_le_delta
confidence
high for the public supplied-proxy shell
axiom trace
#print axioms reports [propext, Classical.choice, Quot.sound] for this theorem.
challenge tested
Tested against certificate overclaim: the block states supplied certificates are assumed and concrete classifier extraction is outside scope.
source
FormalSLT/PACBayesBernstein.lean:521
signature excerpt
theorem finitePACBayesBernsteinMargin_badEventMass_le_delta ... :
  (∑ ω ∈ finitePACBayesBernsteinPenaltyBadSamples ..., ν ω) ≤ delta
does not claim
The shell does not prove that concrete classifier-margin certificates are obtainable.
retraction condition
Retract if certificate assumptions change, public source drops the file, or a later axiom trace adds a nonstandard dependency.

Ville inequality boundary

adjacent checked theorem family
declaration
FormalMartingales.ville_inequality
confidence
high for the adjacent formal-martingales theorem
axiom trace
#print axioms reports [propext, Classical.choice, Quot.sound] for this theorem.
challenge tested
Tested against repo-boundary overclaim: this is not a FormalSLT theorem and is presented only as the anytime-valid bridge.
source
Adjacent repo: formal-martingales/FormalMartingales/Martingale/Ville.lean:264
signature excerpt
theorem ville_inequality ... :
  ε * μ {ω | ∃ n : ℕ, (ε : ℝ) ≤ f n ω} ≤ ENNReal.ofReal (μ[f 0])
does not claim
This page does not claim Ville's inequality is inside FormalSLT.
retraction condition
Retract if the adjacent formal-martingales theorem changes, fails to build, or its axiom trace adds a nonstandard dependency.

theorem chain

The diagram now starts from proof outcomes, not repo size.

The SVG is copied from `docs/theorem-chain.svg` in the current public FormalSLT repository and served locally from the web app.

  1. 01public sharp additive McDiarmid theorem
  2. 02public two-sided product theorem
  3. 03public downstream constant propagation
  4. 04public PAC-Bayes Bernstein shell
  5. 05adjacent formal-martingales Ville theorem
FormalSLT theorem chain showing Rademacher, VC, sharp McDiarmid, PAC-Bayes, and Dudley proof layers

what is new in v0.3

Public PR #6 folded in the v0.3 proof lane.

PR #71, #72, #74, and #75 are the development provenance for the public PR #6 bundle. The claim evidence above points to public main, public source paths, and the public README.

PR #71Prove sharp McDiarmid tail for bounded differencesfolded into public FormalSLT PR #6source: FormalSLT/Concentration/SharpMcDiarmid.lean5a4bf93d7cebdd9c80d062ea3561f6668c989e24
PR #72Propagate sharp McDiarmid constants downstreamfolded into public FormalSLT PR #6source: Rademacher, VC, and stability wrappers09f6f2cb313c99ad874060f5294a1c2e8818952a
PR #74Add two-sided sharp McDiarmid iid product theoremfolded into public FormalSLT PR #6source: FormalSLT/Concentration/SharpMcDiarmid.leanb3f63baf0b72e8771717d4037ccd095de1c32c17
PR #75Add PAC-Bayes Bernstein margin proxy shellfolded into public FormalSLT PR #6source: FormalSLT/PACBayesBernstein.leand0566a3838dce48e2e12cd5d25b087c3657d93c8

reproduce

The public repository has a rebuild path for this proof surface.

The live badge reads the public GitHub Actions workflow. The commands below rebuild public main against the pinned Lean and Mathlib versions listed in the provenance panel.

git clone https://github.com/Robby955/FormalSLT.git
cd FormalSLT
lake exe cache get
lake build FormalSLT
lake env lean examples/CheckPACBayesBernstein.lean
lake env lean FormalSLT/Test/SharpMcDiarmidTest.lean
python3 scripts/generate_proof_frontier_manifest.py --check

What this page now claims

  • Public main verifies the sharp additive independent McDiarmid theorem and its CI run is green.
  • Public main verifies the two-sided iid product theorem over a homogeneous product measure.
  • Public main verifies the finite PAC-Bayes Bernstein margin-proxy shell under supplied certificates.
  • The public `Robby955/FormalSLT` CI badge is live and linked to the current workflow run.

What remains separate

  • Ville's inequality is not claimed as a FormalSLT theorem here; it is an adjacent checked result in the martingale/Pythia lane.
  • Continuous Dudley entropy integrals remain future work; the current graph shows finite-net and total-bounded bridge layers.
  • The Bernstein margin shell assumes supplied variance and certificate inputs; concrete classifier-margin extraction is still a later proof step.
  • The old development PR numbers are provenance notes. Public PR #6 and public main are the live source of truth for this page.

retraction conditions

These are the conditions that would change the page.

The page should stay narrow. A later proof audit or public source mismatch should update the claim text rather than hide the boundary.

  • Public CI for `Robby955/FormalSLT` fails on the v0.3 proof surface.
  • A native axiom trace adds a nonstandard dependency to one of the theorem names above.
  • The public README, source tree, or proof-frontier manifest no longer lists the named theorem surface.
  • A later Lean audit changes the sharp exponent or the supplied variance-proxy assumptions.