Teaching-site reconciliation with the updated manuscript¶

Checked 2026-10-05 against ../omsh-paper/main.tex at e049b7c. The site at ~/Documents/omsh-website now has thirteen chapters. Its four appended pages explain the changed formal results while retaining the ten-state warehouse and the original intuition lessons. The earlier audit is a dated record; this note describes the subsequent theory reconciliation. No manuscript, production solver, controller or training path was modified.

Changed mathematical objects¶

The main difference is a distribution nu over action/allocation pairs, rather than only a pure focal action and a single successor allocation. For simultaneous moves the opponent chooses its level before the focal draw, giving max_level E_nu[P_level,a · W], rather than E_nu[max_level P_level,a · W]. The original-game theorem correspondingly uses predictable sets of complete action-row families F=(F_a)_a, which preserve constraints linking actions. Checking separate per-action worst cases can be more conservative.

randomised-theory follows def:fixed_floor_shield and the generalised def:anytime_runtime_certificate. A terminal crossing with opposing 0/0.4 rows illustrates why a balanced mixture costs 0.2 with simultaneous levels and 0.4 with a reactive level. This is a separate toy; the default warehouse remains the multi-step example. Sampled pairs need not individually fit the parent budget. Each sampled W must dominate an inductive certificate with unsafe coordinates one. The few-atoms result (prop:two_atoms) is explained as a decomposition into feasible components with at most |Lambda|+1 pairs; it does not compress an arbitrary distribution into a single such component.

permissiveness-theory distinguishes the pure robust least fixed point from beta_mix, the mixed robust least fixed point. The original warehouse engine still computes the pure operator; no mixed solver is substituted into it. An arbitrary mixed-inductive certificate need only lie above beta_mix; the additional inequality beta_pure <= beta applies to pure upper certificates, not to every certificate in the general theorem. For a fixed level set, thm:fixed_floor_permissive gives soundness and an existential path-law approximation guarantee. With d=||beta-beta_mix||_infinity, strict initial slack gives epsilon=d/(d+p-beta(s0)); exact d=0 permits zero slack. Below-certificate initial budgets and the approximate zero-slack boundary are rejected by the calculator. The guarantee is against history-adaptive, pre-draw level sequences, and does not assert that PPO finds the controller. An upper bound on d from mixed lower iteration gives a conservative epsilon bound. The manuscript's floor-zero Pursuit–Evasion numbers give about 0.63, which is not an empirical reward loss.

coverage-theory follows prop:tv_confidence_sequence, cor:row_union_bound, lem:tv_ball_bellman and cor:frozen_sets. Counts centre a time-uniform TV ball; the neural kernel remains a nominal model. The user chooses delta_cov, then row and visit schedules allocate it. Adaptive visits are permitted by stationary, state-sufficient dynamics with fresh transition draws and complete legal support. Singleton support needs no statistical radius; a multi-successor unvisited row uses radius one. The interactive count tables hold proportions fixed to isolate sample size, and do not pretend to simulate new observations. The exact one-row TV supremum greedily transports legal probability from low to high W, unlike the cheap range-based upper bound, which can be loose. Manual-radius mode explicitly makes no confidence-sequence coverage claim.

Neural re-centring requires inflating the radius by the empirical/neural TV distance. Joint-row coverage must be combined with a valid opponent-action envelope. The frozen-prefix result covers every later compliant episode conditionally on a good prefix; it is not a lifetime-across-resets guarantee. The one-run original-game accounting still reserves delta_cov from the initial threshold.

dominance-theory follows cor:risk_dominance and its finite-horizon stopped excess bound. For the pure wrapper, true-row containment is stronger than the true expectation of its committed W fitting q. The toy explicitly defines Entry, Inspection, Delivered and Collision. Entry starts at 0.3; Inspection carries 0.4; Delivered and Collision carry 0 and 1. Both active states use the same row. A TV ball of radius 0.02 around (0.5,0.4,0.1) has worst expected W 0.28, so the committed allocation fits both active budgets. Changing the true row can violate containment without introducing excess. The calculator computes stopped occupancy-weighted excess, not a horizon times an observed excess. With wait probability w and collision probability c, actual reach is c sum_{t<T} w^t; expected excess is eta_Entry + eta_Inspection sum_{1<=t<T} w^t for T>=1.

The risk-dominance corollary conditions after the realised action/allocation draw. An unrestricted safe randomised shield may have positive excess on some sampled pairs; pairwise zero excess is not a necessary condition for its distribution-level soundness. The site states this explicitly instead of treating pure-step dominance as equivalent to randomised coverage.

Reported audit and patience numbers are separately attributed to manuscript tables at the checked revision. They are empirical diagnostics of frozen evaluation, rather than validated coverage or certified excess expectations. The floor can violate coverage yet leave the true certificate expectation conservative; neither the heuristic nor sample-level zero excess proves it almost surely. The patience screen retains 64 as primary, despite 4096 delaying raises; the website does not change the runtime default.

Packaging and verification¶

reconciliation-section.html owns the four new chapters. reconciliation.js exports pure calculators for Node and attaches browser controls when a DOM is present. The builder embeds it as the fifth script, along with all styles and markup, in the self-contained index.html. It retains isolated desktop document-portal loading without sibling files. The older safety-assumptions chapter now labels its equations as the pure-step special case and links to the general family-set formulation. Navigation retains the old hashes and extends its chapter counter to thirteen.

reconciliation-check.cjs adds 1,704 assertions: independent joint-outcome enumeration, theorem backup-mixture algebra, substitution into the confidence tail bound, independent halfspace-vertex LP solutions of three-coordinate TV balls, and backwards finite-horizon reachability for the stopped-excess example. The combined suite passes 32,013 assertions. Ordinary floating-point arithmetic remains an educational limitation; this is not formal numerical verification or an original-game deployment certificate.

Run node build.mjs --check, node check.cjs, and the optional browser-check.cjs in the standalone directory. Browser checks exercise all thirteen chapters, the new controls and infeasible boundaries, isolated-file and HTTP loading, seven viewports, keyboard navigation and all-chapter no-JavaScript reading. For the OmSh snapshot, select tests with uv run python scripts/run_tests.py changed and build docs with uv run zensical build --strict. Documentation-only changes require no production trainer or graph test suite. Chromium and Firefox passed these browser checks, and desktop and phone screenshots were inspected. The changed selector used explicit documentation paths because an unrelated untracked scheduled-task lock would otherwise select the broad fast suite; the documentation selection needs no pytest, and the strict documentation build passed.

The standalone repo and teaching-site/ snapshot are synchronized explicitly. Do not copy its README.md into the snapshot: it collides with the generated HTML's docs route. Keep README.txt and update its explicit asset list.