competitiveness from one honest tracker: the named hypothesis is the tracker's allowance

Maintainer decision, landed by the second follow-up. Competitiveness — the winners' signed margin over non-incident blocks o(K) — is derived rather than assumed: if the class contains a hypothesis whose bid on the winning continuation is within ε_k of the realized residual, Σ ε_k = o(K) (BRIAFollowup2.Honest), then wherever its bid is feasible an underpromising winner is outbid (underpromise_le_of_feasible, under the auction rule that the winner's bid is the highest feasible bid on the winning continuation, HighestFeasible), and its wealth is its allowance less its honest losses (tracker_wealth_ge), so with cumulative allowance covering a bid's worth w̄ · D at entry plus Σ w_j ε_j it is feasible at every block (tracker_feasible) and the margin is Σ_{k<K} w_k ε_k (competitive_of_affordable_tracker, rate_le_of_honest_tracker). The expected obstruction — the tracker's capital — does not arise under opening timing, where the bid is a feasibility gate and not a payment: the tracker needs feeding at the rate of its honesty error, not growth; the minimal allowance is trackerAllowance, total w̄ · D + Σ w_j ε_j, o(K) iff the honest losses are. What remains a named hypothesis is that the arrangement's uniform per-hypothesis stream supplies it, since the schedule cannot target the honest hypothesis. Witnesses: the class with an unfed tracker has a linear margin, the same class with the tracker fed has margin zero (Witness.unaffordable_witness, affordable_witness). The corrigibility page's named hypotheses replace competitiveness by an honest tracker in the class. Amended by the third follow-up (2026-09-26): honesty is against the expected residual of the winning continuation, |e_k − m_k| ≤ ε_k with G_k = m_k + ξ_k (BRIAFollowup2.HonestExp) — against the realized residual no bidder is honest under noise, Σ ε_k being linear — and beside it the noise hypothesis by content: the weighted signed noise over any selection of blocks computable at opening ("the tracker wins", "not an incident") is bounded by M(K) = o(K) (NoiseBounded), Azuma–Hoeffding's content, whose per-K tail is derived from the pinned Mathlib (subgaussian_tail, subgaussian_two_sided, azuma_selected_tail) with the selection's martingale-difference property and the uniform-in-K sure bound named. The chain re-proved: Mf K = Σ w_k ε_k + M(K) (competitive_of_affordable_tracker_exp, rate_le_of_honest_tracker_exp), the tracker's allowance gaining the noise term, w̄ · D + Σ w_j ε_j + M(k) (trackerAllowance2); the old form is the noise-free case (honest_implies_exp, noise_free_bounded). What "one honest tracker" requires: some member tracks the expected residual of every continuation that wins — honesty on its own proposals only does not bound the winner (Witness.own_proposal_insufficient). Amended by the fourth follow-up (2026-09-26): a true lemma, not the rate result. The chain's margin is taken over the non-incident blocks, a selection decided with each block's own outcome, and the noise hypothesis on that selection fails whenever the after-the-fact risk persists (BRIAFollowup2.Witness.nonincident_forces_linear), so competitive_of_affordable_tracker_exp, rate_le_of_competitive and rate_le_of_honest_tracker_exp are correct implications whose hypothesis fails when p > 0 and deliver no vanishing incident rate. What the tracker still gives, on the selection "every winning block" fixed at opening: 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) — nothing in the violation claim consumes it. The violation claim is the exchange-rate entry below. Rejected alternative: competitiveness as a primitive hypothesis (the first follow-up); honesty against the realized residual (the second follow-up's form).