thin-value-of-thick

Bridge card

A conjunct of the informal claim public-legitimacy-theory: The public repository defines legitimacy at two levels, a thin specification (correct, sufficient, value) on a finite setting with her prior, model, actual process and a baseline, and a thick definition (Integrity, authorship, Robust Openness, transparency), and proves that the thick conditions satisfy the thin specification.

Declaration Workspace.Deference.Contrib.ThinLegitimacy.value_of_thick in lean/Workspace/Deference/Contrib/ThinLegitimacy.lean (record thin.value-of-thick.record)

Registry thin.value-of-thick: class lean-proved, status active, review ci-only, origin round 2026-10-01-thin-legitimacy-and-effective-authority; bears on item 107

Hypotheses: unread (the record's Source carries the signature; a reader files them).

Completeness (thin.value-of-thick.complete): No premise beyond the signature's binders enters the declaration; the kernel checks it as stated. The result is the record, this leaf and the bridge, and its hypotheses are unread: the record's Source carries the signature verbatim and no hypothesis leaf is filed until a reader files one.

What remains (public-legitimacy-improvable)

The thick and thin legitimacy theory, stated on finite settings with a parameter baseline, can be improved until it reflects legitimacy between a human principal and an AI over real channels well.

• item-109: The thin preservation theorem holds in asymptotic form for a logical-inductor principal whose self-trust is asymptotic and whose program is not a posterior: with the inductor's conditional self-trust as the hypothesis on her model and transparency as the actual record generated as the model says, the actual process satisfies the same self-trust in the limit. — this is item 109
• item-110: The baseline, what would have reached her without anyone's interested interference, has a definition from which the eight-world model's cases are derived rather than declared. — this is item 110
• item-108: The thin properties have a form for valuations with no outside fact to be correct about, and the thick conditions deliver them. — this is item 108
• task-items-53-59: The reason-state blockers of PRIORITIES items 53, 55 and 59 are closed. — item 53, 55, 59
• task-items-61-66: The enforcement and inquiry blockers of PRIORITIES items 61 to 66 are closed, with the inertness dichotomy and Grounded Replay in Lean. — item 62, 66
• task-items-67-73: The authority, provenance and improvement blockers of PRIORITIES items 67 to 73 are closed, with the due-activation term built and the improvement baseline defined. — item 71, 73
• task-reconcile-canonical-pointer: The repository has a single canonical entry point for the legitimacy programme.
• public-legitimacy-improvable.residual (residual): The public legitimacy theory improves toward real channels by a route none of the named ones describes.