legit-ddb-transfer.record
leaf/record · drafted
Statement
The declarations Transfer.legitimizingTT_iff_legitValue, Transfer.legitimizingTT_iff_hullAndModestlyInformed and Transfer.legitimizingTT_iff_epistemicValue in Cleanroom.Corrigibility.CorrLegitGeneral are accepted by the Lean kernel under the package's gate.
Source
projects/deference/faf-cleanroom-2026-10-02/packages/corr-legit-general/corr-legit-general-ledger.md (the three declarations) and corr-legit-general-report.md, "Gate: PASS" (2910 declarations; axioms propext, Classical.choice, Quot.sound).
Notes
The public package carries the report, ledger, findings and audit files, not the Lean sources. Without a claims-registry entry the record's own validity level caps at 2; a human map-read lifts it.
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",
"not in a claims registry"
],
"V": {
"V_prior": null,
"display": "2",
"headline": 2,
"ref": 2,
"valid": 2,
"weaker": "both"
},
"belief": {
"J": 0,
"mid": "47/50",
"range": [
"11/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.