← 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-06-24T15:42:13Z
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

19

Complaints elaborated against the kernel.

Accepted

OK
13

Kernel verdict: ACCEPTED — the validity theorem elaborates.

Rejected

DEGRADED
6

Kernel verdict: REJECTED — at least one element disproved.

Latest run

3.0d ago

Kifor v. Commonwealth — Renewed RICO Complaint (hierarchical decomposition)

Axiomatize-U.S.-Code program

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

Sections encoded

135

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

Tier-A (golden)

OK
74

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

Titles touched

5/58

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

Of USC universe

0.21%

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
kifor_rico_hierKifor v. Commonwealth — Renewed RICO Complaint (hierarchical decomposition) (1:25-cv-11831-AK)rico-hier § 1962(c) (hierarchical)29 / 49 TrueREJECTED102026-06-21T16:07:13Z
usc_t18_enterprise_hierDoe v. Northgate Servicing Group — synthetic § 1961(4) AIF-enterprise sampleusc-t18-hier § 1961(4)4 / 4 TrueACCEPTED02026-06-20T19:50:39Z
titleiienf_threejudgeUnited States v. Northwest Louisiana Restaurant Club — § 2000a-5(b) three-judge convening record (W.D. La. Civ. A. No. 11033)titleiienf § 2000a-5(b) three-judge track8 / 8 TrueACCEPTED02026-06-20T14:19:06Z
titleiienf_singlejudgeUnited States v. DeRosier (Northwood Bar) — § 2000a-5(b) single-judge fallback record (S.D. Fla. No. 71-665-Civ)titleiienf § 2000a-5(b) single-judge fallback4 / 4 TrueACCEPTED02026-06-20T14:19:05Z
titleiienf_threejudge_gulfstateUnited States v. Gulf-State Theaters — § 2000a-5(b) three-judge convening record (N.D. Miss. No. GC6450)titleiienf § 2000a-5(b) three-judge track8 / 8 TrueACCEPTED02026-06-20T14:19:05Z
ageact_sampleH.V. v. Lakeside Workforce Development Program — toy Age Act sampleageact § 6102 (intentional / impact / retaliation)21 / 21 TrueACCEPTED02026-06-08T20:52:50Z
rehab504_sampleM.D. v. Riverside Community College — toy § 504 samplerehab504 § 794 (intentional / failure-to-accommodate / impact / retaliation)21 / 21 TrueACCEPTED02026-06-08T20:52:50Z
titleix_sampleR.K. v. Northgate University — toy Title IX sampletitleix § 1681 (intentional / impact / retaliation / deliberate indifference)25 / 25 TrueACCEPTED02026-06-07T18:21:06Z
titlevii_fedsector_sampleOkafor v. Secretary of Veterans Affairs — toy Title VII § 2000e-16(c) sampletitlevii § 2000e-16(c)5 / 5 TrueACCEPTED02026-06-07T18:04:47Z
titlevii_patternpractice_sampleEEOC v. Borealis Logistics — toy Title VII § 2000e-6(a) sampletitlevii § 2000e-6(a)5 / 5 TrueACCEPTED02026-06-07T18:04:47Z
Sorted by runFinishedAt, descending.

§ 1962(c) (hierarchical) intro-rule shape — Kifor v. Commonwealth — Renewed RICO Complaint (hierarchical decomposition)

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.

§ 1962(c) (hierarchical) intro-rule shape — Kifor v. Commonwealth — Renewed RICO Complaint (hierarchical decomposition) 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 Section1962c violation pattern ValidCivilRicoComplaint ValidCivilRicoComplaint1962c Section1962c PatternOfRacketeering injury ✓ True · Low causation ✓ True · High timely ✓ True · Low culpable ✗ False · Medium enterprise — · not exercised interstateCommerce ✓ True · Low distinct ✓ True · Low associated ✓ True · Low conducts ✓ True · Low twoOrMore allRacketeering — · not exercised withinWindow ✓ True · Low related — · not exercised continuous — · not exercised
Predicate roster — Kifor v. Commonwealth — Renewed RICO Complaint (hierarchical decomposition) 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
common
1CulpablePersonCapableOfIntentfamilyCourt kiforComplaintFalsemedium¶ 8.6: 'MIDDLESEX PROBATE AND FAMILY COURT, i.e., [Current Chief Justice] (official capacity), Probate and Family Court Administrative Office'18 U.S.C. § 1961(3)section1962c_intro.—
2EngagedInInterstateCommerceenterprise kiforComplaintTruelowCCNE ("CCNE," now CCNE, with 36 locations in MA and 13 in NH), i.e., [CCNE CEO] (official capacity), 4800 N. Scottsdale Road, Suite 2500, Scottsdale, AZ 8525118 U.S.C. § 1962
6WithinTenYearsact3 act10 kiforComplaintTruelowAct-3 dated 2022-11-22 (¶ 33)18 U.S.C. § 1961(5)
7BusinessOrPropertyInjuryfather kiforComplaintTruelow¶ 64: 'he lost $1M+ in "legal fees" as part of his $10M+ in damages' — quantified pecuniary loss.18 U.S.C. § 1964(c)
9WithinFourYearLimitationsPeriodfather kiforComplaintTruelowHeader: 'Case 1:25-cv-11831-AK Document 9-2 Filed 09/09/25' + '¶'-dated 'September 8, 2025' — filing date.18 U.S.C. § 1964(c)
§ 1962(c) (hierarchical)
3PersonEnterpriseDistinctfamilyCourt enterprise kiforComplaintTruelow¶54: "This complaint refers to the 'association in fact' between Family Court, also including its practicing attorneys or 'trusted officers,' its Guardian ad Litems ('GALs'), its supervised visitation centers, etc., and the other Defenda…18 U.S.C. § 1962(c)
4EmployedOrAssociatedfamilyCourt enterprise kiforComplaintTruelow¶ 54: 'This complaint refers to the "association in fact" between Family Court, also including its practicing attorneys or "trusted officers," its Guardian ad Litems ("GALs"), its supervised visitation centers, etc., and the other Defend…18 U.S.C. § 1962(c)
5ConductsOrParticipatesfamilyCourt enterprise kiforComplaintTruelow¶57: "Family Court is the de facto 'hub' of this Enterprise, with all the other Defendants being the service provider 'spokes.' This coherent group 'works' together, with the members knowing the general nature of the Enterprise and that …18 U.S.C. § 1962(c)
8ProximateCausefather kiforActs kiforComplaintTruehigh¶76: 'Despite Father being the only targeted person, 2 colluding Mothers, 3 independent Family Court dockets...' — plaintiff is the sole, direct target of the predicate acts, not a competitor/supplier/shareholder of a direct victim (dist…18 U.S.C. § 1964(c)
10HasSharedPurposeenterprise kiforComplaintTruemedium¶ 55 — This Enterprise has (1) a shared purpose of investigating, determining, and enforcing child support payments (and then collecting the federal reimbursements); ... and (3) all the members depending on and working in concert/coordin…
11HasOngoingRelationshipsenterprise kiforComplaintTruemedium¶ 55(3) — all the members depending on and working in concert/ coordination with each other to pursue the shared interest (incentivized by professional fees).
12HasLongevityenterprise kiforComplaintTruelow¶ 55 — This Enterprise has (1) a shared purpose of investigating, determining, and enforcing child support payments (and then collecting the federal reimbursements); (2) a charter, continuity, and longevity of its structure; and (3) all …
13DistinctFromPatternenterprise kiforComplaintTruemedium¶ 55 — This Enterprise has (1) a shared purpose of investigating, determining, and enforcing child support payments (and then collecting the federal reimbursements); (2) a charter, continuity, and longevity of its structure; and (3) all …
14SharesPurposeact3 act10 kiforComplaintTruelow¶33 — The U.S. District Court noted, “Put more simply, [he] maintains that Family Court, on multiple crucial occasions, deliberately failed to notify [him] of its rulings, which resulted in [Father] not being able to appeal the same” on …
15SharesParticipantsact3 act10 kiforComplaintTruelow¶33 (lines 519-526) — The U.S. District Court noted, "Put more simply, [he] maintains that Family Court, on multiple crucial occasions, deliberately failed to notify [him] of its rulings, which resulted in [Father] not being able to appe…
16SharesVictimsact3 act10 kiforComplaintTruelow¶33 (lines 524-526) — Family Court, on multiple crucial occasions, deliberately failed to notify [him] of its rulings, which resulted in [Father] not being able to appeal the same on 11/22/2022.
17SharesMethodsact3 act10 kiforComplaintTruemedium¶69 / ¶933 — Family Court deliberately omitted to notify Father altogether (allegedly to preempt appeals).
18ClosedEndedContinuitykiforActs kiforComplaintTruelow¶ 74 — These Racketeering Activities started ~10 years before the first claims and continued through related acts, thus forming § 1961 (5) patterns of racketeering.
19OpenEndedContinuitykiforActs kiforComplaintTruelow¶ 78 — As adjudging complaints of contempt re: in-arrears child supports are part of Family Court's regular way of conducting its business ..., the threat of open-ended continuity, i.e., “all past conduct that by its nature projects into…
20IsEnumeratedOffenseact1 kiforComplaintTruelow¶ 38 — Since the secret 12/5/2013 “gatekeeper” order -- deliberately concealing Father’s exhaustive “Offer of Proof” documentation submitted on 11/25/2013 --, the Family Court’s manifested objective had been to effectively erase all of F…
21PleadedWithParticularityact1 kiforComplaintFalsemedium¶ 34 — The Family Court's capricious or never communicated ad hoc 'gatekeeper' orders are arbitrary, untraceable, and unappealable
22HasFederalProceedingNexusact1 kiforComplaintFalselow¶ 38 — Since the secret 12/5/2013 "gatekeeper" order -- deliberately concealing Father's exhaustive "Offer of Proof" documentation submitted on 11/25/2013 --, the Family Court's manifested objective had been to effectively erase all of F…
23IsEnumeratedOffenseact2 kiforComplaintTruelow¶ 34 — stripping him of his protecting legal custody of his children on 2/3/2014. Predictably, this occurred after the first “gatekeeper” orders were issued by Family Court on 12/5/2013.
24PleadedWithParticularityact2 kiforComplaintFalsemedium¶135 — 12/5/2013 when Family Court omitted mailing the above, thus, unappealable denial. Father learned about it only after 6/30/2014.
25HasFederalProceedingNexusact2 kiforComplaintFalselow¶ 34 (lines 536–544) — all the meticulously documented systemic child abuses/agenda-driven parental alienations were effectively concealed when the Family Court discarded Father's submitted filings -- while stripping him of his protectin…
26IsEnumeratedOffenseact3 kiforComplaintTruemedium¶ 33 (lines 524–526), p. 11 — Family Court, on multiple crucial occasions, deliberately failed to notify [him] of its rulings, which resulted in [Father] not being able to appeal the same” on 11/22/2022.
27PleadedWithParticularityact3 kiforComplaintFalsemedium¶33 (page 11, line 524-526), dated 11/22/2022 — Family Court, on multiple crucial occasions, deliberately failed to notify [him] of its rulings, which resulted in [Father] not being able to appeal the same
28HasFederalProceedingNexusact3 kiforComplaintFalselow¶ 33 — Family Court, on multiple crucial occasions, deliberately failed to notify [him] of its rulings, which resulted in [Father] not being able to appeal the same
29IsEnumeratedOffenseact4 kiforComplaintTruelow¶ 43 — SJC-13427 ruled in an endlessly circular fashion on 8/8/2023: a) “to the extent he challenges the entry of interlocutory ‘gatekeeper’ orders... he could seek reconsideration of those orders” -- which is not possible in the purpose…
30PleadedWithParticularityact4 kiforComplaintFalsemedium¶ 43 (pp. 14-15) — to the extent he challenges the entry of interlocutory 'gatekeeper' orders... he could seek reconsideration of those orders -- which is not possible in the purposeful absence of the actual orders
31HasFederalProceedingNexusact4 kiforComplaintFalselow¶ 43 — SJC-13427 ruled in an endlessly circular fashion on 8/8/2023: a) "to the extent he challenges the entry of interlocutory 'gatekeeper' orders... he could seek reconsideration of those orders" -- which is not possible in the purpose…
32IsEnumeratedOffenseact5 kiforComplaintTruemedium¶ 39(b) — The silent -- without notice -- online revelation by Family Court on 4/20/2024 of the prior secret, i.e., manifestly discrimination-concealing, “gatekeeper” order from 12/5/2013
33PleadedWithParticularityact5 kiforComplaintFalsemedium¶ 39(b) — The silent -- without notice -- online revelation by Family Court on 4/20/2024 of the prior secret, i.e., manifestly discrimination-concealing, “gatekeeper” order from 12/5/2013;
34HasFederalProceedingNexusact5 kiforComplaintFalsemedium¶ 39b — The silent -- without notice -- online revelation by Family Court on 4/20/2024 of the prior secret, i.e., manifestly discrimination-concealing, “gatekeeper” order from 12/5/2013;
35IsEnumeratedOffenseact6 kiforComplaintTruelow¶ 39c (p. 13) — The SJC's confirmation on 5/31/2024 of the implied invidious mail/wire fraud, ongoing falsified Family Court dockets, and, hence, Father's repeatedly sabotaged direct appeals.
36PleadedWithParticularityact6 kiforComplaintFalsemedium¶ 39(c) — The SJC's confirmation on 5/31/2024 of the implied invidious mail/wire fraud, ongoing falsified Family Court dockets, and, hence, Father's repeatedly sabotaged direct appeals.
37HasFederalProceedingNexusact6 kiforComplaintFalselow¶ 39c (lines 591–593) — The SJC's confirmation on 5/31/2024 of the implied invidious mail/wire fraud, ongoing falsified Family Court dockets, and, hence, Father's repeatedly sabotaged direct appeals.
38IsEnumeratedOffenseact7 kiforComplaintTruelow¶ 18 (p. 7) — the AGO knowingly deceived in Superior Court on 11/5/2024 despite the evidence: ... [he] claims that he mailed documents to the court, but those documents 'then disappeared with no trace before the judges reviewed his filin…
39PleadedWithParticularityact7 kiforComplaintFalsemedium¶ 18 — That is, the AGO knowingly deceived in Superior Court on 11/5/2024 despite the evidence:
40HasFederalProceedingNexusact7 kiforComplaintFalselow¶ 18 — That is, the AGO knowingly deceived in Superior Court on 11/5/2024 despite the evidence
41IsEnumeratedOffenseact8 kiforComplaintTruelow¶ 14 (lines 240-244) — The Family Court deceivingly 'allows' Father's [e-filed] requests for permission to file the 77-page-long documents, only to docket a [mere two] meaningless pages. With [all] the 437 uncontested facts erased from t…
42PleadedWithParticularityact8 kiforComplaintTruemedium¶ 15 (embedded testimony, p.5-6) — The Family Court deceivingly 'allows' Father's [e-filed] requests for permission to file the 77-page-long documents, only to docket a [mere two] meaningless pages. With [all] the 437 uncontested facts e…
43HasFederalProceedingNexusact8 kiforComplaintFalselow¶ 14 (lines 240-246) — The Family Court deceivingly 'allows' Father's [e-filed] requests for permission to file the 77-page-long documents, only to docket a [mere two] meaningless pages. With [all] the 437 uncontested facts erased from t…
44IsEnumeratedOffenseact9 kiforComplaintTruelow¶ 14 — the 6 justices named in 12 motions for relief [from fraud on the court e-filed on 3/26, 3/31, 4/6, and 4/28/2025] can claim 'no facts.'
45PleadedWithParticularityact9 kiforComplaintFalsemedium¶ 149 — Father could never prove that Family Court explicitly discarded (or effectively erased) his mailed pleadings and evidence as mere “garbage.”
46HasFederalProceedingNexusact9 kiforComplaintFalselow¶14 (lines 246–248) — the 6 justices named in 12 motions for relief [from fraud on the court e-filed on 3/26, 3/31, 4/6, and 4/28/2025] can claim 'no facts.'
47IsEnumeratedOffenseact10 kiforComplaintTruelow¶ 15 (lines 294-298) — during the 7/21/2025 Title VI hearing, Family Court demanded that Father furnish the mothers' signatures stipulating the "uncontested-ness" of 437 comprehensive facts
48PleadedWithParticularityact10 kiforComplaintFalsemedium¶ 15 (complaint lines 296–298) — during the 7/21/2025 Title VI hearing, Family Court demanded that Father furnish the mothers' signatures stipulating the "uncontested-ness" of 437 comprehensive facts
49HasFederalProceedingNexusact10 kiforComplaintFalselow¶ 15 (p. 6) — during the 7/21/2025 Title VI hearing, Family Court demanded that Father furnish the mothers' signatures stipulating the "uncontested-ness" of 437 comprehensive facts
rico-hier § 1962(c) (hierarchical) — 29 of 49 True.

Metrics

frameworkCount
5
frameworksPresent
2
runsTotal
19
runsAccepted
13
runsRejected
6
uscEncodedSections
135
uscTierA
74
uscTierB
36
uscTierC
25
uscTitlesTouched
5
uscTitleUniverse
58
uscSectionUniverse
62831
uscUniversePct
0.2149
latestRunId
kifor_rico_hier
latestRunAt
2026-06-21T16:07:13Z
latestVerdict
REJECTED
latestProofGraphUrl
https://qnarre.quantapix.com/proof-graph/run/kifor_rico_hier/debug/