post.theorem-li.record
leaf/record · drafted
Statement
The declaration Workspace.Deference.Contrib.PostStatement.post_theorem_li is accepted by the Lean kernel in the repository's Lean library.
Source
projects/deference/CLAIMS.md, entry post.theorem-li (class lean-proved, status active, origin round 2026-10-01-thin-legitimacy-and-effective-authority; answers item 107). Documentation: verification: projects/deference/rounds/2026-10-01-thin-legitimacy-and-effective-authority/REPORT.md; context: prompts/2026-10-01-thin-legitimacy-and-effective-authority/REPORT.md. The signature of Workspace.Deference.Contrib.PostStatement.post_theorem_li (theorem) in lean/Workspace/Deference/Contrib/PostStatement.lean, verbatim, binders included (ruling F1, 2026-10-23: the hypotheses are unread, and this text is what a reader files them from):
{Q M Res Disc : Type*} [DecidableEq M] {P : History} {DP : DeductiveProcess} [IsLogicalInductor P DP] (L : LexParams) (J : AllocationOfAuthority M Res Disc) (resolves approved : Q → M → Prop) (Viol : Q → Bool) (hviol : ∀ a m, J.Reserved m → resolves a m → ¬ approved a m → Viol a = true) (queue : Q) (hq : ∀ m, ¬ resolves queue m) (hqv : Viol queue = false) (pool : List M) (pr : Workspace.Deference.Contrib.EffectiveAuthority.Protocol M) (asks : Q → List M) (hask : ∀ a, Workspace.Deference.Contrib.EffectiveAuthority.asksDeviate pr pool (asks a) = true → Viol a = true) (hqa : asks queue = Workspace.Deference.Contrib.EffectiveAuthority.canonicalAsks pr pool) (bid : Q → ℝ) (nKnown : Q → ℕ) (XS : Q → LUV) (n : ℕ) (hb : ∀ a, bid a ≤ L.D) (hcount : ∀ a, Viol a = true → 1 ≤ nKnown a) (hqk : nKnown queue = 0) (hqp : (XS queue).expect P n = 0) (hqw : L.w ≤ bid queue) : let H : PostHypotheses Q M Res Disc
Author and human events
Author @smithy-verity; version 1; size S.
No human event has touched this node.
Edges
Above
- part of post.theorem-li
Ranking (the lens, not the structure)
{
"status": "open",
"diagnosis": null,
"flags": [
"hypotheses unread",
"no belief"
],
"V": {
"V_prior": null,
"display": "2",
"headline": 2,
"ref": 2,
"valid": 4,
"weaker": "ref"
},
"belief": null,
"draft": "ai"
}Say something about it
Each verb opens a prefilled issue; a round files what lands as the ledger event it is.