Evidence

Claim-level traceability, with boundaries visible.

FormalSLT revision dated: September 4, 2026 · Lean mapping 2026-05-07

TheoremPath records reviewed qualified-name and path mappings from governed claims to checked Lean theorem artifacts. The current formal layer covers selected probability, statistics, and learning-theory results. Of the 1,231 governed claims, 56 carry a Lean manifest entry and 153 carry recorded source support. The rest carry neither, and this page makes no review claim about them.

Lean-checked entries are grouped by public declaration mapping: 51 have reviewed public declarations with equal normalized unelaborated statement text, 2 have reviewed public declarations with different normalized statement text, and 3 have no reviewed public qualified-name/path mapping at the audited revision. The source comparison ends before the top-level proof assignment, so proof bodies are not compared. It also does not compare elaborated Lean expressions or establish semantic equivalence between repositories. The theorem index lists the entries one claim at a time; the Lean dashboard carries the toolchain pins and the per-entry mapping class.

This page also separates product contracts from research evidence: a signed-in smoke can prove that state is written and read, but it does not prove learning lift, calibrated item difficulty, or an IRT model fit.

Product truth contract

The adaptive layer is instrumented, not validated as an outcome claim.

The implemented learner loop can save state, connect attempts to the graph, and schedule reviews. The evidence bar is higher for claims about improved learning, calibrated ability, or item discrimination. Those claims require enough real signed-in data and comparison against baselines.

FSRS

scheduler signal

FSRS-style review state estimates card retrievability from review timing and grades. It can decide what is due for review; it is not a proof of mastery or a claim that the learner understands the theorem.

Q-matrix

coverage map

The Q-matrix links questions to skills, claims, and prerequisites. It explains what an item is meant to test; it is not a causal proof that a missed item has one unique cause.

PFA

guarded fit lane

Performance Factor Analysis is the planned interpretable fit over practice opportunities and correctness. Current production rows are data-insufficient, so PFA stays behind calibration gates instead of being presented as a validated personalization model.

Public mapping: text equal

Reviewed public declaration present with normalized unelaborated statement text equal before the proof assignment.

Public mapping: text different

The reviewed public qualified declaration is present, but its normalized unelaborated statement text before the proof assignment is different.

No reviewed public mapping

The legacy manifest records this entry as checked. It has no reviewed public qualified-name/path mapping at the audited revision.

Formalized claims

Checked formal statements whose recorded scope matches the governed claim.

Dependency formalized

Checked supporting lemmas that do not by themselves prove the full public claim.

sorry / admit

Lean placeholders across these checked entries: sorry=0, admit=0.

Operating dashboard

Gaps are part of the evidence record.

These counts are generated from governed claims, source-location records, the Lean manifest, assessment links, and published topic MDX. The point is not a trust badge; it is a work queue with visible missing pieces.

Governed claims

1,231

Claim records tracked in the public governance index.

Flagship trail coverage

12/12

0 missing trail requirements across theorem-first paths, including the two failure-check floor.

Atlas traces

48 curated checkpoints; 0 missing trace requirements.

Source locators

153/153

100% of source-supported claims resolve to source-location IDs.

Lean mapping

118 source-supported formal claims still need manifest entries; 3 are explicit source-only deferrals.

Source-only formal

Broad source-reviewed theorem claims that are deliberately not treated as Lean-mapping tasks yet.

Diagnostic items

116

108/153 source-checked claims have canonical item links.

Missing theorem blocks

625/672 published topics include theorem blocks.

Missing exercise blocks

632/672 published topics include exercise blocks.

Structure queue

Published topics missing theorem or exercise blocks across 672 topics.

Research quality queue

Ranked from the generated coverage report. Each row points to the first concrete gap to close in that work lane.

4 active lanes

01
Collect diagnostic calibration data
Real usage is below the publication threshold. Item difficulty: 6/30.
#evidence-calibration-difficulty
0/6
usage milestones met
02
Map source-checked theorems to Lean
Source-supported formal claims should either have a Lean manifest entry or remain visibly source-only.
/topics/inner-product-spaces-and-orthogonality#claim-evidence
118/153
formal claims without Lean
03
Add canonical diagnostics to checked claims
Claims with evidence should have at least one diagnostic item that tests the exact assumption or theorem.
/topics/cramer-rao-bound#claim-evidence
45/153
checked claims without diagnostics
04
Close theorem and exercise structure gaps
Published topics without theorem or exercise blocks should be fixed or kept out of flagship paths.
/topics/agent-based-modeling-with-ml#topic-mdx-content
47/672
published topics with structure gaps

Source locator gaps

All source-supported claims currently resolve to source-location IDs.

Lean mapping gaps

118

Source-only formal claims

Diagnostic gaps

Topic structure gaps

Flagship trail audit

Every flagship theorem trail currently satisfies the theorem-first contract, including at least two evidence-linked failure checks.

Atlas trace checkpoints

Every curated theorem trace currently exposes edge reasons, checkpoints, and trail links.

Audit receipts

Learner loop contracts: 15/15 All checks covered.

Required smoke gates before calling this production-ready: route shell, signed-in web state, account deletion guard, iOS continuity, Browser and iPhone proof assets, and Signed-in iPhone visual walkthrough receipts.

Covered means the contract exists and has a receipt. It does not mean the study policy is empirically better than a baseline or that the psychometric model is calibrated.

3 of 3 production smoke receipts are more than 30 days old. Each receipt row shows when its smoke ran and against which commit.

Source receipt: data/content/learner-loop-readiness.json. Generated September 17, 2026.

Q-matrix rows: Diagnostic items are tied back to the same governed claim and skill graph.
Claim links: Claim-to-assessment links are treated as reviewable evidence, not page decoration.
Content gaps blocking trails: Open trail blockers stay visible until the flagship audit is clean.
Failure modes: Trail checks must include at least two evidence-linked failure checks before promotion.

Open production health Open sign-up flow Open iOS graph contract Open gap finder

Open route

Markov tail bound Chebyshev variance tail Finite union bound Hoeffding lemma Hoeffding finite-sum bound Finite-class uniform convergence

Inspect learner-loop receipt rows

Public route shell (covered)
Home, Atlas, Evidence, sign-up, learner home, and Profile routes exist in the current branch.
Signed-in web launch gate (covered)
The required signed-in smoke has a preflight that rejects localhost, stale host state, missing smoke email, unsafe deletion aliases, and stale public learner-loop contracts. A fresh-user wrapper chains the public contract, the iOS companion source contract, the iOS intended API contract, Clerk test-auth onboarding storage-state capture for +clerk_test accounts, intended walkthrough, a post-walkthrough bearer-token refresh, and required-by-default iOS signed-in continuity with a non-logged bearer-token file handoff. If destructive deletion is enabled with iOS continuity, deletion runs last so iOS can read the account state before removal.
Diagnostic persistence (covered)
Signed-in diagnostic submissions write diagnostic attempts, learning events, event logs, and evidence envelopes.
Saved, review, and Profile state (covered)
The intended signed-in walkthrough answers a saved diagnostic item, then exercises a saved topic, review entry point, learner home evidence, Profile identity, and authenticated API receipts for saved, diagnostic, review, and mastery state.
Account deletion guard (covered)
Deletion smoke is gated behind an explicit flag and a disposable +tp-delete- alias, then verifies the deleted account no longer has a live API profile.
No PII in learner-loop events (covered)
Product-loop events redact sensitive keys and values; typed learning events reject raw learner text metadata.
Evidence dashboard inputs (covered)
Claims=1231, Lean mappings=56, source locators=135, diagnostic items=3496, Q-matrix rows=13878, claim links=133, content gaps=10.
Flagship theorem trails (covered)
Flagship audit reports 12/12 trails under the machine contract.
Atlas trace checkpoints (covered)
Atlas path responses include traversal-order reasons/checkpoints, the UI renders them, and check:atlas-paths enforces the contract.
iOS companion contract (covered)
The tracked iOS contract receipt covers the companion contract, intended public API probe, bearer-token continuity probe, TestFlight readiness check, simulator tests, and simulator build-run.
Latest public deployment contract smoke (covered)Ran June 29, 2026 on commit f08ec23stale (88 days)
Latest verified public learner-loop smoke passed against https://theorempath.com with THEOREMPATH_EXPECTED_GIT_SHA=f08ec233488add2af375eb15c36b6fbe3c197b6a. The current live production SHA is reported separately by /api/health so this static receipt does not pretend to prove its own future deploy commit.
Signed-in production/staging smoke (covered)Ran June 29, 2026 on commit f08ec23stale (88 days)
Fresh disposable-account smoke passed against production: public contract, Clerk test-auth onboarding without OTP, diagnostic completion, beta topic save, daily review, learner home, Profile identity, post-walkthrough bearer-token refresh, persisted API receipts, and deletion-only account removal after iOS continuity. Raw smoke email and bearer token were not stored.
iOS signed-in API continuity (covered)Ran June 29, 2026 on commit f08ec23stale (88 days)
iOS signed-in API continuity passed against production using the refreshed non-logged bearer-token file from the fresh web smoke: /api/v1/me, saved beta-distribution state, diagnostic attempts, review today, and mastery state were readable for the same disposable account before deletion.
Browser and iPhone proof assets (covered)
The proof receipt tracks one production browser evidence-dashboard capture plus iOS simulator Today, Atlas, Saved, and Profile screenshots under data/content/learner-loop-demo-capture.json.
Signed-in iPhone visual walkthrough (covered)
Signed-in fresh-install iOS screenshots show the same disposable production smoke account in Today, Saved, Atlas, and redacted Profile; the API continuity probe also passed for that account.

Usage calibration

Diagnostics are calibrated only where real usage supports it.

This block is generated by npm run psychometrics:report from LearningEvent rows. It separates item difficulty, item skip rate, item discrimination, review conversion, and later performance after review.

Implemented today

Signed-in learner state, Q-matrix links, review events, saved topics, profile identity, and iOS API continuity have contract receipts.

Not claimed yet

The saved report is still data-insufficient for item calibration or IRT. No public claim should treat the current samples as a fitted psychometric model.

Next evidence

Collect enough real signed-in attempts per item, then compare review and recommendation policies against baselines before promoting effectiveness claims.

Open psychometrics audit20 AssessmentAttempt rows · 146 LearningEvent rows · 11 DiagnosticAttempt runs

snapshot June 28, 2026

Calibration state

Sparse

Real usage rows exist, but sample sizes remain below calibration thresholds.

Answer events

142

Non-review LearningEvent rows used for item difficulty and discrimination.

Difficulty usable

Items with enough observations for empirical difficulty estimates.

Skip rate

Items with recorded skipped answers in the current usage report.

Discrimination usable

Items with enough learner contrast for high-minus-low ability separation.

Review conversion

0/12

Weak diagnostic answers that were followed by a review event.

Review effect pairs

Weak diagnostic answers followed by review and a later performance event.

Unreviewed pairs

Weak diagnostic answers without review but with later performance, used as a comparison group.

Readiness milestones

Best observed item-level counts against the publication thresholds. Source: database · 146 LearningEvent rows.

0/6 met

Item difficulty

6/30

24 more needed on one item.

Skip rate

6/30

24 more needed on one item.

Item discrimination

2/30

28 more needed on one item.

Review conversion

2/10

8 more needed on one item.

Later performance after review

0/10

10 more needed on one item.

Unreviewed comparison

0/10

10 more needed on one item.

Next collection targets

Item-level targets from the same saved usage report. These are collection instructions, not calibration claims.

6 open

Item difficulty
question:diverse-spot-error-002
24 more events with scored answer outcomes.
6/30
Open topic Collect signal
Skip rate
question:diverse-spot-error-002
24 more events with answer or skip outcomes.
6/30
Open topic Collect signal
Item discrimination
question:diverse-spot-error-002
28 more events from learners with other answered items.
2/30
Open topic Collect signal
Review conversion
question:diverse-counterexample-002
8 more events where weak diagnostic answers enter review.
2/10
Open topic Collect signal
Later performance after review
question:activation-relu-dead-neurons-004
10 more events where reviewed weak answers get later performance.
0/10
Open topic Collect signal
Unreviewed comparison
question:activation-relu-dead-neurons-004
10 more events where unreviewed weak answers get later performance.
0/10
Open topic Collect signal

Item difficulty: 6/30.
Skip rate: 6/30.
Item discrimination: 2/30.
Review conversion: 2/10.
Later performance after review: 0/10.

Calibration policy

difficulty n: 30
discrimination learners: 30
review opportunities: 10
effect pairs: 10
later window: 30d
simulation: excluded

Difficulty collection queue

question:linear-algebra-path-012
inner-product-spaces-and-orthogonality · n=2
Open topic Run diagnostic
n=2/30
question:linear-algebra-psd-pd-009
positive-semidefinite-matrices · n=2
Open topic Run diagnostic
n=2/30
question:inner-product-gram-schmidt-020
inner-product-spaces-and-orthogonality · n=1
Open topic Run diagnostic
n=1/30
question:inner-product-orthogonal-complement-021
inner-product-spaces-and-orthogonality · n=1
Open topic Run diagnostic
n=1/30

Skip-rate collection queue

question:linear-algebra-path-012
inner-product-spaces-and-orthogonality · n=2
Open topic Run diagnostic
n=2/30 · skip observed 100%
question:linear-algebra-psd-pd-009
positive-semidefinite-matrices · n=2
Open topic Run diagnostic
n=2/30 · skip observed 100%
question:inner-product-gram-schmidt-020
inner-product-spaces-and-orthogonality · n=1
Open topic Run diagnostic
n=1/30 · skip observed 100%
question:inner-product-orthogonal-complement-021
inner-product-spaces-and-orthogonality · n=1
Open topic Run diagnostic
n=1/30 · skip observed 100%

Discrimination queue

No item has enough learner contrast for discrimination yet.

Review conversion queue

question:diverse-counterexample-002
maximum-likelihood-estimation · n=2
Open topic Run diagnostic
0/2 reviewed
question:activation-relu-dead-neurons-004
activation-functions · n=1
Open topic Run diagnostic
0/1 reviewed
question:ei-spot-error-009
stochastic-gradient-descent-convergence · n=1
Open topic Run diagnostic
0/1 reviewed
question:la-drill-rank-nullity-021
vectors-matrices-and-linear-maps · n=1
Open topic Run diagnostic
0/1 reviewed

Later performance queue

No reviewed item has enough later-performance pairs yet.

Sealed evaluation

The sealed holdout of Ask returned a verdict of BLOCKED.

The Ask route answers only from text it retrieves from this site. Its routing decision, whether to answer from a retrieved source or to refuse for want of one, was scored against a case set and a protocol sealed before the code was read, with answer generation disabled. The run reports nothing about answer quality, citation fidelity, or refusal compliance. It was evaluated on August 10, 2026 against commit dd384574b5f3.

The reliability page carries the result: both confusion matrices, every gate outcome, the earlier holdout sealed August 9, 2026 for context, and the artifact hashes. Its figures are read from data/reliability/ask-holdout-report.json and are not restated here. The frozen retrieval evaluation that preceded both holdouts is recorded, with its hashes, in data/learning-model/research-log/2026-08-09-chat-evidence-gate.md.

Status labels

Formalized: The checked Lean theorem matches the governed claim scope.
Dependency formalized: A supporting lemma is checked, and the broader public claim is waiting on additional assumptions or proof steps.
Source-reviewed outside Lean: The claim can be source-supported while carrying no Lean proof badge on this page.

One complete trace: Markov's inequality

A serious evidence record should be inspectable. This example shows the informal claim, the formal theorem, and the boundary of that mapping.

Claim ID	claim:concentration-inequalities::markov-inequality
Informal claim	For a nonnegative random variable, tail probability is bounded by expectation divided by the threshold.
Formalized as	real-valued integrable Markov inequality with explicit nonnegativity, integrability, and positive-threshold assumptions
Public declaration	FormalSLT.Probability.Concentration.markovInequalityRealIntegrable
Legacy manifest declaration	TheoremPath.Probability.Concentration.markovInequalityRealIntegrable
Boundary	This Lean wrapper verifies the recorded real-valued Markov statement; broader concentration variants have separate claim records.

Lean theorem statement

theorem markovInequalityRealIntegrable
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {X : Ω → ℝ} {t : ℝ}
    (hNonneg : 0 ≤ᵐ[μ] X) (hIntegrable : Integrable X μ) (ht : 0 < t) :
    μ.real {ω | t ≤ X ω} ≤ (∫ ω, X ω ∂μ) / t

Public source mapping for this entry: Normalized statement text equal

FormalSLT/Probability/Concentration.lean:48

Verification boundary

Of the 1,231 governed claims, 153 are marked source-checked. The rest are not, and a claim with no Lean entry and no source check has neither form of evidence recorded against it.
The finite-class uniform convergence entry is still a dependency formalization; the full stochastic theorem is tracked as a later composition target.
Active learning-theory proof lanes include iid sampling, bounded-loss instantiation, measurability of hypothesis classes, and closed-form sqrt/log rearrangements.

Examples from the Lean mapping

Each card records the checked declaration, the theorem scope, and whether it formalizes the governed claim or only a dependency.

concentration inequalities

Markov Inequality

FormalizedNormalized statement text equal

In plain English

A nonnegative random variable with small expectation cannot be large very often.

Role in the graph

This is the first tail-bound bridge from averages to probability guarantees.

Legacy checked theorem

TheoremPath.Probability.Concentration.markovInequalityRealIntegrable

Public declaration

FormalSLT.Probability.Concentration.markovInequalityRealIntegrable

Claim scope

real integrable nonnegative markov inequality

Proof scope

exact mathlib wrapper for markov

Mathlib theorem

MeasureTheory.mul_meas_ge_le_integral_of_nonneg

Exact claim-facing mathlib wrapper for Markov's inequality in real-valued integrable form. The finite weighted-support theorem remains a bridge proof, not the canonical verification target.

FormalSLT/Probability/Concentration.lean:48

Legacy manifest checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

concentration inequalities

Hoeffding One Sided Finite Sum

FormalizedNormalized statement text equal

In plain English

A bounded finite sum has an exponential one-sided deviation bound under the recorded assumptions.

Role in the graph

This is the concentration step behind finite-class generalization arguments.

Legacy checked theorem

TheoremPath.Probability.Concentration.hoeffdingBoundedFiniteSumTail

Public declaration

FormalSLT.Probability.Concentration.hoeffdingBoundedFiniteSumTail

Claim scope

finite centered sum bounded hoeffding one sided

Proof scope

exact mathlib wrapper for bounded hoeffding finite sum tail

Mathlib theorem

ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc, ProbabilityTheory.iIndepFun.comp, ProbabilityTheory.HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun

Exact claim-facing wrapper for the one-sided finite-sum Hoeffding bound for bounded independent real random variables.

FormalSLT/Probability/Concentration.lean:170

Legacy manifest checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

subgaussian random variables

Hoeffding Lemma

FormalizedNormalized statement text equal

In plain English

A bounded centered random variable has a sub-Gaussian moment-generating-function bound.

Role in the graph

This is the standard bridge from bounded variables to Hoeffding-style tails.

Legacy checked theorem

TheoremPath.Probability.Concentration.hoeffdingLemmaBoundedCenteredSubgaussianMGF

Public declaration

FormalSLT.Probability.Concentration.hoeffdingLemmaBoundedCenteredSubgaussianMGF

Claim scope

bounded centered real subgaussian mgf

Proof scope

exact mathlib wrapper for hoeffding lemma

Mathlib theorem

ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero

Exact mathlib wrapper for Hoeffding's lemma in sub-Gaussian MGF form. Source review now permits claim-level display without implying the whole page is Lean verified.

FormalSLT/Probability/Concentration.lean:154

Legacy manifest checked April 29, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

measure theoretic probability

Borel Cantelli First

FormalizedNormalized statement text equal

In plain English

If event probabilities are summable, the limsup event has probability zero in the mathlib formulation.

Role in the graph

This turns a previous finite bridge into a direct probability theorem wrapper.

Legacy checked theorem

TheoremPath.Probability.BorelCantelli.borelCantelliFirstLimsupMeasureZero

Public declaration

FormalSLT.Probability.BorelCantelli.borelCantelliFirstLimsupMeasureZero

Claim scope

first borel cantelli limsup atTop ennreal

Proof scope

exact mathlib wrapper for first borel cantelli

Mathlib theorem

MeasureTheory.measure_limsup_atTop_eq_zero, MeasureTheory.ae_eventually_notMem

Exact claim-facing mathlib wrapper for the first Borel-Cantelli lemma in limsup-measure-zero form. The finite union-bound artifacts remain supporting bridge proofs, not the source of verification.

FormalSLT/Probability/BorelCantelli.lean:19

Legacy manifest checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

kolmogorov probability axioms

Probability Measure Finite Union Bound

FormalizedNormalized statement text equal

In plain English

The probability of a finite union is at most the sum of the individual probabilities.

Role in the graph

This is a foundational tool used throughout concentration and learning theory.

Legacy checked theorem

TheoremPath.Probability.KolmogorovAxioms.probabilityMeasureFiniteUnionBound

Public declaration

FormalSLT.Probability.KolmogorovAxioms.probabilityMeasureFiniteUnionBound

Claim scope

probability measure finite union bound

Proof scope

exact mathlib wrapper for probability measure finite union bound

Mathlib theorem

MeasureTheory.measure_biUnion_finset_le

Exact claim-facing wrapper for the finite union bound for probability measures.

FormalSLT/Probability/KolmogorovAxioms.lean:74

Legacy manifest checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

common inequalities

Cauchy Schwarz Inequality

FormalizedNormalized statement text equal

In plain English

The absolute inner product is bounded by the product of the two norms.

Role in the graph

This is a reusable inequality across linear algebra, statistics, and optimization.

Legacy checked theorem

TheoremPath.LinearAlgebra.CommonInequalities.cauchySchwarzRealInner

Public declaration

FormalSLT.LinearAlgebra.CommonInequalities.cauchySchwarzRealInner

Claim scope

real inner product space cauchy schwarz

Proof scope

exact mathlib wrapper for cauchy schwarz core

Mathlib theorem

abs_real_inner_le_norm

Exact claim-facing mathlib wrapper for the core Cauchy-Schwarz inequality in real inner product spaces. Equality, probability, and finite-sum variants remain separate explanatory scopes until governed separately.

FormalSLT/LinearAlgebra/CommonInequalities.lean:20

Legacy manifest checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

vc dimension

Sauer Shelah Lemma

FormalizedNormalized statement text equal

In plain English

A finite set family with bounded VC dimension cannot shatter too many subsets.

Role in the graph

This is a core combinatorial bridge behind classical learning-theory capacity bounds.

Legacy checked theorem

TheoremPath.LearningTheory.VCDimension.sauerShelahFiniteSetFamily

Public declaration

FormalSLT.VC.Dimension.sauerShelahFiniteSetFamily

Claim scope

finite set family sauer shelah binomial sum

Proof scope

exact mathlib wrapper for sauer shelah binomial sum

Mathlib theorem

Finset.card_le_card_shatterer, Finset.card_shatterer_le_sum_vcDim

Exact claim-facing mathlib wrapper for the finite set-family Sauer-Shelah binomial-sum bound. The common (em/d)^d analytic estimate is treated as a downstream corollary, not as part of this verified claim.

FormalSLT/VC/Dimension.lean:15

Legacy manifest checked April 28, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

uniform convergence

Finite Class Uniform Convergence

Dependency formalizedNormalized statement text equal

In plain English

The checked artifact is a scoped reduction step toward the finite-class uniform convergence theorem.

Role in the graph

It is useful evidence, but it is deliberately not labeled as the full stochastic theorem.

Legacy checked theorem

TheoremPath.LearningTheory.UniformConvergence.finiteClassEpsilonRepresentativeHighProbabilityFromOneSidedTails

Public declaration

FormalSLT.UniformConvergence.finiteClassEpsilonRepresentativeHighProbabilityFromOneSidedTails

Claim scope

finite class epsilon representative failure probability from one sided risk deviation tails

Proof scope

scoped high probability risk bridge for finite class uniform convergence

Mathlib theorem

MeasureTheory.measure_union_le, TheoremPath.Probability.FiniteUnionBound.finiteMeasureUnionBound, MeasureTheory.ofReal_measureReal, ENNReal.ofReal_le_ofReal

Scoped bridge artifact for finite-class uniform convergence. It proves the risk-facing high-probability reduction from paired one-sided true-risk/empirical-risk deviation tail bounds and a delta-sized finite-class union-bound expression to a simultaneous epsilon-representative failure bound, and now includes fixed-hypothesis empirical-average upper- and lower-tail Hoeffding bridges with explicit sample-size hypotheses plus ENNReal adapters for the measure-valued union-bound layer; it does not verify iid sampling as the data-generating model or the closed-form sqrt/log sample-complexity display.

FormalSLT/UniformConvergence.lean:524

Legacy manifest checked April 30, 2026 · Lean 4.30.0-rc2 · mathlib 25b7ac7d0c

Diagnostic assumption links

A diagnostic item can be mapped to the exact assumption or theorem it tests. The Hoeffding slice records separate links for independence, the boundedness-to-sub-Gaussian step, and the finite-class union-bound step.

These mappings are evidence for learner state. They are not public theorem badges, and they should be audited like any other claim-to-source or claim-to-Lean link.

What waits before public badges

Evidence panels must show claim scope, not just page-level status.
Dependency formalizations must be visually distinct from exact claim wrappers.
Topic pages need stable source and diagnostic links before any trust indicator is promoted.

For the rules behind this page, see methodology. For the breakdown of 51 public mappings with equal normalized statement text, 2 with different normalized statement text, and 3 entries without a reviewed public mapping, see the Lean verification dashboard. For the claims themselves, see the theorem index.