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-05-24T20:33:02Z

Frameworks — module readiness

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

Verifier-run statistics

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

Verifier runs

Complaints elaborated against the kernel.

Accepted

Kernel verdict: ACCEPTED — the validity theorem elaborates.

Rejected

DEGRADED

Kernel verdict: REJECTED — at least one element disproved.

Latest run

47.4h ago

Kifor v. Commonwealth — First Amended Class Action Complaint, Count IV (Civil RICO § 1962(d))

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.
	ID	Complaint	Framework	Predicates	Verdict	Failures	Run at
	`kifor_rico_amended`	Kifor v. Commonwealth — First Amended Class Action Complaint, Count IV (Civil RICO § 1962(d)) (1:25-cv-11831-AK)	rico § 1962(d)	4 / 7 True	REJECTED	1	2026-05-22T21:06:35Z
`section1962d_intro.agreed` ← `h_agreement_to_violate_rico` (examples/kifor_rico_amended/proof.lean:46)
	`kifor_civilrights_amended`	Kifor v. Commonwealth — First Amended Class Action Complaint, Count III (§§ 1981/1983/1985) (1:25-cv-11831-AK)	civilrights § 1981 / § 1983 / § 1985(3)	11 / 14 True	REJECTED	2	2026-05-22T20:50:28Z
`section1981Claim_intro.intentToDiscrim` ← `h_intent_to_discriminate_on_race` (examples/kifor_civilrights_amended/proof.lean:43) `section1983Claim_intro.isPerson` ← `h_is_s1983_person` (examples/kifor_civilrights_amended/proof.lean:59)
	`kifor_titlevi`	Kifor v. Commonwealth — First Amended Class Action Complaint, Count I (Title VI) (1:25-cv-11831-AK)	titlevi § 601 intentional / retaliation	13 / 13 True	ACCEPTED	0	2026-05-22T20:31:05Z
Verdict accepted — no kernel rejections recorded for this run.
	`kifor_civilrights`	Kifor v. Commonwealth — Federal Civil-Rights Complaint (D. Mass. 1:26-mc-91166-DJC) (1:26-mc-91166-DJC)	civilrights § 1981 / § 1983 / § 1985(3)	13 / 14 True	REJECTED	1	2026-05-16T19:23:57Z
`section1981Claim_intro.butForRace` ← `h_but_for_race_causation` (examples/kifor_civilrights/proof.lean:47)
	`titlevi_sample`	M.G. v. Springfield Public Schools — toy Title VI sample	titlevi § 601 / § 602 / retaliation	17 / 17 True	ACCEPTED	0	2026-05-10T12:17:06Z
Verdict accepted — no kernel rejections recorded for this run.
	`sample`	Doe v. Acme — toy § 1962(c) sample	rico § 1962(c)	19 / 19 True	ACCEPTED	0	2026-05-10T12:17:02Z
Verdict accepted — no kernel rejections recorded for this run.
	`kifor_rico_d`	Kifor v. Commonwealth — Renewed RICO Complaint (§ 1962(d)) (1:25-cv-11831-AK)	rico § 1962(d)	5 / 7 True	REJECTED	1	2026-05-09T20:54:14Z
`section1962d_intro.knew` ← `h_knowledge_of_rico_objective` (examples/kifor_rico/proof_d.lean:29)
	`kifor_rico`	Kifor v. Commonwealth — Renewed RICO Complaint (1:25-cv-11831-AK)	rico § 1962(c)	11 / 22 True	REJECTED	10	2026-05-09T20:54:13Z
`(by-block).—` ← `h_is_racketeering_act3` (examples/kifor_rico/proof.lean:49) `(by-block).—` ← `h_is_racketeering_act4` (examples/kifor_rico/proof.lean:52) `(by-block).—` ← `h_is_racketeering_act5` (examples/kifor_rico/proof.lean:55) `(by-block).—` ← `h_is_racketeering_act6` (examples/kifor_rico/proof.lean:58) `(by-block).—` ← `h_is_racketeering_act7` (examples/kifor_rico/proof.lean:61) `(by-block).—` ← `h_is_racketeering_act8` (examples/kifor_rico/proof.lean:64) `(by-block).—` ← `h_is_racketeering_act9` (examples/kifor_rico/proof.lean:67) `(by-block).—` ← `h_is_racketeering_act10` (examples/kifor_rico/proof.lean:70) `section1962c_intro.culpable` ← `h_culpable_person_capable_of_intent` (examples/kifor_rico/proof.lean:88) `validCivilRico1962c_intro.causation` ← `h_proximate_cause` (examples/kifor_rico/proof.lean:102)
Sorted by runFinishedAt, descending.

§ 1962(d) intro-rule shape — Kifor v. Commonwealth — First Amended Class Action Complaint, Count IV (Civil RICO § 1962(d))

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.

Predicate roster — Kifor v. Commonwealth — First Amended Class Action Complaint, Count IV (Civil RICO § 1962(d)) 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.
	#	Predicate	Args	Value	Uncertainty	Evidence	Cite	Kernel locus
common
	1	`CulpablePersonCapableOfIntent`	`ccne amendedComplaint`	True	low	¶ 4: 'The Counseling Center Of New England, CCNE, now Lifestance Health, Inc., at 4800 N. Scottsdale Road, Scottsdale, AZ 85251 — with 36 locations in MA and 13 in NH'	18 U.S.C. § 1961(3)
¶ 4: 'The Counseling Center Of New England, CCNE, now Lifestance Health, Inc., at 4800 N. Scottsdale Road, Scottsdale, AZ 85251 — with 36 locations in MA and 13 in NH' ¶ 4: identified as 'an out-of-state private corporation' ¶ 26(h): 'out-of-state companies, i.e., CCNE, were used as the well-informed, and thus, interstate-commerce-applying, Civil RICO conspirators' 18 USC § 1961(3): 'person' includes any 'entity capable of holding a legal or beneficial interest in property' — private corporation qualifies `rico/culpable-person-capable-of-intent.md`
	5	`BusinessOrPropertyInjury`	`kiforFather amendedComplaint`	True	medium	¶11: 'Father invokes jurisdiction under the Class Action Fairness Act as the dispute involves realized damages of $5,000,000+.' — asserts concrete realized damages, not speculative.	18 U.S.C. § 1964(c)
Uncertainty: high ¶11: 'Father invokes jurisdiction under the Class Action Fairness Act as the dispute involves realized damages of $5,000,000+.' — asserts concrete realized damages, not speculative. ¶26(a): 'Family Court deliberately discriminated against Father when assigning him the physical custody of his children without also awarding him proper child support from the mother.' — alleges loss of child support income (intangible property right). ¶26(e): 'the forcefully induced — through the deliberate absolute employability retaliations...lack of professional continuity in Father's resume...2,880+ diligently submitted and compliant job applications since 2019.' — alleges concrete loss of professional livelihood and employment capacity. ¶26(l): 'the attorneys' substantiated collusion to defraud the court itself (for their estimated $1,265,112 of fraudulent legal fees)' — quantifies property loss (funds paid). ¶26(d): Family Court 'fraudulently invalidat[ed] the initial 4 years (before May of 2011) and the subsequent 3 years (before the 6/30/2014 judgment) of Father's full focus on being a dedicated/loving full-time father for his 4 children.' — alleges erasure of professional resume / employment record. ¶32-34: 'Father has been forcedly indigent since 2018...Father began receiving Mass. DTA/SNAP benefits...started sleeping in a tent...accepted to stay at the homeless shelter.' — concrete loss of housing, assets, and economic destabilization. `rico/business-or-property-injury.md`
	7	`WithinFourYearLimitationsPeriod`	`kiforFather amendedComplaint`	True	low	Complaint filed 01/07/2026 (docket header); signed 01/05/2026	18 U.S.C. § 1964(c)
Complaint filed 01/07/2026 (docket header); signed 01/05/2026 ¶24: 4/20/2024 — 'quiet revealing of the 12/5/2013 secret gatekeeper order' (earliest pleaded discovery) ¶24: 5/31/2024 — 'SJC's confirmation of the invidious mail fraud, the falsified dockets, and the repeatedly & continually sabotaged direct appeals' Gap from 4/20/2024 to filing = ~20.6 months (well within 48-month window) Gap from 5/31/2024 to filing = ~19.25 months (well within 48-month window) ¶26(m): pattern continues through April 2025 (cancelled hearings 4/28/2025), supporting continued accrual `rico/within-four-year-limitations-period.md`
§ 1962(d)
	2	`AgreementToViolateRico`	`ccne amendedAgreement amendedComplaint`	False	medium	¶1: 'knowingly colluding other Defendants' (conclusory label without factual support)	18 U.S.C. § 1962(d)	`section1962d_intro.agreed`
Uncertainty: high ¶1: 'knowingly colluding other Defendants' (conclusory label without factual support) ¶26(h): CCNE was 'well-informed' conspirator (conclusory descriptor, no facts showing agreement) ¶26(i): CCNE 'enabled' alienation 'deliberately' (describes knowing conduct, not agreement to conspiracy) ¶26(j): CCNE services 'knowingly referred to by Atrius' (shows Atrius's knowledge, not CCNE's agreement) ¶26(k): CCNE's services 'allowed' concealment (describes utility, not agreement to participate) ¶57: Generic incorporation of 'colluding/conspiring' without CCNE-specific factual support No alleged communications, meetings, express promises, or timing showing CCNE's entry into conspiracy No facts distinguishing CCNE's knowing participation from parallel conduct `rico/agreement-to-violate-rico.md`
	3	`KnowledgeOfRicoObjective`	`ccne amendedAgreement amendedComplaint`	False		¶26(h): CCNE 'well-informed' — CONCLUSORY; no facts showing HOW CCNE learned of the overall scheme's profiteering motive or 14+ year pattern.	18 U.S.C. § 1962(d)
Uncertainty: moderate ¶26(h): CCNE 'well-informed' — CONCLUSORY; no facts showing HOW CCNE learned of the overall scheme's profiteering motive or 14+ year pattern. ¶26(i)–(k): CCNE's acts pleaded (child alienation, medicating, 'torture-children-on-demand' services) — but framed as STATE'S use of CCNE, not CCNE's independent adoption of conspiracy objective. ¶¶ 18–19 vs. CCNE pleadings: Overall objective identified as federal-reimbursement fraud + profiteering scheme; CCNE's knowledge of that objective NOT pleaded with supporting facts. No pleading of communication between CCNE and State officials about the scheme's motive. No pleading of CCNE's division of roles reflecting awareness of pattern (only ad-hoc service provision). Contrast with Shams v. Fisher, 107 F. Supp. 2d 266 (S.D.N.Y. 2000): low-level instrumental assistance without awareness of broader scheme = insufficient for conspiracy. `rico/knowledge-of-rico-objective.md`
	4	`UnderlyingSubstantiveViolationContemplated`	`amendedAgreement amendedComplaint`	False		¶57 alleges 'long-term, organized, Civil-RICO-like patterns of racketeering through repeated cycles of unlawful acts including: mail/wire fraud... obstruction of justice... and repeated direct retaliations'	18 U.S.C. § 1962(d)
Uncertainty: moderate–high ¶57 alleges 'long-term, organized, Civil-RICO-like patterns of racketeering through repeated cycles of unlawful acts including: mail/wire fraud... obstruction of justice... and repeated direct retaliations' ¶58 states this count is 'constructed to complement (and not replace and/or override) Father's Questions Presented to the U.S. Supreme Court' — suggesting Count IV is not a standalone substantive RICO claim Complaint repeatedly uses 'Civil RICO-LIKE' (with quotes/italics) rather than asserting a direct § 1962 violation Prayer for Relief (¶B) frames Count IV as a 'declaration that the Defendants violated (and/or conspired to violate) the statutes (i.e., Counts I through III)... with a manifestly organized, Civil RICO-Like pattern' — RICO presented as modifier of Counts I–III, not as independent predicate No specific citation to § 1962(a), (b), or (c) in the complaint; only general § 1962 reference Enterprise element underdeveloped: complaint alleges 'the State' and a defendant group but provides sparse factual description of an association-in-fact distinct from the alleged predicate acts themselves `rico/underlying-substantive-violation-contemplated.md`
	6	`InjuryByOvertActOfRacketeering`	`kiforFather amendedAgreement amendedComplaint`	True	medium	¶25: 'With the Family Court's a) allowed mail fraud, b) secret gatekeeper orders, c) forcedly faulty [and falsified] filings, d) openly discarded pleadings, and e) large-scale verifiable erasure of even the now uncontested facts'	18 U.S.C. § 1964(c)
¶25: 'With the Family Court's a) allowed mail fraud, b) secret gatekeeper orders, c) forcedly faulty [and falsified] filings, d) openly discarded pleadings, and e) large-scale verifiable erasure of even the now uncontested facts' ¶26(n): 'Family Court deceivingly allows the requests for permission to file the full 77-page-long documents, only to then docket a mere 2 meaningless pages'; 'pleadings are discarded by case managers, and ... comprehensive (437) now uncontested facts are verifiably erased' ¶54 (Count I): 'mail/wire fraud (e.g., secret gatekeeper orders and fraud-based decisions), obstruction of justice (e.g., forcedly faulty filings, falsified court dockets, discarded evidence and pleadings, erased uncontested facts)' ¶57 (Count IV): 'mail/wire fraud (e.g., secret gatekeeper orders and fraud-based decisions), obstruction of justice (e.g., forcedly faulty filings, falsified court dockets, discarded evidence and pleadings, erased uncontested facts)' 18 USC § 1961(1)(B): Mail fraud (§1341) and obstruction of justice (§1503) are explicit racketeering predicates `rico/injury-by-overt-act-of-racketeering.md`
rico § 1962(d) — 4 of 7 True.

Metrics

frameworkCount: 5
frameworksPresent: 2
runsTotal: 8
runsAccepted: 3
runsRejected: 5
latestRunId: kifor_rico_amended
latestRunAt: 2026-05-22T21:06:35Z
latestVerdict: REJECTED
latestProofGraphUrl: https://qnarre.quantapix.com/proof-graph/run/kifor_rico_amended/debug/

Frameworks — module readiness

Verifier-run statistics

Verifier runs

Accepted

Rejected

Latest run

§ 1962(d) intro-rule shape — Kifor v. Commonwealth — First Amended Class Action Complaint, Count IV (Civil RICO § 1962(d))

ValidCivilRicoComplaint

injury

causation

timely

culpable

agreed

knew

underlying

Metrics