8 Boundaries and obstacles
On a wall moving at , impermeability requires . No-slip also matches tangential velocity; free-slip does not. These are distinct models. Prescribed normal wall velocity enters the divergence right-hand side. Atmospheric-pressure openings instead fix pressure and allow flow. Combining both conditions on one face can overconstrain the system.
Binary geometry
A first obstacle model can classify cells and block faces. The resulting staircase approximates a curved boundary but changes effective volume and creates grid-aligned features. Refinement can move the represented wall discontinuously as classifications change. An accurate linear solve cannot remove geometric error.
A boundary snapshot should have one version consumed by advection, pressure and rendering for a step. If geometry changes during pressure solution, discard or restart the stale candidate rather than publish velocity corrected for a different domain.
Fractional faces
An open area fraction and fluid cell-volume fraction produce divergence terms proportional to . Tiny creates small-cell stiffness. Clamping coefficients changes the model; removing cells changes topology. Either can be an explicit approximation, not a free fix.
Batty, Bertails and Bridson develop variational solid-fluid coupling on coarse Cartesian grids [S7]. The structural lesson is to choose gradient, divergence and energy together. Rheon’s arbitrary-matrix theorem does not establish cut-cell quadrature.
For the linear homogeneous operator , with cell metric and face metric , require
An attractive divergence formula paired with an unrelated gradient can yield an inconsistent pressure operator. Test this linear weighted adjoint identity with random vectors on every supported geometry class after prescribed boundary flux is separated. For the metric construction in Chapter 3, , , and . The full physical divergence is affine: . Therefore its identity includes boundary work:
Omitting the final term is valid only when its value is zero, for example homogeneous prescribed flux. The companion includes nonzero Q to reject that omission. The existing Lean arbitrary-B theorem proves the linear algebraic identity, not moving-boundary assembly.
Trajectory collision
A departure point outside solid material does not prove the path avoided it. A long trace can cross a thin wall and emerge on the far side. Intersect straight traces with geometry and apply the declared rule at the earliest hit. Multi-stage curved traces need compatible approximation. Limiting travel helps but is not collision proof.
Boundary interpolation must define its extension. Constant extrapolation, mirrored normal velocity and no-slip ghost values differ. Do not bury them in a texture sampler mode. Check samples on both sides of walls and at corners.
Diagnostic sequence
Test a sealed box with uniform translation, then stationary fluid under gravity with hydrostatic pressure, then moving obstacles with displaced-volume and wall-work accounting. A wall thinner than one cell must be resolved or explicitly unsupported rather than silently leak.
Report flux by boundary category and closed component. Long-term leaks often originate in one inconsistent face update. More pressure iterations help only if pressure residual is responsible; topology, geometry and buffer timing remain separate suspects.
Two cells and boundary work
Predict the power before changing the controls. The embedded example uses two unit cells, a shared opening of area A, prescribed face speed u and balanced external outward fluxes (q,-q). The shared flux is phi=A u. With unit volumes, the divergences are (phi+q,-phi-q). They sum to zero, even if neither is zero. The pressure test values are prescribed probes, not a solved pressure field.
At A=1/2 m², u=1 m/s, q=1/2 m³/s and p=(1,3) Pa, the pressure-divergence pairing is -2 W. The interior term -(pR-pL) phi is only -1 W. The remaining -1 W is (pL-pR) q, the prescribed boundary work. Set q=0 to recover the homogeneous identity; do not drop the term for general data.
Balanced flow is not zero boundary work
Now q=-1/2 m³/s cancels each cell’s divergence. Interior work is -1 W and boundary work +1 W. The vanishing total does not imply vanishing contributions. The same shared transfer must be used with opposite signs in both cell ledgers. Area changes flux; it does not change the velocity arrow’s fixed scale.
The research dossier derives units, signs, source applicability and the 81-state domain. This is instantaneous finite algebra, not arbitrary mesh assembly, a moving wall or an accepted CFD step.
Exact finite proof and limits
EngineeringFlux.lean proves shared face cancellation, the two-cell update, boundary-work identity and the concrete omission counterexample. It assumes the declared ledger; it does not prove geometry assembly, positivity, numerical execution or physical accuracy. Fresh kernel status is recorded separately from these statements.
Skew samples and normal gradients
At samples L=(-1/2,0), R=(1/2,1/2), T=(-1/2,1) m, take p=x+y+2 Pa. The pressures are (3/2,3,5/2). The two-point contribution along the centre vector predicts a face-normal gradient of 6/5 Pa/m although the exact x gradient is 1. The rendered patch has normal x; its arrows encode pressure gradient, not velocity. Moving the skew control changes the actual sample geometry.
An affine correction with a third sample
Use the third sample to reconstruct b=(p_T-p_L)/t and then a=p_R-p_L-s b. Adding the missing normal component corrects 6/5 by -1/5 to give 1 Pa/m. The linearly interpolated face value 9/4 Pa also needs a -1/4 Pa skew correction. Two samples alone do not determine both gradient components. This finite affine result is not a general nonlinear mesh reconstruction or a collision-mesh reader.
Reconstruction and coupling proof scope
CouplingStudy.lean checks the stated sample, correction and recurrence identities with explicit nonzero denominators. See the complete research derivation for primary sources, units, worked numbers and implementation exclusions. No general geometry conditioning or production pressure solver is certified.