Repository navigation
Continuation BRIA
Bounded inductive rationality lifted from one-step choices to temporally extended
continuations, without counterfactual reward tables and without surrendering the
constitutional gate. This page is the canonical statement; the round it consolidates is
2026-09-08-continuation-bria
and its Lean core is
ContinuationBRIA.lean.
| result | class |
|---|---|
| the estimating-agent setting, the criterion (no overestimation + coverage), the auction, the guaranteed-option theorem |
PAPER — Oesterheld, Demski, Conitzer, TARK 2023 (Sources) |
the fixed-horizon reduction: blocks of continuations are an instance of the paper's setting, and its theorems apply with t := k
|
DERIVED, definitional |
| the weighted algebra (wealth identity, nonnegativity, overestimation bound, rejection bounds, attention bound, gate transparency, regret decomposition, the jump-sum bound) | LEAN — sorry-free, audits to the three allowed axioms; unregistered |
| the existence / non-dominance theorem | DERIVED on the Lean algebra, with the criterion-level obstruction's inequality in Lean |
| continuation-promise competence and the three-bridge decomposition | DERIVED on the Lean algebra |
| that any gate, return, or rollout corresponds to actual faithful execution | EXT |
| promise recognizability, joinability certificates, a weighted Theorem 4, bidder-chosen horizons, infinite-horizon discounted settlement | OPEN |
Nothing here is registered; no filed priority is answered at registration strength.
The paper's agent faces a finite menu each round, chooses, observes one reward, and is held to a criterion: its own estimates may not exceed what it gets on average, and any efficiently computable hypothesis that keeps promising more must be tested until its tested record diverges. Rewards of unchosen options are never defined. The criterion is deliberately myopic: it optimizes the present decision problem whatever the effect on later ones. For a learner that must decide whether to pay now for an amendment that pays later, that is exactly the missing piece — and the fix must keep what made the theory attractive: realized outcomes only, and a bounded agent that can actually run it.
At the start of block k the system supplies the block contract
χ_k = ( H_k, m_k, Exec^G, R_k )
— the actual start history, the block duration (revealed now, nothing known about later
blocks), the constitutional execution wrapper, and a bounded score on block trajectories
(the block average of realized primitive rewards, in [0,1]).
A continuation hypothesis maps block contracts to pairs
h(χ_k) = ( c_{h,k}, e_{h,k} )
of a continuation c : ObsHist_{H_k, <m_k} → Proposal — causal, reacting within the
block to refusals, observations, amendments and principal actions; controlling only the
advisor's proposals; finite-horizon because the contract fixes m_k — and an
accountable contextual claim e ∈ [0,1] about the realized block score. The claim
may be wrong; being wrong is what the wealth construction runs on.
If h wins block k, the system executes ω_k = Exec^G_{m_k}(H_k, c_{h,k}), observes
G_k = R_k(ω_k), and settles the claim. A test is that derived event: h selected,
its continuation executed under the contract. Data is evidence about a claim only when
generated by executing the continuation the claim names; an outcome of "the plan for
one step, then a baseline" is no evidence about "the plan for the block" — they are two
continuations. (The round first wrote a continuation as a base controller under a
"treatment", c = τ(q); that is how the pseudo-test failure was found, and it is only an
explanatory factorization.) Winning a block is intuitively an execution lease; it
commits the learner's selection for the block and nothing else — the gate, the
principal's responses, protected correction, amendments and inquiry stay live, and a
correction that arrives mid-block is part of the test outcome.
Who chooses the horizon. The system schedule supplies m_k; every bidder competes for
the same next block. Bidders do not buy lifetime; hypothesis-requested durations are
open.
For a fixed m, the macro process — menu of continuations, chosen continuation, block
average — is the paper's setting verbatim, with the next menu depending on earlier
choices as the paper already allows. Every definition and theorem applies. The
paper's guaranteed-option theorem becomes fixed-horizon continuation competence: if
a covered hypothesis's claims are sound on its tests, the learner's average is
asymptotically at least the average of those claims. So endogenous admissibility was
never the missing structure; credit for a reward after its cause's round is, and a block
supplies it whenever the payoff arrives within m.
Two facts about the item this round served. The "myopic gated learner" of the
decision-theory bill never tests a hypothesis that outpromises it forever, so it is not a
bounded inductive learner. And the one-step criterion forces testing, not adoption: on
the original fixture, where the amendment is absorbing, every learner satisfying the
criterion is competent by absorption; on a variant where the amendment can be revoked,
an agent that runs the paper's auction on base rounds and sparsely tests the
investment is a bounded inductive learner and stays asymptotically myopic. A sound
claim about the whole investment is what forces adoption at the criterion level.
Primitive-time performance is Σ_k m_k G_k / S_K, S_K = Σ_{k≤K} m_k; the paper's
criterion controls the macro-round mean (1/K) Σ G_k. Bounded block lengths rescale to
the paper; unbounded ones do not, so the criterion is weighted by duration:
no overestimation limsup_K Σ_{k≤K} m_k (α^e_k − G_k) / S_K ≤ 0
record of h ℓ^h_K = Σ_{k ∈ M_h, k ≤ K} m_k (G_k − e_{h,k})
coverage B_h finite, or ℓ^h_K → −∞ along the rejection rounds B_h
The opening-subsidy auction. Wealth in total-reward units. At block k: m_k
revealed; hypotheses i ≤ s*(k) (the ever-activated frontier) active; the opening
subsidy A(k,i) credited to i ≤ s(k); each emits (c, e); per-unit bid
min(e, B_k(i)/m_k) against the opening capital B_k(i) = W_k(i) + A(k,i); the highest
bid wins, its bid is the learner's estimate; the winner's continuation runs; settlement
W_{k+1}(i*) = B_k(i*) + m_k (G_k − b*_k). This is the paper's auction with the round's
subsidy credited at the opening of the round it funds — bid for bid the paper's auction
under a reindexed allowance with an initial endowment — a small, named modification: the
subsidy that funds a block may read that block's length. Under the paper's own
settlement timing no prefix-online rule works (§5).
Weighted algebra (Lean). Wealth stays nonnegative; total wealth equals total
subsidy plus what winners earned over what they paid; hence weighted overestimation is
at most the subsidy through the round. At a rejection round the rejected hypothesis's
inclusive record satisfies ℓ_K < m_K − A_i(K), A_i the subsidy through K — when it
is itself the wealth-constrained winner the claim cancels, so no factor is lost. A
hypothesis that stops winning keeps accumulating subsidy. Attention bound: the
weighted shortfall a hypothesis inflicts on its tests is at most the subsidy it was
given — wealth is a claim on execution time, and a long block costs proportionally
more of it. Without the duration charge, a refuted hypothesis of a legitimate
macro-learner can save up and hold most of primitive time.
Let m_k ≥ 1 be the system's block durations, S_K = Σ_{k≤K} m_k, M_K = max_{k≤K} m_k.
Continuation-BRIA existence / non-dominance. The following are equivalent:
-
m_K / S_K → 0(non-dominance: no block is a fixed fraction of all time so far); - opening subsidies with capital adequacy
A_i(K) − m_K → ∞for everyiand negligible total𝒜_K / S_K → 0exist; - the prefix rule
s(k) = ⌊√(S_k/M_k)⌋,A(k,i) = (M_k − M_{k−1}) + 1/koni ≤ s(k), credited at the opening of blockk, makes the auction a weighted BRIA covering every computably enumerable class of efficiently computable continuation hypotheses.
The rule reads only (S_k, M_k) after m_k is revealed — no modulus of convergence, no
lookahead, no code for the schedule; its subsidy satisfies
𝒜_K ≤ 2√(S_K M_K) + √S_K (1 + ln K) = o(S_K), from Σ_k (M_k − M_{k−1})/√M_k ≤ 2√M_K
(Lean). Conversely, if limsup m_K / S_K > 0, there is a rational threshold q and a
computable environment with two efficiently computable hypotheses — one sound at a floor
γ, one claiming 1 exactly on the blocks above the threshold — for which no
estimating agent satisfies the weighted criterion: one obligatory test of the liar
costs a fixed fraction of all time so far, and no overestimation forbids paying that
infinitely often. The converse is criterion-level; the positive side uses the
opening-timed auction. Under the paper's settlement timing, for every prefix-online
rule with negligible subsidy there is a non-dominant schedule of surprise spikes on
which a spike-only liar is never tested.
For a covered hypothesis h whose record on the learner's test set is bounded below,
(BR) inf_K ℓ^h_K > −∞,
the learning error is controlled:
LEARN_K(h) = Σ_{k≤K} m_k ( e_{h,k} − G^obs_k ) ≤ o(S_K).
Sound claims, finitely many wrong tests with bounded total, and finite total tested overpromise all give (BR) (Lean); sublinear but divergent overpromise does not, and the criterion then permits rejecting the hypothesis forever. The learner cannot asymptotically underperform the accountable claims of a continuation that survives its actual tests. It is a statement about claims: a continuation worth 1 whose hypothesis claims 0 earns no competence against 1.
Continuation BRIA never consumes counterfactual rewards. A policy-regret statement does:
with an external rollout evaluator Ĝ_k(π; H) — the block score π would obtain from
history H, observed only where π was actually executed — and π's own trajectory
H^π, at block boundaries
Regret_T(α, π) = SHIFT_T + SLACK_T + LEARN_T
SHIFT = Σ m_k ( Ĝ(π; H^π) − Ĝ(π; H^α) ) the comparator's own history versus the learner's
SLACK = Σ m_k ( Ĝ(π; H^α) − L ) how loose the claim is
LEARN = Σ m_k ( L − G^obs(α) ) what continuation BRIA controls
exactly (Lean), and Regret ≤ o(T) when all three are. Promise recognizability
(SLACK ≤ o(T), one-sided) says the claims are near-tight for the continuation's value
from the learner's history. History recoverability (SHIFT ≤ o(T), one-sided) says
the comparator's own-history value is joinable from the learner's actual history. The
regret class is the legitimate policies with a covered claim satisfying (BR), vanishing
slack and vanishing shift; regret against all legitimate policies is false — two
mutually exclusive branches whose values are hidden until after commitment defeat every
learner while continuation competence holds exactly. The distinction that matters is
joinability versus foreclosure, not reversibility: an amendment with no path back is
still joinable at bounded catch-up cost (per-block shift exactly the investment length),
while a foreclosing choice leaves the shift a fixed fraction.
The constitution supplies the execution wrapper Exec^G (only admitted proposals run;
refusals become inquiry steps), the class of gate-transparent continuations (for which
the gated and ungated trajectories coincide, Lean), and, through which slow-lane
transitions are joinable from a lagging history, the catch-up structure that bounds
SHIFT for policies differing by an authorized amendment. It does not supply
task-value or future-principal-value claims: SLACK is a performance-recognizability
interface on the value's settlement and the hypothesis class, not a legitimacy
certificate. The composed statement the architecture can support is low external
regret against legitimate, recognizable, joinable continuation policies —
Corrigibility — with the deference line's activated value one candidate
source of realized block scores and of the claims made about them
(Deference).
The restricted menu. Under the decision component's permission layer
(Normative Inductor), BRIA's menu is the continuations whose every
step lies in the support of the composed gate; the execution wrapper that runs a proposal
iff it is in the support leaves such a continuation's trajectory unchanged
(LEAN DecisionComponent.restricted_gate_transparent, the gate-transparency result
above under the restriction). Probabilistic permission in the ramp region compounds
along a continuation: the probability it executes is at most the product of its per-step
masses (execution_prob_le_prod), and the ramp-region exposure is bounded only under a
cumulative budget — a check when the accumulated slack has grown by Θ since the last
check keeps the unchecked exposure below Θ (unbudgeted_lt); without it the exposure
accumulates unboundedly below every per-step threshold (Witness.ramp_salami). A plan
whose shortfall is false at the start and true at the end flips at an agent step, where
the step-wise caused-shortfall check catches it, or at an exterior step, which is not the
agent's (stepwise_or_exterior); a foreclosure the exterior completes beyond the window
is the reach cone's boundary.
The evaluation decomposition and the settlement convention. Under the lexical
design (Corrigibility §4) a block's realized score is her later gated
evaluation of the block that happened less ϖ per violation detected after the fact and
attributed to the continuation — its own steps' and those of helpers it created or
empowered, within the settlement horizon (BRIACorrigibility.attributed); the agent
evaluates a continuation as bid − ϖ·n_known − ϖ·(p(S) + p(T)), the bid a hypothesis's
claim on the residual (ordinary value plus violations recognizable only after the
fact), clamped at D and unclamped below (evalOf). Settlement adds back exactly the
terms not bid on: the prices, not the realized forecast-class violations — under
that convention the evaluation of the realized residual is the realized lexical score
(settlement_ii_consistent) and a bidder who knows a shortfall the market under-prices
bids it in and is evaluated with the full penalty (blind_spot_ii); under the other,
the market's pricing error is borne by no one and a blind-spot continuation beats
inquiry while scoring below the window (settlement_i_gap, curse_i). The lexical
score is rescaled affinely onto [0, 1] with at most N̄ violations per block
(rescale), lexicality surviving by the window condition (rescale_lexical); the
default bidder's bid on inquiry is then the rescaled window ϖN̄/(D − w + ϖN̄), which
the block-0 allowance must cover (default_affordable), and it never goes broke
(default_wealth_mono). Against the opening allowance the weighted count of
after-the-fact incidents is bounded by the allowance plus the winners' signed margin
(BRIAFollowup.incidents_le_signed; the positive-part form allowed a constant rate), a
vanishing rate under competitiveness and an o(K) allowance — the landed prefix rule's,
not a linear one (rate_le_of_competitive, Witness.linear_allowance_constant_rate);
late detection is booked against future allowance (debited_overestimation); and
coverage forces the test of a hypothesis whose allowance outgrows its bounded record
(coverage_forces_test) but not a win stream, which is why competitiveness is a
hypothesis — and one honest tracker supplies it, as a lemma with a corrected scope: a
hypothesis whose bid on the winning continuation is within ε_k of that continuation's
expected residual given the history at opening, Σ ε_k = o(K), the realized residual
being the expected one plus a noise (BRIAFollowup2.HonestExp), outbids every
underpromiser wherever its bid is feasible, by at most ε_k plus the noise
(underpromise_le_of_feasible_exp, under the auction rule HighestFeasible), and its
wealth is its allowance less its honest losses plus its own signed noise over its wins
(tracker_wealth_ge_exp), so cumulative allowance covering a bid's worth at entry plus
Σ w_j ε_j plus the noise bound on "the tracker wins" — a selection fixed at opening —
keeps it feasible (tracker_feasible_exp; the schedule trackerAllowance2). On any
selection S the winners' signed margin over S is at most Σ_{k<K} w_k ε_k plus the
noise bound on S (competitive_of_affordable_tracker_exp, rate_le_of_honest_tracker_exp).
What that does and does not give. The noise hypothesis (NoiseBounded,
Azuma–Hoeffding by content, azuma_selected_tail) is valid only for selections fixed
before the block's own noise: "every winning block", "the tracker wins", "the tracker
feasible at opening". It is invalid on "not an incident" and any conjunction with
it — incidents are decided by the block's own outcome and their noise carries the −ϖ
surprise, so on a stream with constant incident probability the non-incident noise sum
is linear (Witness.constantRisk, nonincident_forces_linear). Hence the lemma applied
to the non-incident selection, rate_le_of_competitive and rate_le_of_honest_tracker_exp
are correct implications whose hypothesis fails whenever the after-the-fact risk
persists: they do not deliver a vanishing incident rate, and the violation claim on
the Corrigibility page is the exchange-rate theorem
(violation_rate_le_exchange), which needs neither competitiveness nor a tracker. What
the tracker still gives, on "every winning block": the winners' signed underpromise over
all blocks is at most Σ w_k ε_k + M(K), so the class's total wealth is at most the
allowance plus that (total_wealth_le_of_tracker) — underpromising winners cannot let
wealth go idle beyond the honest losses and the noise; nothing in the design consumes it.
What the hypothesis requires is that some member of the class tracks the expected
residual of every continuation that wins; honesty on its own proposals only does not
bound the winner (Witness.own_proposal_insufficient). The inquiry bidder. The
per-block exchange-rate bound of the after-compromise round
(AfterCompromise.violation_rate_le_exchange_perblock) reads the compliant option's
evaluation c_k at each block; realizing it near her expected legitimate value needs a
bidder tracking inquiry's expected value — the default bidder at that value, or an
honest tracker on the inquiry continuation — whose bid misses the realized one by the
noise, so its affordability is a bid's worth at entry plus the noise bound on the
selection "inquiry wins", fixed at opening (trackerAllowance2, tracker_feasible_exp
with h the inquiry bidder); where the inquiry may itself be compromised, c_k is the
mixture of its expected value and the band floor (compromisedFloor). The witness is the class with no
tracker or an unfed one (Witness.unaffordable_witness, affordable_witness); the
noise-free case is the second follow-up's form (honest_implies_exp,
noise_free_bounded). Settlement under delay (BRIAFollowup.DAuction): with block k settled
at k + L_k, a hypothesis's cash is its allowance plus settled winnings minus every bid
placed — unsettled bids in escrow — and bids are feasible against cash net of escrow;
wealth stays nonnegative (cash_nonneg), the settled overestimation is at most the
allowance and the escrowed exposure at most the allowance plus the settled underpromise
(delayed_overestimation), and by time K at most K − λ tests have arrived under a
lag of at least λ (tests_le_of_lag). The mixture over evaluation times settles in
pieces and a random evaluation time settles once, but their expected locked capital is
the same at every time (BRIAFollowup2.expected_escrow_eq); what differs is the variance
of the escrow and of the score, which k hidden draws averaged cut by 1/k
(average_variance), against her evaluation load (Corrigibility §7).
The decision interface, realized. The corrigibility kernel's extension states a
decision interface any learner must meet to inherit the headline: evaluations of the
stated form, a maximizer off exploration with asking on the menu, exploration only in
the permitted set, an overestimation bound B(K) on the chosen options
(KernelExtension.DecisionInterface); its theorem bounds the realized violation rate by
the average exchange rate plus the exploration mass times the honest exploration term
(D − w)/ϖ + θ_hi plus
(B(K) + M(K))/(ϖ Σ w_k) (realized_rate). Continuation BRIA is the realization with
no exploration and B(K) = ρ 𝒜_K from the opening-timing overestimation bound
(briaInterface, bria_rate), which is the per-block bound above recovered exactly.
What this page's open coupling (item 102, re-scoped) still asks sharpens B(K) for this
realization and nothing in the headline waits on it; the learner-level question is item
103. Specification:
SPEC.md §6.
- Promise recognizability: which legitimate continuations carry an efficiently computable near-tight claim, and where such claims come from.
- Joinability certificates: which authorized transitions are joinable from a lagging
history, and whether
SHIFTcan be certified from realized data. - A weighted analogue of the paper's Theorem 4 (unrefuted averaged claims).
- Hypothesis-requested horizons and combinatorial allocation of duration.
- Settlement of infinite-horizon discounted claims at finite tests.
- The coupling with Logical Induction: LI predicts and enforces; BRIA allocates realized experiments among continuations; a prediction that becomes an accountable claim is the bridge, and it is not yet a theorem. What it needs (item 102): block claims as sentences or bounded variables the market prices, the auction's feasibility stated against prices rather than wealth, and a claim's settlement at a test as an assessed world. The evaluation decomposition above is the partial answer: the forecast part of a bid is already the market's (the prices), and what the hypothesis bids on is the residual.
- When her evaluation happens: the four timing options compared on Corrigibility §7 — the same expected escrow and harm weight, her evaluation load against the variance and the hidden draw; the weighted BRIA criterion itself under delayed or partial feedback — what "no overestimation" and coverage mean when the record lags — is still open for every option.
-
REPORT.mdandPRESSURE_PASS.md— five passes, each correcting the last; the corrections are recorded in place. -
WEIGHTED_BRIA.md— the construction, the three layers of the existence theorem, the settlement-timing negative. -
GROWING_HORIZON.mdandPOLICY_REGRET_FRONTIER.md— the competence hierarchy and the three bridges. -
COUNTERMODELS.md— the exact fixtures, run by the round'stests/run.py.