From 421b90f5d21b87e28cf642ba71f1e018f1bb9671 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 30 Oct 2026 06:20:31 +0000 Subject: [PATCH] =?UTF-8?q?docs:=20S0=20draft=20=E2=80=94=20applied/pendin?= =?UTF-8?q?g=20motion=20state,=20donor=20sets,=20mass=20ledger,=20pre-kern?= =?UTF-8?q?el=20gate=20conditions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- docs/moving_bodies.md | 85 +++++++++++++++++++++++++++++++++++++++---- 1 file changed, 77 insertions(+), 8 deletions(-) diff --git a/docs/moving_bodies.md b/docs/moving_bodies.md index a4de59c..9012223 100644 --- a/docs/moving_bodies.md +++ b/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.