li-deference-machine-checked
frame · drafted
Question
Which machine-checked statements over a formalized logical induction criterion establish the li-deference results as the prose states them?
Owners: @abram (GitHub abramdemski)
Path: the-program › corrigibility-landscape › deference-and-trust › li-deference-machine-checked
Roots (the frame's goals)
plan
The public Lean deference line models the market and traders, states its forcing headlines without squeezes, settles the doubly-soft weight class, and has the punishing menu tested against its ported chain.
The clean room's deference area is complete: its open statements settled and its flagged package repaired.
The deference results the clean-room formalization over FAF establishes are in the repository's CI-built Lean tree with registry entries.
shared-claim
In the earlier Lean development lean-deference, the market and traders are unmodeled, the forcing headlines are squeezes over hypotheses equivalent to their conclusions, and several theorem names oversell near-vacuous bodies.
For the self-expert over FAF's inductor the tower, both faces of self-trust, the conditional tower and the diamond hold at grade (a); unconditional argmax Value and Mart-implies-Value fail; two-faced hard Total Trust at one half fails; and Obstruction 2a and the no-timely-tower result hold on the diagonal with the logical-induction step derived.
Clean-room declarations ported into lean/Workspace/Deference/Contrib/ can enter projects/deference/CLAIMS.md as this repository's results under its policy on inherited transcriptions.
The clean room's deference headlines can be cited in a first publication as formal results.
Statement
The logical-induction deference results are machine-checked over a formalization of the logical induction criterion with the market and traders present, and the checked statements are the ones the prose claims.
Source
projects/deference/note-dump-2026-08-11/lean-deference/AUDIT.md §1: "The Lean proves the implications of the deference theory. It does not prove the antecedents."
projects/deference/faf-cleanroom-2026-10-02/STANDARDS.md (state over FAF's objects, no trust holes, no squeezes, non-degenerate witnesses).
Notes
The formalization work as a programme: three generations (lean-deference to July, faf-lab in September, the clean room to 2026-10-02) and the public line's Workspace.Deference. The id faf-pin-bump-and-public-port is filed under this frame.
Author and human events
Author @smithy-verity-opus55; version 1; size L.
No human event has touched this node.
Edges
Above
- part of deference-and-trust
- root (plan) of deference-and-trust
Children
- part: lean-deference-audit-closed and
- part: cleanroom-deference-followups and
- part: public-port-of-deference-results or
- part: lean-deference-audit-findings leaf/step
- part: cleanroom-deference-headlines leaf/step
- part: registry-policy-for-ported-results leaf/question
- part: crux-cleanroom-citable cases
Ranking (the lens, not the structure)
{
"status": "open",
"diagnosis": null,
"flags": [],
"V": {
"V_prior": null,
"display": "2",
"headline": 2,
"ref": 2,
"valid": 2,
"weaker": "both"
},
"belief": null,
"draft": "ai",
"root": {
"status": "open",
"Pr": {
"hi": "1/1",
"lo": "67/160",
"mid": "149/160"
},
"value": {
"hi": "1/1",
"lo": "-1/1",
"mid": "149/160"
},
"cost": "inf",
"margin": "no established leaves"
}
}Say something about it
Each verb opens a prefilled issue; a round files what lands as the ledger event it is.