Mathematical audit of the teaching website¶

The 5 October reconciliation updates the site for the subsequently revised manuscript. This audit records the 2 October construction and verification; its pure-step examples remain valid special cases of the newer randomised family-set formulation.

Checked 2026-10-02 against Edwin Hamel-De le Court et al., §3, the AAMAS 2026 tutorial (printed slides 103–113), and the current local omsh-paper/main.tex. This is a focused audit of the tutorial, not formal verification of its JavaScript or a new audit of all production shielding paths.

Result¶

The central construction matches Edwin's Definitions 2–3. The minimum eventual unsafe-reachability value is the least Bellman fixed point. The computed certificate must be both an upper bound and inductive: B(beta-bar) <= beta-bar. Augmented states have q >= beta-bar(s); successor allocations obey W >= beta-bar and E[W] <= q; the realised successor carries its own allowance. Unsafe successors get allowance one. A realised budget may increase while its pre-transition expectation fits the parent.

The ten-state example's nominal optimal Entry risk is approximately 0.1467046039, independently checked by enumerating all 256 deterministic stationary policies and solving each linear reachability system. Exit lane gives beta*(s7)=0.02/(1-0.04)=1/48. Its transient region is contracting under all its policies, with Delivered and Collision absorbing. The interval solve is appropriate for these rows; this small engine is not a certified solver for arbitrary stochastic games. Its action-dependent reward scores are teaching data and do not enter the safety equations.

Notation is explicit: SoundVIResult.q / q_of(s) are computed state certificates, whereas runtime q is an allowance. Edwin's allocation alpha is runtime W; OmSh's opponent posterior alpha is a different object. The slides' beta_t is runtime q_t, and their VI tolerance delta is not coverage-failure probability.

Repairs and qualifications¶

• Numerical boundaries: the old budget + 1e-10 test admitted beta=[0.1], P=[1], q=0.1-5e-11. This violates the exact inequality. The teaching helpers now reject any base expectation above budget and check final costs without an acceptance tolerance. Any roundoff overshoot retracts toward the feasible backup. Radial projection includes every positive denominator; mixture coordinates are checked after clipping and fall back if still over budget. Safety menu and credible-tail comparisons are also strict. Tolerances remain for optional filling termination and reward ties. This does not prove machine-level directed rounding; the site uses floating-point arithmetic for teaching.
• Safety versus optimality: Edwin's encoded actions use vertices of the feasible distribution polytope. Its convex hull satisfies the displayed inequality. Pure-action trajectories and the restricted allocator search retain safety but remove some safe reward-optimal choices. The site now distinguishes exact-value optimality, the approximation limit under Slater's condition, and PPO, which has no promised global optimum. A misleading “pure-action continuation lower bound” phrase now means a conservative lower limit on successor allowances, not a lower bound on optimal mixed-policy risk.
• Inductiveness: the pipeline now displays the certificate inequality rather than an approximate fixed-point equality. A merely pointwise upper estimate does not establish the required nonempty continuation set. Current MDP checks verify the inductive inequalities and backup feasibility.
• Slides' indexing: printed slides 103 and 109 (physical PDF pages 220 and 226) put beta_{t+1} on the right of the expected-allocation constraint. Visual inspection confirms the PDF text. Under the stated action timing this appears to be an indexing typo: compare with the current q_t, then set q_{t+1}=W_t(s_{t+1}), following Edwin's Definition 3 and the OmSh manuscript. The site's timing was already correct. The HTML paper also displays alpha(s) in its transition Dirac expression; its following support description identifies the intended successor alpha(s').
• Algorithm naming: Edwin permits any algorithm returning the required inductive certificate. The website illustrates the repo's interval implementation; it does not claim to implement the published Quatmann–Katoen SVI algorithm described in the manuscript's SVI appendix.
• Original-game scope: retained-row robustness covers those kernels and their convex hull, including covered level switching. Posterior weights can rank reward and propose floors; they are not time-uniform coverage certificates. Accepted certificate families must be antitone in the floor, and the real row must remain covered after an irreversible floor increase. Credible-tail guarantees retain the stated calibration and true-level assumptions. Softened posteriors alone cannot establish them.

Added pages¶

opponent-theory follows the manuscript's recursive imagined policies and Bayesian mixing: cloning at level zero, alternating focal/opponent improvement, finite-horizon rollout scores, a Boltzmann target, and observed-action likelihood updates. An interactive warehouse example applies exact Bayes or a selected temperature and EMA weight. Belief updates do not themselves change its floor or certificate.

guarantee-theory follows as:anytime_coverage, def:anytime_runtime_certificate, thm:anytime_safety, and cor:padded_omsh. It explains predictable outer sets, a feasible certificate at each safe history, and the stopped-budget supermartingale proof of Pr(ever unsafe) <= min(1,p+delta_cov). It does not assume that conditioning on future coverage preserves transition laws. The persistent-hazard example follows the manuscript: 1-(1-epsilon)^H -> 1.

This page separates VI approximation error, TV padding radii, and coverage/tail failure probabilities. Its calculator reserves separately justified error probabilities from a total target and compares the warehouse floor-zero demand. It does not certify coverage or feasibility after enlarging the ambiguity set. If coverage already includes floor exclusions, a separate tail reserve would double-count the same event. Guarantees begin after certification and concern one focal agent's budget-carrying run; resetting the initial budget starts a new query.

Validation¶

node teaching-site/check.cjs passes 30,309 assertions, including 4,229 new strict-boundary, projection and posterior likelihood-ratio checks. Earlier allocation and backup checks are now strict. Independent Bayes checks use the analytic level-1 odds multiplier four for each yield; temperature two and EMA weight one-half give (5/12,7/12).

Chromium and Firefox passed isolated single-file loading and HTTP at seven viewport sizes, all nine chapters, all worked-model tabs/modes, Bayes updates, error-budget infeasibility, keyboard navigation and readable no-JavaScript text. Desktop and phone theory layouts were visually inspected. Sources remain embedded in index.html; the OmSh snapshot is synchronized manually. Production controllers, solvers and manuscript files were not changed.