mart-implies-value-kernel

Bridge card

A conjunct of the informal claim li-deference-collapse: For a novice logical inductor and an inductor expert whose day-n estimates are published decided facts, Total Trust of the novice in the expert over the gap-closed class of expert-referencing bets implies Mart (the tower) on that class, and Mart on that class implies Value (argmax deference on menus drawn from it).

Declaration DeferenceArgmax.value_argmax_asymptotic (record mart-implies-value-kernel.record)

Hypotheses, read:

• tt-implies-mart-gap-bets : For an observable, coherent, introspective expert and a bet class D closed under the gap construction Z ↦ Z − ⌜E*(Z)⌝ and under negation, Total Trust of the novice in the expert over D implies Mart on D: for every Z in D, E^H_n(Z) ≈_n E^H_n(⌜E*(Z)⌝).
  The pictures are readings of the theorem's setting: the surrogate expert with exact, provably linear expectations; the inductor expert with asymptotic introspection; Total Trust granted only over parallel cuts of single bets; and a residual. The asymptotic-introspection row conditions on the repair tt-mart-repair-via-bounds-transfer (a conditional table): its conditional splits into the probability of the conclusion if the repair holds and if it fails, so tracing the repair moves this row without a new picture. The two independent verifications the page's status line reports were wiki-level AI passes; they mint no level here, and no human has traced the proof.
• expert-knows-own-estimates : For every formula that case-splits on the expert's own published estimates, the expert's estimate of the formula equals the value obtained by resolving the case-split with those estimates.
  Shared by both roots and by the kernel result's hypotheses; for an inductor expert it holds only asymptotically, which is what the asymptotic-introspection picture of the prose theorem exploits.
• tie-break-ledger-decided : The rule selecting among equal-maximal menu options is computable from the published estimates and the ledger, so the followed strategy is an efficiently describable logically uncertain variable whose value the expert's estimate places at the maximum.
  Discharges part of hUM_S. The page's counterexample shows a definable but undecidable rule breaks F1 by correlation and, with an adversarial rule, breaks Value itself.
• novice-expprovind proved-in-model: The novice's expectations satisfy expectation provability induction (Theorem 4.8.10 of the logical induction paper): a bounded identity or inequality between efficiently describable logically uncertain variables that is provable in Γ is carried through E^H_n asymptotically.
  Discharges hMon. The model that proves it is the logical induction paper's: the novice is a logical inductor by the setting, and the theorem holds for every logical inductor.

Completeness (mart-implies-value-kernel.complete): No premise beyond the kernel-checked composition, its bridge and the four listed discharging claims is needed for Value to hold on menus drawn from the gap-closed class.

What remains (li-deference-collapse.improvable)

The logical-induction deference collapse, in which Total Trust implies the tower and the tower implies Value, can be improved until it reflects a human epistemic process deferring to a distinct, faster AI inductor it gives feedback to, on questions that may mention the AI's outputs well.

• route-collapse-regularity-scope: Restricting the Value arrow to menu sequences whose chooser satisfies REGULARITY, as the maintainer's deck states it, gives a version of the collapse that holds for a human inductor deferring to a distinct AI inductor on non-trivial menus.
• route-collapse-hedged-value: Replacing argmax Value by δ-hedged Value removes the tie-break and conditional-stability premises, and the hedged collapse holds for a human inductor deferring to a distinct AI inductor whose ramp quotes the human can price.
• route-collapse-policy-level: A policy-level analogue of Total Trust, for an AI trained to act whose policy the humans trust directly, yields a version of the collapse with no selection to condition on.
• route-collapse-distinct-expert: Transporting both arrows between Total Trust and the tower, the conditional tower and the scoped Value corner from the self-expert to a distinct novice reading an inductor expert with asymptotic self-knowledge keeps the collapse with one stated hypothesis per arrow.
• route-collapse-scheduled-grade: Weakening the per-day grade to scheduled weighted averages, the grade at which the cross-process results hold, gives a version of the collapse whose Value arrow holds over arbitrary efficiently describable menus with no scope condition.
• route-collapse-quote-free: Restricting the question families to those that do not mention the AI's quotes keeps the pointwise tower out of reach of the Gödel-coin diagonal, and a version of the collapse holds there for a human inductor deferring to a distinct AI inductor.
• li-deference-collapse.residual (residual): A refinement of the collapse that none of the other routes describes reflects a human epistemic process deferring to a distinct, faster AI inductor it gives feedback to.