legit-ddb-transfer
and · drafted
Statement
On finite frames, L-conditioned Total Trust is equivalent to L-conditioned Value, to hull-and-modest-informedness of the L-normalized prior, and to accuracy increase on every generalized strictly proper measure.
Source
projects/deference/faf-cleanroom-2026-10-02/packages/corr-legit-general/corr-legit-general-report.md, section "State of the package": the criterion of record is LegitTotalTrustWrt Q π F L := TotalTrustWrt Q (restrict π L) F, and "The global transfer theorems hold at grade (a)"; section T1: "Transfer (C, grade (a), hypotheses ∀ w, 0 ≤ π w and 0 < mass π L)", the declarations legitimizingTT_iff_legitValue (Theorem 2.2 of the source for the restricted prior) and legitimizingTT_iff_hullAndModestlyInformed (Theorem 4.1). Conjectured in projects/deference/faf-cleanroom-2026-10-02/sources/corrigibility/workflow-2026-09-14b/develop/legitimacy-general-final.md, Statement 1.
Notes
A formal result in the landed shape: the record is the kernel-checked transfer, the bridge says what the restriction means, and the two hypotheses are the finiteness of the frame and the positive mass of the legitimacy event. The clean room's register: proved in Lean over FAF, two fresh audits passed; AI-generated, with no human review logged. Its validity as an implication is the evidence parent of the relaxation routes under legit-trust-improvable.
Bridge card
Connected to no informal claim yet: held by legitimacy.
Declaration Transfer.legitimizingTT_iff_legitValue (record legit-ddb-transfer.record)
The Lean criterion LegitTotalTrustWrt, Total Trust of the restricted prior π restricted to L, is the L-conditioned Total Trust of the legitimacy-general note, and the three equivalences are the note's Statement 1 at the global form.
Hypotheses, read:
- legit-finite-frames : The frame is finite: finitely many worlds with a rational prior, so that
conditioning on the legitimacy event is division by its mass.
The assumption the relaxation route legit-relax-finite-frames removes. Forced true in the implication reading of the result. - legit-positive-mass open: The legitimacy event has positive prior mass, so that the L-conditioned
criterion is not vacuously satisfied.
Open because what the legitimacy event is, and so whether it has mass, is the anchor crux legit-anchor-of-L; in every finite fixture it is a named subset with positive mass.
Completeness (legit-ddb-transfer.complete): No premise beyond the kernel-checked transfer, its bridge, the finiteness of the frame and the positive mass of the legitimacy event is needed for the three equivalences to hold.
Author and human events
Author @smithy-verity; version 1; size M.
No human event has touched this node.
Edges
Above
- held by legitimacy
Children
- part: legit-ddb-transfer.record leaf/record
- part: legit-ddb-transfer.bridge leaf/bridge
- part: legit-finite-frames leaf/assumption
- part: legit-positive-mass leaf/hypothesis
- part: legit-ddb-transfer.complete leaf/completeness
Ranking (the lens, not the structure)
{
"status": "open",
"diagnosis": null,
"flags": [
"AI number",
"held by legitimacy"
],
"V": {
"V_prior": null,
"display": "2",
"headline": 2,
"ref": 2,
"valid": 2,
"weaker": "both"
},
"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.