FINITE STRAIN / INTERACTIVE OPERATOR LAB
See strain become
viscous force.
Change the velocity samples. Watch the same retained strain rows gather a deformation, then scatter a resisting force back to the faces.
One stationary, aligned box. Sealed free-slip outer walls · no-slip obstacle · no time advancement
THE ACTUAL MAC SPECIMEN
Face samples, cell strains.
uₓuᵧu_z, near/far z faceselected sector loss
Arrows show the active samples. Prescribed wall traces are eliminated zeros.
TRY A VELOCITY FIELD
Viscosity scales the force and dissipation. It leaves the geometric rows unchanged.
Loading qualified native rows…
FOLLOW ONE ROW
Gather, weight, scatter.
| Active face | E coefficient | Velocity | E u |
|---|
WHY THE CORNER COUPLES COMPONENTSThree fluid quadrants.
Three fluid quadrants.
Two velocity samples.
Kcorner =2 1
1 2
1 2
After reflecting local coordinates and components to put the solid southwest, the unit sector rows are 2U + 2V, 2U and 2V, each weighted by ¼ m³.
Dcorner / μ = ¼(2U + 2V)² + ¼(2U)² + ¼(2V)²
= 2U² + 2UV + 2V²
The shared northeast sector creates the cross term. In those reflected local coordinates, the reconstruction uₓ = U max(y,0)/ℓᵧ, uᵧ = V max(x,0)/ℓₓ vanishes on the two solid half-walls.
The displayed algebra is the operator.
1. Gather a strain
Each row evaluates sᵣ = Σ Eᵣf u_f. Normal rows use ∂ₐuₐ. Engineering shear uses γₐᵦ = ∂ᵦuₐ + ∂ₐuᵦ; the symmetric tensor entry is εₐᵦ = γₐᵦ/2.
2. Weight its square
Normal rows carry 2V. Each shear row carries its actual fluid sector volume v_q. Thus D = μΣ wᵣsᵣ². The shear term is μ v_q γ², including the two symmetric off-diagonal tensor entries.
3. Scatter a force
The same coefficients scatter Ku = EᵀWEu. The stationary viscous force is f = −μKu in newtons. Exact finite algebra gives u·f = −D.
Browser force/work identity u·f + D: — W. Kinetic energy with stored m_f = ρA_fd_f: — J. Coefficient estimate B: — m/kg, UNENCLOSED. These nearest-rounded diagnostics authorize no timestep.
Local rotation can cancel an interior shear row. The surrounding fixed traces can still produce global loss. The affine patterns sample the active faces; prescribed obstacle and outer normal speeds stay zero.
Assumptions, native source and exact Lean statements
This specimen is one exactly aligned internal box with at least one fluid cell of padding. The immutable native operator supplies every row, active face and stored mass. Outer walls impose uₙ = 0 and free-slip tangential traces. The obstacle imposes stationary no slip. Outer shear strains vanish analytically before enumeration; zero rows on included samples remain present.
These controls evaluate fixed finite rows. They do not advance a fluid state or invoke pressure projection. The exact Lean theorems treat stored coefficients, weights and masses as real inputs; they do not prove Rust assembly, JavaScript arithmetic, IEEE error enclosure or continuum convergence.
- gather and strainOperator — finite sums
- transpose_work — uᵀKu = D
- loss_nonnegative — fixed nonnegative weights
- unit_corner_block — the coupled quadratic form
- Download local Lean source · Read the reconstruction and boundary derivation
Inspect the source-bound specimen packet · Immutable native operator source. Packet capture commit: d8771ad83c30644d29929c96534548ce238bb357.