Consecutive bounded column-interface intervals

This implementation extends the atmospheric slab lane in chapters 04, 09 and 21. The existing binary-slab constructor retains its frozen contract. A new opt-in column model admits mixed top fractions and derives subsequent interval geometry from conserved column volume. One constant liquid density equals carrier density. Atmospheric pressure is zero; air inertia, tension, viscous traction, adhesion, variable density and mesh solids remain absent.

Geometry and pressure update

Choose a grid axis d. Each column is attached to its lower wall: n full cells, one optional mixed cell with fraction alpha in [0,1), then air. Its physical height is origin_d + h_d (n+alpha). Initial disconnected or multiply mixed columns reject. Every column must contain the bottom pressure center (n+alpha > 1/2) and retain an air center above (n+alpha <= N_d-1/2); neighboring heights differ by at most one cell. These are declared resolution/topology limits, not clamps. Drying below this range, overtopping it, unsupported gaps or excessive slope preserve the accepted frame and return typed errors.

For pressure classification use normalized phi_i = (layer_i-n_column)+(1/2-alpha_column), evaluated with local integer offsets rather than subtracting large world coordinates. Negative values are wet centers; a center exactly on the interface uses known atmospheric zero. On a wet/air edge, linear interpolation gives theta = -phi_w/(phi_a-phi_w), so the interface distance is theta h_edge. The integrated coefficient is A_edge/(rho h_edge theta), and the velocity correction uses 1/(rho h_edge theta). Wet/wet edges retain the existing full-distance weight; air storage has identity rows and zero RHS. Both PCGs use the same existing six-vector workspace and recompute the diagonal for the held geometry. No minimum theta is substituted. Nonfinite, subnormal or rounded-to-zero required coefficients reject. A native test reaches overflowing inverse-distance scaling with theta about 1e-16 and retains that rejection.

This follows the ghost-pressure derivation in Bridson and Müller-Fischer’s course notes, section 4.5.1. Our height sample interpolation is a bounded approximation, not a general signed-distance or cut-cell reconstruction. Pressure uses full grid face areas, not reconstructed wetted apertures or a physical partial-cell momentum mass. The connected bottom pressure layer and an atmospheric connection above each column give the anchored graph an SPD argument; the new Lean identities do not prove that complete assembled graph or the Rust solver.

Conservative geometric transport and column closure

Inside a mixed cell, the transport reconstruction is the axis-aligned plane s=alpha, with liquid on the lower side of the normalized unit cell. For signed axial Courant magnitude C, the upward outgoing liquid slab has length max(alpha-(1-C),0) and the downward slab has length min(alpha,C). Multiply this length by the cell volume and the direction sign. Transverse swept prisms use the existing shared donor amount dt A u alpha; for this axis-aligned plane that is its geometric intersection volume. Each interior face transfer is computed once and reused with opposite signs. Outer faces retain the explicit existing uniform inlet-fraction policy. Basilisk’s primary VOF implementation illustrates the general swept-region method; this implementation does not port its multidimensional reconstruction or splitting scheme.

All original outward-Courant, checked product/division, nonzero-subnormal, raw fraction-bound, divergence and native ledger gates remain. Geometric per-face C must also pass the original configured outward limit before clipping a swept region. Bounds of an individual axial intersection do not prove an unsplit multidirectional positivity theorem: a bad combined candidate still rejects. Pressure divergence acceptance applies to the held wet centers and remains explicitly reported separately from air divergence.

After raw transport, a canonical column retains its exact n and alpha. A noncanonical but bottom-attached, contiguous raw column can be closed by its compensated sum H=sum_j f_j, reconstructing n=floor(H), alpha=H-n. This explicit height-volume closure redistributes unresolved vertical donor smearing into one bottom-attached region. It is not a reconstruction of arbitrary VOF geometry or a silent fraction clamp. It cannot repair a negative or overfull raw cell because those have already rejected. A true air gap with positive liquid above rejects rather than collapsing a disconnected volume. The report counts collapsed columns and records the reconstruction volume change.

Summing a raw column cancels all internal axial transfers, leaving transverse exchange, top/bottom boundary transfers and sources. The ideal bottom-fill reconstruction has the same column volume. Floating arithmetic is qualified again after closure: amounts and mass use the original scale checks, and balance and budget are recomputed with the unchanged 64 eps (abs(before)+abs(after)+out+in+sum abs(source)) expression. No tolerance or raw-bound relaxation is introduced. Canonical output can differ from raw fractions, but represented mass must still satisfy that original ledger.

Pressure-invalid internal faces are cleared before forces. After correction, one inactive face layer copies only an active face immediately below it along d. A copied air face never becomes a donor for another copied layer; outer walls remain zero, and pressure-active faces are unchanged. This bounded extension supplies transport velocities at a partial top cell whose center is air. It is neither a general normal-direction air-band extension nor an air momentum solve. Force and energy diagnostics retain the existing box quadrature; no physical free-surface work identity is claimed.

Ownership, stamps and cancellation

LiquidTransportSimulation::with_reconstructed_surface(..., axis) owns the existing carrier and liquid state plus ColumnSurfaceWorkspace. Geometry is derived from the volume owner and has no independent mutable phase API. A workspace contains three capped arrays of ColumnHeight: accepted end geometry, candidate geometry, and the geometry of the last accepted pressure interval. Thus retained payload is the previous 16 F + 80 N plus 3 C sizeof(ColumnHeight), nominally 48 C on this 64-bit target. There are 23 field/geometry arrays. Transferred fraction capacity and nominal geometry are preflighted together before geometry allocation; actual Vec capacities are charged. No per-step allocations or rollback snapshots are used.

The read-only view distinguishes reconstructed_surface at the accepted end from pressure_columns held over the accepted interval. Pressure geometry carries the input volume stamp; end geometry carries the output stamp. This explicit time split avoids claiming that pressure was solved on a future transported surface. It also retains a coherent last frame when the next step fails: candidate reconstruction never aliases either accepted geometry array. Prepare carrier, conservative volume, reconstruction, ledger and next-geometry coefficient checks before the single final callback. Then copy the held geometry, swap its candidate, and publish both original owners and accepted pressure without further fallible work. Prescribed carrier box flow and SmokeSource remain unsupported in coupled surface mode. Conservative phase-source proposals retain original gates; they are not a bulk divergence-source model.

For manufactured advection, LiquidVolumeState::advance_reconstructed(ColumnVolumeInputs, workspace, callback) atomically publishes phase and its geometry under caller-supplied velocity. It verifies geometry/grid/stamp/fraction identity first. This lower-level route deliberately makes no pressure or momentum qualification claim. Stale or mismatched derived workspace state rejects. Reconstruction stages are visible for cancellation; failed candidates may dirty scratch, never accepted fractions, pressure history or geometry.

Executed numerical and exact-real scope

The native tests independently assemble variable-distance matrices, recover a rectangular 3D manufactured pressure with unequal spacings, and check column hydrostatics on all axes. Mixed hydrostatic states repeat sixteen times with both PCGs. Eight consecutive two-column pulses preserve total volume, including a case starting at alpha=1/2 that activates a new pressure center for subsequent intervals. Native late source/geometry failures and cancellation verify all published field/clock/stamp/geometry bits and retry equivalence. A disconnected source-created proposal and an excessive-slope proposal reject after carrier/pressure preparation. The existing binary-slab raw rounding rejection remains frozen and is replayed; it was not repaired by clamping.

The laboratory separates coupled dynamics from imposed advection. Coupled scenes show continued publication, reconstruction and pressure classification, not a fluid-accuracy convergence oracle. Axial imposed translation grows and drains a flat surface across complete layers for sixteen intervals, matching analytic height and volume exactly in the dyadic fixture. Transverse imposed X translation stores the height profile on n x 4 x 2 cells and matches the independent binomial donor oracle. At fixed T=1/2 and C=1/4, L1 height error decreases from approximately 0.0043409 (n=16) to 0.0022360, 0.0011341 and 0.0005711 (n=128), approaching first order. Halving C at n=64 raises donor diffusion to about 0.0013195. This is combined spatial/time refinement of a prescribed flow, not multidirectional liquid convergence. Open-boundary ledgers include the small numerical outflow tail.

Ten standalone Lean 4.19.0 exact-real identities prove supplied ghost interpolation/gradient, height-edge zero crossing, positive variable-distance coefficient under positive area/density/spacing/theta, supplied reconstruction volume, three-cell internal axial cancellation, shared-column cancellation, individual upward/downward swept-volume bounds, and a one-dimensional transverse convex donor bound. They require supplied geometry/fluxes and explicit nonzero/positive hypotheses. The audit checks all ten and rejects actual sorry and additional-axiom variants. They do not establish IEEE preservation, general geometry validity, global multidimensional positivity, PCG convergence, the complete assembled SPD graph or physical calibration. Historical proof inventories and published PDF inputs remain unchanged; this file is a new implementation companion.

The frozen successor at 70b5ce3 addresses the earlier NaN/ledger weaknesses in tools/verify_free_surface.py and tools/test_free_surface_verifier.py, confirmed before new edits and again in an exact isolated checkout normally and with -O. The new column gate likewise checks all finite fields before reductions, independently recomputes the raw and reconstructed ledgers, verifies held/end geometry versions and native pixels, and uses manufactured advection oracles. The original assert-based composition verifier is not claimed to be optimization-safe.

Remaining gaps include breaking/overturning interfaces, detached drops and films, general oblique PLIC and cut-cell momentum, a general velocity extension, variable density, capillarity, viscosity/adhesion, mesh solids, pressure accuracy at moving curved surfaces and validated multidirectional liquid dynamics. The height closure and full-area ghost pressure are explicit approximations. No fully validated liquid simulator or real-time performance claim follows from these fixtures.