Stationary obstacle pressure and reduced wall shear
The same immutable static box owner now supplies geometry to two bounded field operators. Both borrow its retained triangle surface, physical cell volumes and unique shared face openings. Neither creates another collision mesh or substitutes a binary solid mask. The original geometry lab remains a construction-only record. The new field-response lab plays native pressure and reduced-shear results with independent rational checks.
These operators have different declared boundary models. Pressure uses a sealed stationary container. Shear is a fully developed, tangentially invariant/periodic extrusion above one stationary obstacle wall. They are not a composed three-dimensional fluid step. Arbitrary embedded tensor viscosity, evolving liquid interfaces, moving solids, general material variation and adhesion/contact-angle evolution remain open.
Pressure: geometry, incidence, units and inertia
For each internal open face, let be its negative-side cell, its positive-side cell, the owner’s opening in m², and the separation in metres of its represented nominal grid pressure centers. The unknowns are the positive-volume cells only. A pressure point can lie inside the cut-away part of a cell: this face-area method does not relocate general cut-cell pressure centers or establish a continuum consistency order there.
With constant density in kg/m³, define
is a declared face-area lumped mass. It is not the exact clipped staggered dual-cell mass. The operator is symmetric in its integrated form; in exact arithmetic. No minimum volume, area or distance clamp changes the admitted geometry. Invalid, subnormal, nonfinite or lost-positive coefficients refuse construction.
The owner’s outward flux uses at and at . All outer container faces and fully blocked faces must have exactly zero speed. For an explicit positive step in seconds,
Pressure has units Pa. has units m³/s; the integrated right-hand side, operator result and residual have units m³/s². Pressure correction changes the actual stored binary64 field, rather than merely reporting a residual.
Components, gauges and acceptance
The retained geometry labels active cells by positive-opening connectivity. Each sealed component has its own constant-pressure mode and compatibility condition . The workspace pins a largest-volume wet cell of each component to zero, with the lowest index winning exact volume ties, including isolated singleton components. Dry cells are not unknowns and must have zero right-hand side. An all-dry owner is a valid zero operation. Compatibility is checked independently for every component with a compensated sum and a declared allowance. Incompatible data are refused; no global mean subtraction quietly transfers volume between isolated regions.
The component sum may be nonzero within that arithmetic allowance. In
exact residual accounting, if the non-gauge rows are solved, the pinned
row retains that component sum. Using a largest-volume cell minimizes
its local divergence amplification among the component’s cells. It does
not remove incompatibility, alter the RHS, relax a tolerance or
guarantee convergence. The full residual and actual-field gates still
apply. An exhausted/nonpositive internal PCG product is classified as
ArithmeticFailure, not caller
InvalidParameter.
Deterministic regressions use a first-cell volume , an explicitly roundoff-compatible RHS , and a three-cell flux field with speeds 0.1 and 1 m/s whose represented RHS has a component defect. They distinguish unavoidable compatibility roundoff from amplification caused by choosing a tiny gauge cell. Equal-volume and disconnected-component controls retain the stable tie break. Earlier first-cell-gauge records remain historical; new packets must qualify against the current gauge oracle and source.
Jacobi-preconditioned conjugate gradients operate on the gauge-eliminated system. Every candidate acceptance recomputes the full integrated residual, including gauge rows. With , the exact identities have the signs
Both the full residual norm and must satisfy the caller’s tolerances. After correction, the owner independently differentiates the actual stored face speeds and checks again. A tiny positive cell cannot hide behind a small integrated residual. A contract with volume deliberately fails a loose integrated-residual gate because its local divergence is too large. This is a numerical acceptance control, not a lower bound on all future cut-cell conditioning.
The face-area kinetic energy is . In exact arithmetic the correction satisfies
The right side is numerical residual work. Stationary impermeable walls do no mechanical work. Rust reports all terms, checks the identity with its declared binary64 allowance, and permits no unexplained energy increase. This ledger does not change the declared lumped-mass approximation into an exact geometric mass theorem.
Reduced shear: when scalar diffusion really is Newtonian strain
StaticObstacleShear admits only a box covering the
entire two-dimensional cross-section and extending from below the
container to one lower wall. The fluid above it is a connected channel.
The normal direction may be X, Y or Z; the laboratory uses Y. The upper
wall is stationary no-slip. Tangential directions are
invariant/periodic, so no sealed end-wall response is implied.
For the exact reduced continuum mode , constant Newtonian symmetric strain gives shear stress and dissipation . Thus this scalar reduction is physically justified within that mode. It is not a license to smooth each component independently near arbitrary embedded or free-surface boundaries.
Each fluid layer has volume obtained by summing the owner’s cell volumes, centroid from its actual clipped interval, and mass . Interlayer area is the sum of the owner’s shared open normal faces. The conductance and equal-opposite fluid forces are
For wall-to-centroid distance , stationary no-slip gives . A finite Navier friction coefficient , in Pa s/m, gives the series fluid/wall closure
At there is zero tangential
wall traction. NoSlip is its own boundary mode, not an
enormous finite beta. The effective boundary dissipation combines the
fluid half-layer loss and wall friction. Increasing beta changes
friction; it does not introduce adhesion, wall/interface energy or
wetting.
Forcing, one update and its work ledger
Dynamic viscosity is Pa s;
kinematic viscosity is in
m²/s. Force input is explicit: Density(q) means N/m³, while
Acceleration(a) means m/s² and converts to . With the symmetric traction matrix
, including stationary-wall diagonal
terms, the update is
A tridiagonal direct solve performs one backward-Euler step. There are no hidden substeps. The exact discrete energy and momentum identities are
The source checks both identities and the true momentum equation residual before publishing the field. Unforced kinetic energy cannot increase beyond the declared arithmetic allowance. This is a discrete forced/dissipative response, not a transient continuum-reference or temporal-convergence qualification.
A one-layer hand control has area 1 m², fluid thickness 0.5 m, density 2 kg/m³, viscosity 1 Pa s, and stationary no-slip walls. Its mass is 1 kg and total conductance is 8 kg/s. At s, N/m³, starting from 1 m/s, the exact discrete answer is m/s. Changing the lower closure to finite Navier friction or free slip changes the actual velocity, force and energy ledgers.
Native records and independent controls
The exporter records four pressure cases: partial-box gradient removal, an outside-box control, a disconnected separator, and partial-box rest. Six shear cases record initial rest and eight updates, comparing no-slip/Navier/free-slip and fixed-q/fixed-a density responses. These are 4 pressure projections and 48 bounded shear updates. No historical seven-equation campaign is run or replaced.
The checker recomputes box measures and components with exact rational arithmetic. It checks analytic affine pressures, actual corrected speeds, cellwise divergence and pressure work. A tiny dense rational Gaussian-elimination oracle checks each shear field independently of the Rust tridiagonal algorithm, along with energy and impulse balances. Its 48 rational linear solves are fixture-level discrete controls, not continuum reference integrations. Separately, the checker substitutes the actual recorded old and new fields, plus the independently checked represented coefficients, into the momentum equations and energy/impulse ledgers. The exact reference trajectory never substitutes for those stored fields.
The actual shear equation gate is the native . Pressure energy uses times the actual ledger-term scale; shear energy and momentum use their documented scales. Exported maxima and budgets must be finite and nonnegative. Every exported budget is checked against its formula from the reported terms, with a separate relative allowance for that short arithmetic expression. Reported ledger terms/residuals are compared to exact rational recomputation using times their contributing-term scales. These checks have no unit-sized absolute floor. They are explicit fixture arithmetic allowances, not new operator tolerances or universal IEEE error theorems. The independent ideal-trajectory field allowance remains ; pressure additionally requires independent actual and predicted divergence at most s⁻¹.
Records, executable hashes, qualification receipts, browser captures, generated book/PDF editions and logs stay outside Git. Publication requires a frozen clean source, exact record bytes and matching source hashes. Missing packets produce an explicit source-only page. Browser controls select saved native fields; they do not solve fluid equations in JavaScript. Corruption tests must reject changed geometry, gauges, fields, force semantics and ledgers in normal and optimized Python.
Proof boundary and original research
The existing Discrete and StaticObstacle
Lean modules establish exact-real graph symmetry/energy, incidence
cancellation, component-constant jumps and conditional positive-volume
scaling. ObstacleOperators.lean
adds 24 public theorems and 15 definitions. With pinned Lean 4.19.0 and
the unchanged axiom allowlist, all ten modules and the root compile; 88
public theorems, 118 explicitly expected declarations and 135 total
declarations are audited. The three real negative audit probes and four
source/pin tests pass in normal and optimized Python. This local
qualification invoked the pinned compiler directly with private
dependency artifacts; it is not a new lake build or
hosted-CI receipt.
The new contracts derive signed/absolute residual-divergence scaling, per-label compatibility, matched-mass pressure work, forced shear energy and two-wall momentum, the Navier traction/loss split, and the reduced 3-by-3 symmetric-strain identity. Exact shear coordinate equations and physical coefficient assumptions remain explicit hypotheses. No theorem here proves Rust mesh admission, IEEE arithmetic, PCG/Thomas convergence, complete graph-nullspace identification or arbitrary-domain continuum accuracy. All historical proof receipts and failed numerical evidence retain their own source identities.
Batty, Bertails and Bridson’s original pressure work formulates projection as a kinetic-energy minimization and discusses subgrid geometry and face-area approximations. It motivates the matched coefficient/mass relation; this bounded stationary implementation does not reproduce their moving rigid/deformable coupling. Original paper, 2007. The author’s reference implementation explicitly distinguishes face-area weights from fluid-volume weights.
Batty and Bridson’s viscosity work derives an implicit variational update from symmetric-strain dissipation and emphasizes the coupled traction condition at free surfaces. The present exact shear reduction has neither general free-surface traction nor arbitrary embedded tensor assembly. Original paper, 2008.
The next physical gate is shared staggered interaction geometry for general embedded symmetric strain and an integrated pressure/viscosity step under one consistent boundary model. Variable-density transport, moving/two-way solids, capillarity and contact-angle dynamics need their own contracts and evidence.