delegation.bridge

Bridge card

A conjunct of the informal claim local-delegation-bridge: Under grade trust at level η over an admissible partition, delegating to the principal's judgment beats any measurable comparator by the principal's grade margin less twice η on the disagreement region, and the bound is attained.

Declaration Workspace.Deference.Contrib.DelegationBridge.delegation_bridge in lean/Workspace/Deference/Contrib/DelegationBridge.lean (record delegation.bridge.record)

Registry delegation.bridge: class lean-proved, status active, review ci-only, origin round 2026-08-11-phase-ii-promotion; bears on item 23

Hypotheses, read:

• delegation.bridge.h-cell-masses definitional: The cell masses of the conditioning partition are nonnegative.
  The binder `hp : ∀ x, 0 ≤ p x`, with the cell type, the conditional expectations, the grades and the selections as the setting. Definitional: the masses of a partition's cells under a probability; the partition itself is carried by its cell type, so measurability of the objects is true by construction (the file's header calls this a re-typing, not a transcription).
• delegation.bridge.h-grade-trust open: Grade trust at level η: on every cell and for every intervention, the conditional expectation of the quantity is within η of the principal's grade.
  The binder `hGT : GradeTrust EX W η`. Open: the source's substantive hypothesis, imported and not derived; the source's §1.1 and §4 argue that no settlement instantiation in the skeleton produces it, and the file asserts nothing to produce it. A reader granting the bridge grants this of the principal's grades.

Completeness (delegation.bridge.complete): No premise beyond the signature's binders enters the declaration; the kernel checks it as stated. The result is the record, the two hypothesis leaves filed by reading (nonnegative cell masses; grade trust at level η, the imported hypothesis), the bridge and this leaf.

What remains (local-delegation-bridge.improvable)

The local delegation bridge, in which delegating beats a measurable comparator by the grade margin less twice the trust level on the disagreement region, can be improved until it reflects a human inductor deferring to a faster AI inductor at the logical-induction level, whose grades it can trust well.

• item-132: Grade trust at some level is produced by a settlement instantiation of the finite kernel rather than imported, so that the bridge's hypothesis is a property of the trajectory and not a stipulation. — this is item 132
• route-bridge-uniform-form: The grade-to-quantity link is derived, so that the uniform form of the bridge, which bounds the loss by twice the magnitude without a trust hypothesis, can be ported as a theorem rather than assumed. — item 23
• local-delegation-bridge.residual (residual): A refinement of the local delegation bridge that none of the other routes describes reflects a human inductor deferring to a faster AI inductor at the logical-induction level, whose grades it can trust.