docs: S0 draft — applied/pending motion state, donor sets, mass ledger, pre-kernel gate conditions

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

docs/moving_bodies.md

@@ -97,6 +97,31 @@ fluid pull from a solid slot of a moving body is BFL-written.
   synchronization failure leaves host and device motion state unknown: the
   simulation is marked unusable (existing `_require_usable` lifecycle), and
   no API may report a host/device match afterwards.
+
+### 4a. Applied geometry vs pending target (CANDIDATE, narrow API)
+
+Two distinct facts per moving body, one authority each:
+`applied` = offset (and velocity) of the geometry last applied on the device,
+changed only by a successful commit; `pending` = an optional requested target
+`(offset, velocity)`, changed only by `set_body`. A setter returning proves
+nothing about the device. The uploaded motion record is derived each run:
+`{c_old = base + applied.offset, c_new = base + (pending or applied).offset,
+u = (pending or applied).velocity}`. One moving step consumes one target.
+
+| situation | contract |
+|---|---|
+| `set_body` target | validated against `applied` (box, `|Δc|_2 ≤ 0.5` cell, speed bound) before mutation; on success replaces `pending` |
+| two setters before a run | last wins; each validated against `applied`, not against the earlier pending target |
+| `run(1)` with pending | upload record, step, sync; on success `applied := pending`, `pending := None` |
+| `run(1)` without pending | record with `c_old == c_new`: no cover/uncover, links at `applied`, wall velocity `applied.velocity` |
+| `run(n > 1)` with pending, or with nonzero `applied.velocity` | `ValueError` before mutation (single-step-only moving API) |
+| `run(n > 1)`, no pending, zero velocity | allowed: static geometry, spin only |
+| `run(0)` | no motion upload, no commit; `pending` kept |
+| validation failure | `ValueError`, nothing mutated, retry allowed |
+| upload/launch/sync failure after enqueue | simulation unusable; `applied` and `pending` are not reported as device truth; no re-entry |
+
+Displacement norm: Euclidean per-step `|c_new - c_old|_2 ≤ 0.5` lattice
+cells (declared bound; CANDIDATE value).
 - Membership is never read from a flag that M1 is overwriting. The host
   verifies at `add_body` that every swept-band cell has base flag FLUID, so the
   band's base state is known without reading `flag_gpu`.
@@ -113,9 +138,20 @@ fluid pull from a solid slot of a moving body is BFL-written.
   valid neighbours and `x_d` = the valid neighbour best aligned with the outward
   normal `(x - c^n)/|x - c^n|`; `G_neq(x_d) = G(x_d) - f_eq(rho(x_d), u(x_d))`.
 - Valid donor: inside the domain, base FLUID, `!in_old && !in_new`.
-- No valid donor for the NEQ part → equilibrium only (counted). No valid
-  neighbour at all → cannot happen when the per-step move is < 1 cell
-  (validated on host); counted anyway.
+- Sets: `V(x)` = the 8 lattice neighbours that are in the domain, base FLUID
+  and `!in_old && !in_new`. `rho_bar` = mean density over `V(x)`. NEQ donor =
+  the member of `V(x)` with the largest `c·n` among those with `c·n > 0`
+  (`n` = outward normal at `c^n`); none → NEQ part 0 (counted as `eq_only`).
+- `V(x)` empty → no defined density: the cell is refilled with
+  `f_eq(RHO, u_w(x))` so all 9 slots stay defined, the `no_donor` counter is
+  incremented, and the host treats `no_donor > 0` after the run as a hard
+  failure (simulation unusable). It is not a silent fallback.
+- Non-emptiness is NOT assumed from the displacement bound. Geometry
+  assumptions: circle radius `R ≥ R_min` (CANDIDATE 4 cells), `|Δc|_2 ≤ 0.5`.
+  S1 includes a host enumeration over sub-cell centre positions and
+  displacement directions on a fine grid within these bounds that checks every
+  fresh cell has nonempty `V(x)`; it is evidence for those bounds, not a
+  proof, and runtime keeps the counter.
 - Fresh cells only write, old-fluid cells only read: no race.
 
 ## 6. Discrete momentum ledger (to review; not a selection)
@@ -163,10 +199,28 @@ false (Astra), so their existence does not establish which combination its
 validation cases use. A bookkeeping identity alone does not select the
 physical force either.
 
+Mass ledger (same proposition status). With `M^n` the active-fluid mass
+summed over `F^n` at the sample point,
+
+    M^n - M^{n-1} = sum_L dm - m_cover + m_uncover + B_m^n
+
+(`dm = f_r - f_t`, `m_cover`/`m_uncover` = summed `sum_q G` of covered and
+refilled cells, `B_m` external-boundary mass flux; collision conserves mass).
+
+Sample point (fixed): post-collision storage after the swap of step n, i.e.
+the same level `G` that M1 reads at step n+1; both ledgers are evaluated
+there. Ledger residual = left side minus every listed term. In a closed
+domain (no inlet/outlet, no forcing) `B = S = 0` and the residual must be
+rounding-level; with open boundaries `B`, `S` are not separately measured, so
+the residual is reported as their estimate and is not a pass criterion.
+Both ledger identities are **proposed, unreviewed**: they are not called
+proven until review and a host replay agree.
+
 Accumulators (separate, per body, per step window; all reported raw):
 `link_cme`, `link_wen_correction` (= `sum u_w dm`), `node_cover`,
-`node_uncover`, plus counters of crossings and refill fallbacks, so force
-spikes can be correlated with crossing events.
+`node_uncover` (momentum), `link_dm`, `mass_cover`, `mass_uncover` (mass),
+plus counters of crossings, `eq_only` and `no_donor`, so force spikes can be
+correlated with crossing events.
 
 **OPEN — structural RHS candidates (not selected):**
 (a) `link_cme + node_cover - node_uncover`; (b) `link_cme + link_wen_correction`
@@ -207,8 +261,11 @@ refinement.
 
 ## 9. Gates (map; tolerances OPEN, declared before runs)
 
-G0 zero-motion regression (stationary path unchanged; moving path at rest
-reproduces stationary link set and DDF) · G1 raw force sign (`Cd > 0`) ·
+G0 zero-motion regression, split: G0a populations of the existing stationary
+and spin-only path bitwise unchanged vs main; G0b moving path at rest (with
+and without spin) reproduces the stationary link set and populations; force
+estimator outputs are compared separately from populations, since the moving
+path adds estimator terms · G1 raw force sign (`Cd > 0`) ·
 G2/G3 prescribed translation incl. ledger accumulators · G4 matched
 relative-flow (moving body in quiescent fluid vs fixed body in uniform
 stream), optional boost, co-moving sanity · G5 Dütsch et al. 1998 Re 100,
@@ -228,12 +285,24 @@ amplitude change ≤ 1 %; matched-frame force RMS ≤ 2 % and improving with
 refinement; VIV refinement amplitude ≤ 2 %, frequency ≤ 1 %, five consecutive
 cycle amplitudes within 1 %.
 
+Conditions stated before any moving kernel (S2/S3), not only at the
+oscillator stage: (i) fluid refinement protocol for the prescribed-motion
+gates — diffusive scaling (dx halved, dt quartered, physical Re, KC and
+amplitude fixed), the observed quantities and norms named in advance;
+(ii) Galilean constant-boost G4-boost requires boundaries compatible with a
+uniform boost (periodic in the boost direction or boundaries that move with
+it); if the current dense configuration cannot represent that, G4-boost is
+recorded as not runnable rather than replaced by another test.
+
 ## 10. Proposed minimal S1 scope (host only; held until cross-review)
 
 - `add_body` moving-circle declaration: base centre, declared offset box
   (x/y), speed bound; swept-band computation and band-placement validation.
 - `set_body(offset=..., velocity=..., omega=...)` validation before mutation
-  (section 7) and the fail-closed commit of section 4.
+  (section 7), applied/pending state and the run-transition table of 4a,
+  and the fail-closed commit of section 4.
+- Host enumeration check of refill-donor non-emptiness (section 5) within
+  the declared `R_min` and displacement bound.
 - Motion-record host layout and upload path; exclusion of moving bodies from
   the packed `CurvedBoundaryKernel` links (stationary packing unchanged).
 - Explicit rejections for unsupported modes.