Resolved single-liquid slab pressure interval

This opt-in implementation follows the eliminated atmospheric-pressure boundary in book chapters 04, 09 and 21 and the single-liquid lane in expansion/PLAN.md. The admitted geometry is deliberately smaller: liquid fills the lower complete layers along one coordinate axis, air occupies the remaining layers, and the outer box is sealed. Density is one positive constant, equal bit-for-bit in the carrier and represented-liquid owners. Atmospheric pressure is zero. Negligible air dynamics, zero surface tension and no viscous normal traction are model assumptions, not measured material properties.

Discrete equations and public ownership

For a wet/wet face with area A and center separation h, use w=A/(rho h). At the wet/air face the atmospheric point is the face itself, distance h/2 from the wet center, so a=2w. A wet row is sum_wet w(p_i-p_j) + sum_air 2w p_i; RHS is -sum_faces A u_star / dt. There is no wet gauge pin or closed-box RHS mean correction: the resolved slab touches an atmospheric anchor. Air pressure storage uses uncoupled identity rows with zero RHS and yields p_air=0; these dummy rows are not air momentum equations. Jacobi-PCG and SGS-PCG use the same existing six-vector pressure workspace. Velocity correction uses the identical wet/wet or half-distance wet/air coefficients. Outer faces and air/air faces are zero.

SlabFreeSurface::new(grid, axis, wet_layers, stamp) requires at least one wet and one dry layer. LiquidTransportSimulation::with_free_surface validates the exact binary fractions and equal densities before constructing the existing owners. PressureOperator::with_free_surface also exposes the anchored operator for manufactured tests. The ordinary constructors retain full-box pressure and their original arithmetic order. The facade state publishes the pressure geometry used during the interval; it is not reconstructed from end fractions. Reports attach its caller-supplied stamp and explicitly identify the volume divergence domain as LiquidSlab rather than AllCells.

Preparation reuses the carrier candidate buffers and liquid donor workspace. After existing MAC advection, inactive air/air and outer faces are cleared, body forces act only on wet-adjacent internal faces, and pressure corrects those active faces. Divergence acceptance applies to the old wet cells. Air divergence may be nonzero and is explicitly demonstrated in the pulse fixture. This is zero storage in inactive air, not a tested air-band velocity extension algorithm. Existing force work/energy diagnostics retain their box face quadrature; no physical free-surface kinetic-energy or traction-energy identity is claimed.

The conservative donor transfer still visits every cell and shared face, with the original checked scale arithmetic, raw fraction bounds, outward Courant gate and ledger. The interface flux uses one shared donor amount on its two sides. Pressure, velocity, tracer, fractions, clocks and stamps publish at the same final checkpoint. No new field arrays, snapshots or per-step allocations are introduced: the original 20-array facade inventory remains 16 F + 80 N bytes, excluding Vec metadata and allocator overhead. The geometry is a bounded descriptor. Example-only bit snapshots used to demonstrate rollback are outside the solver.

The held binary slab must match the accepted fractions at the next call. A nontrivial surface interval can create mixed cells; the next call then rejects before callbacks and preserves the accepted pair. There is no geometry reset/import/reconstruction API. Hydrostatic cases whose fractions stay exactly binary can repeat. Prescribed box flow and appearance SmokeSource are rejected in this mode; conservative liquid source proposals retain their existing bounds, checks and atomic failure behavior.

Executed qualification and exact proofs

Independent Rust fixtures assemble the small anchored matrix without using the operator, manufacture rectangular 3D pressure with unequal cell spacings, and check hydrostatic center pressures along all three axes. Both original PCG methods recover the solution. The coupled two-column, one-Z-cell pulse accepts p=(-1/8,+1/8,0,0), interface speeds (+1/8,-1/8), and fractions (1,15/16,1/16,0) at dt=1/2; represented volume stays exactly 2. Air divergence is (-1/8,+1/8), while old wet divergence is zero. The next interval rejects unresolved mixed geometry. Cancellation stages and a late volume rejection start with already accepted nonzero pressure and verify bitwise preservation and retry equivalence.

The release example also executes 16 exact one-cell hydrostatic intervals. A refinement probe is retained rather than hidden: SGS at 16 wet layers rejects a raw fraction of 1.0000000000000004 and keeps time zero and all accepted field bits. Jacobi at 2/4/8/16 layers and SGS at 2/4/8 accept the first interval in this run. No clamp or relaxed bound was added. These probes do not establish convergence of a moving liquid surface.

New standalone Lean 4.19.0 identities in evidence/free-surface/FreeSurface.lean use the original pinned mathlib revision. They prove two-cell eliminated quadratic form, nonnegativity under nonnegative coefficients, removal of the constant mode with positive shared and anchor weights, half-distance scaling with nonzero denominators, supplied row/residual correction with nonzero dt, hydrostatic cancellation, and shared-transfer cancellation. The audit checks all nine definitions/theorems and rejects actual sorry and additional-axiom variants. These exact-real identities assume supplied geometry and coefficients; they do not prove a general graph theorem, Rust refinement, IEEE bounds, geometry assembly, PCG convergence or physical validation. Existing proof inventory, historical chapters and PDF are unchanged.

Native PNGs are +Z fraction-integral guidance with coefficient 8/m and +Y upward. They show accepted volume data, not a reconstructed surface or physical scattering. The evidence figure labels the two-column manufactured scope. Numerical gates independently recompute finite values, fractions, pressure, face divergence, native pixel equations, carry-forward and rounding budgets, including adversarial fixtures with Python optimization enabled.

Remaining features include evolved interface reconstruction, arbitrary wet topology/cut geometry, air-band velocity extension, variable density/two-fluid pressure, surface tension, viscosity/adhesion, mesh solids, and validated multidirectional liquid dynamics. This feature is a bounded pressure-and-transport interval, not a fully validated liquid simulator.