← 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-04T11:41:43Z
OK

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. § 1981 42 U.S.C. § 1981 § 1983 42 U.S.C. § 1983 § 1985(3) 42 U.S.C. § 1985(3)

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

55.0d 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

196

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

Tier-A (golden)

OK
126

≥3 axes agree, all cross-axis bridges discharge sorry-free (Tier-B 41 / Tier-C 29).

Titles touched

7/58

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

Of USC universe

0.31%

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-05-10T12:17:06Z
sampleDoe v. Acme — toy § 1962(c) samplerico § 1962(c)19 / 19 TrueACCEPTED02026-05-10T12:17:02Z
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 · — intentional ✓ True · — officialCap ✓ True · — personInUS ✓ True · — notInstrumentality ✓ True · — recipient ✓ True · — receivesFFA ✓ True · — programOfRecipient ✓ True · — 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 titleviComplaintTrue
2NotAStateInstrumentalitymg titleviComplaintTrue
3IsRecipientspringfieldDistrict titleviComplaintTrue
4ReceivesFederalFinancialAssistancespringfieldDistrict titleviComplaintTrue
5IsProgramOfRecipientlincolnMagnet springfieldDistrict titleviComplaintTrue
6OccursUnderProgrampolicy2022 lincolnMagnet titleviComplaintTrue
7OccursUnderProgramsuspension2023 lincolnMagnet titleviComplaintTrue
8DefendantSuedInOfficialCapacityspringfieldDistrict titleviComplaintTrue
9ActionDirectedAtPersonpolicy2022 mg titleviComplaintTrue
10IntentionalDiscriminationpolicy2022 ProtectedGround.nationalOrigin titleviComplaintTrue
11IsFaciallyNeutralPolicypolicy2022 titleviComplaintTrue
12AdverseDisparateImpactpolicy2022 ProtectedGround.nationalOrigin titleviComplaintTrue
13CausalLinkBetweenPolicyAndImpactpolicy2022 titleviComplaintTrue
14LacksSubstantialLegitimateJustificationpolicy2022 titleviComplaintTrue
15ProtectedActivitymg titleviComplaintTrue
16AdverseActionsuspension2023 mg titleviComplaintTrue
17RetaliatoryCausationsuspension2023 mg titleviComplaintTrue
titlevi § 601 / § 602 / retaliation — 17 of 17 True.

Metrics

frameworkCount
5
frameworksPresent
2
runsTotal
2
runsAccepted
2
runsRejected
0
uscEncodedSections
196
uscTierA
126
uscTierB
41
uscTierC
29
uscTitlesTouched
7
uscTitleUniverse
58
uscSectionUniverse
62831
uscUniversePct
0.3119
latestRunId
titlevi_sample
latestRunAt
2026-05-10T12:17:06Z
latestVerdict
ACCEPTED
latestProofGraphUrl
https://qnarre.quantapix.com/proof-graph/run/titlevi_sample/