legit-ddb-transfer.bridge
leaf/bridge · drafted
Statement
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.
Source
projects/deference/faf-cleanroom-2026-10-02/packages/corr-legit-general/corr-legit-general-report.md, section T1: "The global form is corr-reflect-frames' LegitimizingTT, reached by legitTotalTrustWrt_id_iff" and the vacuity remark "legitTotalTrustWrt_empty : LegitTotalTrustWrt Q π F ∅ — hence 0 < mass π L on every conditioned headline".
Notes
Stated by the formalizer; the note's author is an agent, and no human confirmation of the reading is logged. The package's T4 finding says the local form with DDB's own definition of Value behaves differently, so the bridge holds for the global form only.
Author and human events
Author @smithy-verity; version 1; size S.
No human event has touched this node.
Edges
Above
- part of legit-ddb-transfer
Ranking (the lens, not the structure)
{
"status": "open",
"diagnosis": null,
"flags": [
"AI number",
"attribution unvetted"
],
"V": {
"V_prior": null,
"display": "2",
"headline": 2,
"ref": 2,
"valid": 2,
"weaker": "both"
},
"belief": {
"J": 0,
"mid": "43/50",
"range": [
"9/25",
"1/1"
],
"width": "1/1"
},
"draft": "ai"
}Say something about it
Each verb opens a prefilled issue; a round files what lands as the ledger event it is.