← All status

Proving

Proving

Lean4 axiomatic kernel for the legal domain. RICO + Title VI + §§ 1981/1983/1985(3). Predicates return ⟨bool, evidence, citation⟩; the kernel does no I/O. Each verifier run produces a per-predicate report.json + proof-DAG graph.json + intro-rule loci.json — surfaced here as the recent-runs table + latest-run diagram + predicate roster.

version 623bc019a1f2
source proving/lake-manifest.json@623bc019a1f2
built 2026-07-24T09:25:07Z
DEGRADED

Correction ·

Agreement-tier figures withdrawn pending re-verification

What we found. Our own adversarial review lane found leak channels in the cross-axis agreement oracle that classifies our Tier-A/B/C figures. The fan-out agents that are supposed to agree independently could, in principle, see each other's work — so blind agreement was never established for any wave.

What survives. Kernel soundness is unaffected and mechanically re-checked: every lake build, every sorry-free proof still stands. You cannot leak your way into a green build — the encoded work is real. Only the agreement-based confidence is in question.

What is withdrawn. The agreement-based tier counts (proving's Tier-A/B/C and accounting's) are withdrawn — shown as "withheld", restated provisional as of 2026-07-14. Sections-encoded, universe %, sector census and the soundness panels are mechanical and remain.

The schedule. Re-earning a tier means a fresh blind re-slice under the now-closed contracts, not a re-score of the old one. It is sequenced cheapest-first: the operational axis re-attacks first, the financial axis re-slices next, and the textual re-slice is a multi-week program. This notice updates as each axis re-earns its figure.

Frameworks — module readiness

One node per Lean module. Focused = predicates + axioms compile under the current toolchain.

Frameworks — module readiness One node per Lean module. Focused = predicates + axioms compile under the current toolchain. civil RICO 18 U.S.C. §§ 1961–1968 Title VI 42 U.S.C. §§ 2000d et seq. civil-rights 42 U.S.C. §§ 1981/1983/1985(3) Title IX 20 U.S.C. §§ 1681–1688 Title VII 42 U.S.C. §§ 2000e-5/-6/-16 Rehab § 504 29 U.S.C. § 794 Age Act 42 U.S.C. §§ 6101–6107 Title II Enf 42 U.S.C. § 2000a-5(b) ADA 42 U.S.C. ch. 126

Verifier-run statistics

Aggregate over all examples/<id>/report.json artefacts.

Verifier runs

2

Complaints elaborated against the kernel.

Accepted

OK
2

Kernel verdict: ACCEPTED — the validity theorem elaborates.

Rejected

OK
0

Kernel verdict: REJECTED — at least one element disproved.

Latest run

13.8d ago

M.G. v. Springfield Public Schools — toy Title VI sample

Axiomatize-U.S.-Code program

Corpus-wide coverage from proving/coverage.json (dau-cross rollup).

Sections encoded

388

Operative U.S. Code sections encoded across all axes.

Tier-A

withheld

Agreement-tier confidence withdrawn 2026-07-14 — the cross-axis agreement oracle is under re-verification (blind re-slice pending). Sections-encoded and soundness figures are unaffected.

Titles touched

11/58

Distinct U.S. Code titles with at least one encoded section.

Of USC universe

0.62%

Share of the 62,831-section operative universe encoded so far.

Recent verifier runs One row per complaint elaborated against the kernel. Verdict pill reflects whether the validity theorem type-checks; the expand row enumerates each kernel rejection's locus.
IDComplaintFrameworkPredicatesVerdictFailuresRun at
titlevi_sampleM.G. v. Springfield Public Schools — toy Title VI sampletitlevi § 601 / § 602 / retaliation17 / 17 TrueACCEPTED02026-07-10T14:54:17Z
sampleDoe v. Acme — toy § 1962(c) samplerico § 1962(c)19 / 19 TrueACCEPTED02026-07-10T14:54:12Z
Sorted by runFinishedAt, descending.

§ 601 / § 602 / retaliation intro-rule shape — M.G. v. Springfield Public Schools — toy Title VI sample

One node per kernel-required element, coloured by per-element verdict. Round nodes are derived structures/theorems; rectangles are predicate slots. The top-level disjunction is focused.

§ 601 / § 602 / retaliation intro-rule shape — M.G. v. Springfield Public Schools — toy Title VI sample One node per kernel-required element, coloured by per-element verdict. Round nodes are derived structures/theorems; rectangles are predicate slots. The top-level disjunction is focused. via TitleVICoverage coverage ValidTitleVIJudicialClaim IntentionalDiscriminationClaim TitleVICoverage directed ✓ True · Low intentional ✓ True · Medium officialCap ✓ True · Low personInUS ✓ True · Low notInstrumentality ✓ True · Low recipient ✓ True · Low receivesFFA ✓ True · Low programOfRecipient ✓ True · Low underProgram ✓ 2 of 2
Predicate roster — M.G. v. Springfield Public Schools — toy Title VI sample Per-predicate atomic view of the most recent run. Each row is one Bool the kernel consumed via Facts.lean; expand the row for evidence and uncertainty rationale.
#PredicateArgsValueUncertaintyEvidenceCiteKernel locus
§ 601 / § 602 / retaliation
1IsPersonInUSmg titleviComplaintTruelow¶1 — Plaintiff M.G. is a 14-year-old Latino student enrolled at Lincoln Middle School, a public middle school operated by Defendant Springfield Public Schools, in Springfield, Massachusetts.
2NotAStateInstrumentalitymg titleviComplaintTruelow¶1: "Plaintiff M.G. is a 14-year-old Latino student enrolled at Lincoln Middle School... M.G.'s mother, MARIA GUTIERREZ, brings this action on M.G.'s behalf." — plaintiff is a natural person (a minor suing through a parent as next friend…
3IsRecipientspringfieldDistrict titleviComplaintTruelow¶2. Defendant SPRINGFIELD PUBLIC SCHOOLS ("the District") is a Massachusetts public school district. The District operates 28 schools serving approximately 24,000 students.
4ReceivesFederalFinancialAssistancespringfieldDistrict titleviComplaintTruelow¶3: "The District has received federal financial assistance from the U.S. Department of Education since at least 2010, including approximately $4.2 million annually in Title I grants for the 2022-23 and 2023-24 school years."
5IsProgramOfRecipientlincolnMagnet springfieldDistrict titleviComplaintTruelow¶5: "The District operates the Lincoln STEM Magnet (“the Magnet”), a competitive academic program housed at Lincoln Middle School."
6OccursUnderProgrampolicy2022 lincolnMagnet titleviComplaintTruelow¶5 — The District operates the Lincoln STEM Magnet ("the Magnet"), a competitive academic program housed at Lincoln Middle School. Admission is by application; selection criteria are set by the District's Board of Education.
7OccursUnderProgramsuspension2023 lincolnMagnet titleviComplaintTruelow¶15: "Lincoln Middle School Principal SARAH BRENNAN moved to suspend M.G. from Lincoln's after-school enrichment activities, citing \"attendance concerns\" that had not previously been raised."
8DefendantSuedInOfficialCapacityspringfieldDistrict titleviComplaintTruelow¶2 — Defendant SPRINGFIELD PUBLIC SCHOOLS ("the District") is a Massachusetts public school district. The District operates 28 schools serving approximately 24,000 students.
9ActionDirectedAtPersonpolicy2022 mg titleviComplaintTruelow¶12: "M.G. applied to the Magnet in 2023. M.G. ranked in the top 25% of test-takers but did not reach the top 10% cutoff."
10IntentionalDiscriminationpolicy2022 ProtectedGround.nationalOrigin titleviComplaintTruemedium¶9. Following implementation of the 2022 Policy, Latino enrollment in the Magnet dropped to 9% in the 2022-23 admitted class and 8% in the 2023-24 admitted class. Over the same period, Latino representation in the District-wide eligible …
11IsFaciallyNeutralPolicypolicy2022 titleviComplaintTruelow¶7: "In January 2022, the Board of Education adopted a new admissions policy ("the 2022 Policy"). Under the 2022 Policy, the sole admissions criterion is performance on the Springfield High Schools Admissions Test ("SHSAT"), with admissi…
12AdverseDisparateImpactpolicy2022 ProtectedGround.nationalOrigin titleviComplaintTruelow¶7: "Under the 2022 Policy, the sole admissions criterion is performance on the Springfield High Schools Admissions Test (\"SHSAT\"), with admission limited to applicants scoring in the top 10% of test-takers."
13CausalLinkBetweenPolicyAndImpactpolicy2022 titleviComplaintTruelow¶7. Under the 2022 Policy, the sole admissions criterion is performance on the Springfield High Schools Admissions Test ("SHSAT"), with admission limited to applicants scoring in the top 10% of test-takers. Grades and teacher recommendat…
14LacksSubstantialLegitimateJustificationpolicy2022 titleviComplaintTruelowThe District has stated, in public Board meetings, that the SHSAT-only criterion was selected because it is "objective" and "traditional."
15ProtectedActivitymg titleviComplaintTruelow¶14: "On 2023-09-15, MARIA GUTIERREZ filed a written Title VI complaint with the District's Title VI Coordinator alleging that the 2022 Policy discriminated against Latino applicants. She also filed a parallel complaint with the U.S. Dep…
16AdverseActionsuspension2023 mg titleviComplaintTruelow¶15: "On 2023-09-29 — exactly two weeks later — Lincoln Middle School Principal SARAH BRENNAN moved to suspend M.G. from Lincoln's after-school enrichment activities, citing 'attendance concerns' that had not previously been raised."
17RetaliatoryCausationsuspension2023 mg titleviComplaintTruelow¶14: 'On 2023-09-15, MARIA GUTIERREZ filed a written Title VI complaint with the District's Title VI Coordinator alleging that the 2022 Policy discriminated against Latino applicants.'
titlevi § 601 / § 602 / retaliation — 17 of 17 True.

Metrics

frameworkCount
9
frameworksPresent
9
runsTotal
2
runsAccepted
2
runsRejected
0
leanGraphEmitFresh
1
leanGraphEmitRev
5bb06efb0
leanGraphModality
monotone-corpus
leanGraphDenominator
3
leanGraphCoveragePct
1
leanGraphVelocity
0
leanGraphGoldenShare
1
leanGraphAutomatedShare
0
leanGraphMeanDeps
31.5
leanGraphGeneratedFactShare
0.37566137566137564
leanGraphToolchainCurrent
1
uscEncodedSections
388
uscTierA
withheld — agreement oracle under re-verification, 2026-07-14
uscTierB
withheld — agreement oracle under re-verification, 2026-07-14
uscTierC
withheld — agreement oracle under re-verification, 2026-07-14
uscTierBlindCertified
0
uscWavesTotal
77
uscWavesBlindnessCertified
55
uscSectionsReEarned
272
uscTitlesTouched
11
uscTitleUniverse
58
uscSectionUniverse
62831
uscUniversePct
0.6175
latestRunId
titlevi_sample
latestRunAt
2026-07-10T14:54:17Z
latestVerdict
ACCEPTED
latestProofGraphUrl
https://qnarre.quantapix.com/proof-graph/run/titlevi_sample/