--- title: Kenoma Mechanics of Moving Bodies subtitle: An educational research book · Spatial mechanics, evidence and checked claims lang: en --- # Reading a moving body {#reading-a-moving-body} ## Worked reading ### 1. First identify what owns the motion This mannequin starts in an authored neutral pose. Its graph and bound surface describe geometry; they supply neither measured anatomy nor a force law. Orbit the camera without changing the pose. **Observe:** The view changes while the prescribed pose remains neutral. Force, pressure and contact response are not modeled. ### 2. Move a coordinate frame without deforming the body Translate the root by 0.4 scene units in the poser’s horizontal direction. Every local pose coordinate stays the same, so a moved silhouette alone cannot establish tissue strain or mechanical work. **Observe:** The whole character moves together; the pose graph and skin shape are unchanged. This is a prescribed placement, not acceleration under force. ### 3. Change pose, then ask for the missing law The existing hand-on-torso test prescribes a right-hand target and elbow pole. Inverse kinematics chooses bone positions and geometric skinning follows them. A tissue model would additionally need a material law, boundaries, forces and convergence checks. **Observe:** The arm bends toward the torso. The pose does not produce contact pressure or an equilibrium residual; these outputs remain not modeled. A body can look convincing while its forces are wrong. A model can balance its forces while its surface looks wrong. Kenoma's educational book asks how to tell the difference, beginning with quantities that we can calculate and inspect before adding anatomy. The intended reader is a programmer, technical artist, or engineering student who wants to connect geometry, mechanics, computation, and evidence. This edition develops force, torque, energy, anatomical evidence, and a force-driven schematic elbow with activation and a dumbbell load. Seven original resettable 3D laboratories progress through compliant tendon storage, a reduced continuum compression block, a worked tetrahedral FEM/compliant-solver comparison, and a spatial muscle-under-skin/contact strip at identical poses. An eighth, worker-backed experiment jointly solves deforming tissue, distributed tendons and a moving hinge. Its geometry is schematic; the requested anatomical lifting capstone remains under development. A separate evidence viewer contains ten actual atlas meshes, one recorded normalized human trial, and six published model actuator parameter sets. These are three independent evidence streams, not a calibrated person. Three progressive property lessons additionally measure prescribed tetrahedral deformation, compare isochoric volume with cross-section and exterior area, and expose uneven axial strain in a nonuniform bar. A fourth prescribed property lesson separates local from total volume conservation under uneven finite stretch. Three further property lessons add bulk/shear confinement, passive axial load/hold/release, and force-driven unequal 3D blocks with individually preserved volume. The printed edition contains the same explanations, static diagrams, data figures, worked values and original numerical experiments. Clinical or subject-specific prediction is not claimed or required to complete the teaching examples. The content is an **educational extension**. The existing production plans in `docs/plans/` remain separate. A teaching experiment does not silently add a simulator requirement to the Bevy MVP, change its canonical storage format, or establish a production algorithm choice. ## Reading path: measure first, then add a law {#measurement-first-reading-path} Read [force](#force-changes-motion), [torque](#a-force-has-an-application-point) and [energy](#energy-reveals-numerical-error) for the rigid-body quantities and system boundary. Then use the [three property lessons](#measure-deformation-before-choosing-a-muscle-law) in order: measure an imposed deformation; construct prescribed volume preservation; calculate uneven strain under a reduced axial law. Their worked examples introduce length, area, volume, stretch, strain, force and stress before a contact or continuum solver is needed. Continue with [bulk/shear confinement](#compression-bulk-shear-confinement), then [load/hold/release](#dissipative-load-hold-release) to distinguish recoverable storage from viscous loss in the passive axial bar. Then compare [unequal blocks under one force](#serial-specimen-volume), where a declared incompressible material law determines the local stretches and current areas. This separate-block prerequisite does not complete the requested connected continuous specimen with varying cross section, coupled local axial/lateral deformation and volume; that demonstration is not included or established in this edition. Next distinguish [anatomical evidence](#anatomy-is-evidence) from teaching assumptions, and follow the actuator into [elbow motion](#let-forces-move-the-elbow). The later [tissue](#tissue-and-rendered-skin), [tendon/compression](#tendon-tissue-coupling) and [continuum](#from-a-spring-to-a-volume-of-tissue) chapters add material energies, boundary conditions and force-driven deformation. Prescribed constant volume is not a solved material response, and the axial bar is not a full muscle. The [fixed-field projection interlude](#fixed-field-pressure-projection) follows the spatial continuum comparison and precedes interfaces and coupling. Its 27 exact finite weighted-vector statements concern representation at one prescribed state. Spatial solver comparisons and the anatomical research apparatus come after those distinctions; their unfinished scope remains explicit. ## Three different kinds of evidence A **physical assumption** describes the model: a constant force, a perfectly rigid lever, or an ideal spring. A **numerical check** compares the implemented arithmetic with a reference or studies its error. A **formal proof** establishes a precisely stated mathematical claim within its declared domain. Each can be useful; none automatically supplies the other two. The 115 proof cards in this research edition are generated only after checking fourteen source files with Lean 4.19.0: `Mechanics.lean`, `AnatomicalTransfer.lean`, `CoupledMechanics.lean`, `AnatomicalArm.lean`, `ContinuumProperties.lean`, `MaterialResponse.lean`, `MaterialResponseReal.lean`, `MechanicsReal.lean`, `ActuatorConstitutiveReal.lean`, `DissipativeBarReal.lean`, `SerialSpecimenReal.lean`, `MixedLogVolume.lean`, `NonuniformIsochoric.lean` and `ArchitectureForce.lean`. Thirty declarations use integer domains and bundled Std, including five narrow material-response contracts; eighty-five quantify reals with pinned mathlib v4.19.0. These comprise four kinematic identities, five constrained specimen algebra identities, three force/torque/power identities, eleven activation/Gaussian/guarded-series results, eleven local standard-linear-solid energy/relaxation results, twelve homogeneous neo-Hookean serial-block identities, derivatives and ordering results, 27 finite weighted-vector projection results, six declared-gradient/interval/algebraic-cell nonuniform-volume contracts and six scalar architecture-force bookkeeping contracts. The actuator results include real derivatives and conditional nonlinear root existence/uniqueness; the compressible confinement specimen's constitutive derivatives and equilibrium obligations, continuous actuator-mechanics work balances and numerical refinement remain unfinished. Each card reports its exact theorem, assumptions, source hash, implementation link and transitive axioms. The stated real results do not establish floating-point equivalence, general force equilibrium, anatomical validity or biological correctness. This distinction stays visible beside each claim. The new coupled fixture adds a deforming quadratic-tetrahedron block, distributed tensile branches and an implicitly moving hinge whose tissue torque comes from those branches. It is an intermediate engineering experiment. The actual atlas arm, connected attachment patches and interior-axis diagnostics are available separately for review; shared anatomical tendons/aponeuroses and tissue contact are not yet accepted or complete. The earlier schematic strip retains its declared one-way coupling and is no longer presented as completion of the requested anatomical capstone. ## Coordinates and units The original seven laboratories use a right-handed frame: x points right, y points up, and z points out of the page. Laboratories 1–5 solve planar motion or homogeneous block deformation and render them in a 3D scene. Laboratories 6–7 add genuine spatial degrees of freedom; each declares its constitutive and coupling limits. The coupled fixture instead uses +Z downward, so its gravitational potential is −mgz. The separate atlas assembly uses +X anatomical left, +Y posterior and +Z superior. Each viewer identifies its own frame. The scene can be viewed from the front or obliquely; changing the camera changes neither state nor results. A 3D rendering does not turn planar equations into a spatial biomechanical simulation. Store physics in SI units and convert only at input and output. The International System of Units names the metre, kilogram, and second; force has unit newton, energy joule, and torque newton metre. Torque and energy share dimensions but represent different quantities. We write torque in N m to preserve that distinction. [BIPM, SI Brochure, §2.3.4](#source-bipm) | Quantity | Symbol | Unit | Meaning in the laboratories | |:--|:--|:--|:--| | Position | x | m | A coordinate in a specified frame | | Time | t | s | Simulated time, distinct from wall-clock playback | | Mass | m | kg | Inertial mass, strictly positive in controls | | Force | F | N | A vector acting on a specified body | | Torque | τ | N m | A moment about a specified origin and axis | | Energy | E | J | Scalar accounting for a defined system | | Spring stiffness | k | N/m | Force per extension in the ideal linear spring | ## How to use a laboratory Read the model label and the worked example first. Change one control, predict a result, and inspect the numerical output before interpreting the image. Step through time when needed; use Reset to return all physics parameters and the camera to defaults. The laboratories start paused and stop at a bounded step count. Laboratories 1–5 start a new experiment after a non-excitation parameter edit; excitation edits in Laboratories 4–5 retain activation, velocity and time. Laboratory 6 recomputes a static or single-step comparison rather than integrating a trajectory. Laboratory 7 retains current activation, time, pose, velocity and accumulated hinge work/dissipation across parameter edits, then recomputes the spatial shape deterministically. Its angle control explicitly sets pose with zero velocity and clears a domain halt; entering prescribed hold stops motion at the current pose. Reset and the 90° compression fixture deliberately initialize its state. See each laboratory's trace policy before comparing experiments. The first four property lessons update static imposed geometry, an axial calculation or a homogeneous material equilibrium without integrating time. The fifth follows a finite SLS load/hold/unload/recovery protocol; each parameter edit explicitly starts a new experiment and clears its internal-state and energy history. The sixth property lesson recomputes a static, force-driven two-block assembly without changing the requested force; it exposes each finite root residual. The coupled fixture also preserves its tissue coordinates, angle, velocity, activation and time when effort or dumbbell mass changes. Its mass control records the external energy added or removed with the mass; it does not restart the trajectory. Every scene has a text description and static illustration. If WebGL is unavailable, the controls and numerical results still work. All seven mechanics laboratories use original procedural **schematic teaching geometry**: their cylinders, spheres, blocks, grids and arrows are separate from anatomical measurements. The evidence viewer instead shows actual licensed static atlas surfaces, with their source labels, units and limitations. Neither the atlas nor the human-study summaries calibrates the schematic actuator. ## A useful question to carry forward Imagine a forearm holding a dumbbell. Ask: what system did we isolate, what forces act on it, where do those forces act, and what energy enters or leaves it? These questions remain useful whether the next model is a rigid-body joint, a finite-element tissue mesh, or an animation rig. A more detailed surface cannot rescue an unspecified system boundary. The property lessons use the same SI convention with prescribed positive stretches or an explicitly reduced small-strain axial law. The first four update a prescribed geometry or static equilibrium; the fifth integrates an internal viscous strain under its stated axial law, and the sixth solves two separate incompressible homogeneous blocks and independently measures their 3D geometry. Independent geometric measurements and midpoint-integration error remain visible; their exact kinematic claims do not prove a constitutive law or qualify the anatomical tissue envelope. The architecture-force chapter and portable lab connect reference/current area, nominal/Cauchy stress, projection, parallel aggregation and series exchange. Every integrated artifact requires its own complete-book proof receipts, browser/PDF checks and release qualification. The historical nonuniform-volume total was 103 + 6 = 109; this source registry adds six for 115. The preserved standalone qualification does not establish complete-book proof closure, integrated browser/PDF acceptance or anatomical calibration. All example counts, areas, stresses and control ranges are authored. ## Read the model before moving it {#shared-gui-scope} Every chapter now has an example in the shared Kenoma embedded GUI. The label above each view distinguishes illustrative geometry, prescribed kinematics, analytic bookkeeping, a numerical demonstration, and recorded evidence. Orbiting a model does not increase its physical dimension or validate its parameters. An algebraic statement can be kernel-checked while its browser implementation, mesh approximation and biological interpretation remain separate obligations. The simple human poser is an independent artistic system: a graph, generated surface and pose rig with gizmo controls and local SQLite scene files. It has no tissue forces or contact response. Educational model adapters share only presentation components with it. The research apparatus retains its original laws, acceptance criteria and failed-state evidence. Checked cards show their claim, assumptions and limits immediately. Expand a card for its exact statement, source and compilation receipt. The complete Lean appendices are also collapsible on screen; the PDF retains all statements and full sources. A GUI badge never substitutes for the source-bound kernel receipt. ### Interactive 3D: Coordinate and pose inspection Move the root and hand targets; distinguish authored geometry from a measured body. **Evidence class:** Illustrative geometry. **Scope:** No forces, contact, anatomical accuracy or clinical inference. [Open the shared Kenoma GUI](examples.html?chapter=00-scope). # Force changes motion {#force-changes-motion} ## Worked reading ### 1. Predict the first second Start from rest with a constant 4 N horizontal net force on 2 kg. F/m gives 2 m/s², so at 1 s the velocity is 2 m/s and the displacement is ½ × 2 × 1² = 1 m. The grey origin stays fixed; the arrow encodes force, not velocity. **Observe:** Displacement = 1 m; velocity = 2 m/s. Work 4 × 1 = 4 J equals kinetic energy ½ × 2 × 2² = 4 J. ### 2. Double time, quadruple distance Keep the force and mass fixed and advance the analytic solution to 2 s. Acceleration is unchanged. Velocity grows linearly with time, but displacement grows with time squared. No time-stepping solver or display-speed assumption enters this calculation. **Observe:** Displacement increases from 1 to 4 m, while velocity increases from 2 to 4 m/s. Work and kinetic energy both become 16 J. ### 3. Double mass at the same time Keep 4 N and 2 s but double the mass to 4 kg. The acceleration halves to 1 m/s². Both displacement and velocity halve relative to the previous state; the change is caused by mass, not an animation setting. **Observe:** At 2 s, displacement = 2 m and velocity = 2 m/s. Work = kinetic energy = 8 J; the work-minus-kinetic residual is zero. ### 4. Negative direction can mean positive work Return to 2 kg and reverse the force. Acceleration, velocity and displacement all point along negative x. The work is still positive because force and displacement have the same sign: (−4 N)(−4 m) = 16 J. **Observe:** Displacement = −4 m and velocity = −4 m/s, while work and kinetic energy are both +16 J. A negative force is not by itself negative work. A force is not a displacement instruction. For constant mass in an inertial frame, the resultant external force determines acceleration. Doubling force doubles acceleration; doubling mass halves it. Newton's second law and the separation of action-reaction pairs are presented in Dourmashkin's original course notes, §§7.3-7.4. [Newton's laws](#source-force) ## Isolate the body before adding arrows Consider a small object translated horizontally by an actuator. The schematic laboratory includes one constant horizontal net force. If we imagined gravity and a support, their vertical balance would be an additional assumption; this example simply solves the horizontal component. Do not mistake its missing contact solver for evidence that a support is physically correct. For net force $F_x$, mass $m>0$, initial position $x_0=0$, and initial velocity $v_0=0$: $$ a_x=F_x/m,\qquad v_x(t)=a_x t,\qquad x(t)=\tfrac12 a_x t^2. $$ **Text equation:** acceleration equals force divided by mass. Velocity equals acceleration times elapsed time. Position equals half acceleration times elapsed time squared, with both initial conditions zero. This is an analytic solution, so the force laboratory does not accumulate time-integration error. JavaScript still evaluates floating-point arithmetic. We compare selected outputs with exact worked values using numerical tolerances; no theorem in this edition proves the JavaScript implementation. ### Laboratory 1 · Constant force ![A position marker moves along x. Position scale is fixed over the 0–2 s trajectory for the selected mass and force; grid spacing is reported below. Yellow force and violet velocity arrows use separate scales. Values retain SI units.](assets/force.svg) Reference at t = 1 s: m = 2 kg, F = 4 N, x = 1 m, v = 2 m/s. The interactive starts at t = 0 s. Original schematic geometry. **Model:** Analytic planar motion; constant net force; no contact or anatomy. [Open this laboratory in the web edition](index.html#lab-force). ## Worked example Set mass to 2 kg and force to 4 N. The acceleration is 2 m/s². At 1 s the position is 1 m and velocity 2 m/s. At 2 s the position is 4 m and velocity 4 m/s. A negative force produces negative position and velocity; the object accelerates along the negative x direction. **Try:** keep force at 4 N, reset, and increase mass from 2 to 4 kg. At the same simulated time the position is half as large. Then set force to zero: position and velocity stay zero because the initial velocity is zero. A zero force would preserve a nonzero initial velocity in a different experiment. ## Equal and opposite forces belong to different bodies If a tendon pulls a bone, the bone pulls back on the tendon. Those two forces cancel in a combined bone-plus-tendon system. They do not cancel on the isolated bone: only one member of that pair acts on it. This is why a diagram with every arrow drawn on a single object can be misleading. For one scalar component, a pair $f$ and $-f$ sums to zero. That identity is enough to check bookkeeping once we have assumed an action-reaction pair. It does not prove that an actual biological interface follows our chosen constitutive law. **Checked claim force-pair:** An equal and opposite scalar force pair cancels. **Assumptions:** Exact integer forces in a common positive unit scale; the force pair is assumed. ```lean theorem force_pair_cancels (f : Int) : f + (-f) = 0 ``` **Limits:** Does not prove Newton's third law from biology or establish a system boundary. Declaration: `Kenoma.force_pair_cancels`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: propext, Quot.sound; source SHA-256: 6b45c1d9a32fbd0cf6e034d3e4d15d26dc720215afe6845bbbb9d7de07bff2fd. [Full checked source](proofs/Mechanics.lean); [receipt](proof-status.json). The same assumed cancellation also holds for real force components, without introducing an integer SI scale: **Checked claim force-real-pair:** An assumed real equal-and-opposite force pair cancels **Assumptions:** One real force component and its assumed equal-and-opposite partner. ```lean theorem force_pair_cancels (force : ℝ) : force + (-force) = 0 ``` **Limits:** Does not prove an interface follows an action-reaction or constitutive law. Declaration: `Kenoma.MechanicsReal.force_pair_cancels`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: aff41fbe28d5d546f1af36b1187c427cc536ea5c2853017d1539ac35ea645cdf. [Full checked source](proofs/MechanicsReal.lean); [receipt](mechanics-real-proof-status.json). ## Work offers a second calculation A constant horizontal force does work $W=F_x\Delta x$. Starting from rest, the kinetic energy is $K=\tfrac12 m v_x^2$. Substituting the analytic solution gives $W=K$ in this ideal isolated horizontal model. For 4 N over 4 m, both are 16 J. A negative force over a negative displacement also gives positive work. Force direction alone does not determine work's sign; the force-displacement relation does. The next chapter keeps track of the application point of that force, while the energy chapter studies what happens when we replace analytic solutions with time steps. ## Approximation boundary This laboratory omits drag, friction, impacts, variable mass, deformation, actuator limits, and all anatomy. Its moving sphere is a marker for position, not a tissue particle whose radius or volume has medical meaning. Positions beyond the viewing window are reported numerically; the physical trajectory is not clamped to fit the image. ### Interactive 3D: Force, mass and displacement Compare force, mass and elapsed time; check displacement and work against kinetic energy. **Evidence class:** Numerical demonstration. **Scope:** Constant mass and constant horizontal net force; visual arrow lengths are scaled. [Open the shared Kenoma GUI](examples.html?chapter=01-force). # A force has an application point {#a-force-has-an-application-point} ## Worked reading ### 1. Calculate a signed moment A 5 kg load exerts 49.05 N downward in the authored 9.81 m/s² field. The 0.30 m lever is horizontal, so τz = rx Fy = 0.30 × (−49.05) = −14.715 N m. Positive z is counterclockwise viewed toward the origin. **Observe:** Moment arm = 0.30 m and torque = −14.715 N m. A static pose would require an external +14.715 N m hold moment. ### 2. Separate lever length from moment arm Rotate the same 0.30 m lever to 60°. Its horizontal offset is 0.30 cos 60° = 0.15 m, even though its length is unchanged. Gravity acts along the grey vertical line; the orange horizontal segment is the perpendicular offset. **Observe:** Moment arm = 0.15 m and torque = −7.3575 N m: exactly half the horizontal-case magnitude within floating-point precision. ### 3. Put gravity through the pivot At 90°, gravity’s line of action passes through the pivot. The force is still 49.05 N, but its perpendicular offset is zero. This is a posed geometric calculation, not a prediction that the lever stays there without supports. **Observe:** Torque is approximately −9.01 × 10⁻¹⁶ N m and moment arm approximately 1.84 × 10⁻¹⁷ m: numerical zero, not a small physical moment. ### 4. Cross the pivot and reverse the moment At 120° the load is left of the pivot: rx = −0.15 m. Multiplying this negative offset by the downward force gives a positive moment. The unsigned moment-arm magnitude alone cannot tell you the rotation direction. **Observe:** Moment-arm magnitude remains 0.15 m, but torque is now +7.3575 N m. The required static hold moment reverses to −7.3575 N m. A force that passes through a pivot produces no moment about that pivot. The same force applied farther from the pivot can produce a larger moment. The laboratory introduces the moment of a force about a chosen origin; the definitions and axis convention are verified against Dourmashkin's rotational-dynamics notes, §17.1. [Rotational dynamics](#source-torque) ## A planar cross product Let $\mathbf r=(r_x,r_y,0)$ point from the pivot to the application point, and $\mathbf F=(F_x,F_y,0)$ be the force on the lever. The component along z is: $$ \tau_z=(\mathbf r\times\mathbf F)_z=r_x F_y-r_y F_x. $$ **Text equation:** torque around z equals x position times y force minus y position times x force. Positive torque is counterclockwise when viewed from positive z toward the origin. In the schematic example a massless rigid lever of length $L$ supports a point load of mass $m$ at its tip. The angle $\theta$ is measured counterclockwise from the horizontal, not from a clinical elbow coordinate convention. Uniform gravity is $\mathbf F=(0,-mg,0)$, with **illustrative** $g=9.81$ m/s². Therefore: $$ \mathbf r=(L\cos\theta,L\sin\theta,0),\qquad \tau_z=-mgL\cos\theta. $$ This is a posed lever. The slider prescribes its angle; no active muscle, torque controller, angular acceleration, or joint-contact force maintains the pose. A physical static hold would require an opposing moment supplied by some actuator and appropriate support forces. ### Laboratory 2 · Force and lever arm ![A rigid bar extends from a fixed pivot to a load. The yellow arrow points downward. The white projection marks the horizontal distance to the gravity line. This is a posed lever, not an active arm.](assets/torque.svg) Default: m = 5 kg, L = 0.30 m, θ = 0°. Torque about z is -14.715 N m. Original schematic geometry; no anatomical measurements. **Model:** Prescribed pose; massless rigid lever; point load; uniform illustrative gravity. [Open this laboratory in the web edition](index.html#lab-torque). ## Worked values and the moment arm At $m=5$ kg, $L=0.30$ m, and $\theta=0$°, gravity is 49.05 N downward and torque is -14.715 N m. At 90° the line of gravity passes through the pivot and the moment is zero within floating-point tolerance. At 120° the torque becomes positive because the load lies on the other side of the pivot's vertical line. The perpendicular moment-arm magnitude is $d=|L\cos\theta|$. It is not generally the lever length. Its magnitude tells us how strongly gravity acts about this pivot, while the cross product retains direction. **Try:** compare 0°, 60°, and 90°. Predict the torque ratio before moving the slider. At 60° the torque magnitude is half the horizontal value. Move from 89° to 91° and watch the sign change. The exact worked arithmetic can be represented by 300 mm and -49050 mN. Multiplying those scales gives $10^{-6}$ N m per integer product unit. The following theorem checks the integer cross product; division by one million to obtain SI torque is an explicitly stated interpretation. **Checked claim torque-example:** 300 mm crossed with -49050 mN gives -14715000 scaled torque units. **Assumptions:** r=(300,0) mm; F=(0,-49050) mN; product scale 10\^-6 N m. ```lean theorem torque_worked_example : torque 300 0 0 (-49050) = -14715000 ``` **Limits:** Only this exact arithmetic example is checked, not trigonometric slider states. Declaration: `Kenoma.torque_worked_example`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: none; source SHA-256: 6b45c1d9a32fbd0cf6e034d3e4d15d26dc720215afe6845bbbb9d7de07bff2fd. [Full checked source](proofs/Mechanics.lean); [receipt](proof-status.json). ## Combining forces Two forces at the same point contribute torques that add. We can either add their force vectors first or add the two moments. The identity is useful when assembling muscle and external-load contributions around a joint. **Checked claim torque-linearity:** Planar torque is additive in applied force at a fixed point. **Assumptions:** Exact integer planar coordinates and forces; shared positive length and force scales. ```lean theorem torque_linear (rx ry fx fy gx gy : Int) : torque rx ry (fx + gx) (fy + gy) = torque rx ry fx fy + torque rx ry gx gy ``` **Limits:** No arbitrary real coordinates, JavaScript refinement or rounding bound is established. Declaration: `Kenoma.torque_linear`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: propext, Quot.sound; source SHA-256: 6b45c1d9a32fbd0cf6e034d3e4d15d26dc720215afe6845bbbb9d7de07bff2fd. [Full checked source](proofs/Mechanics.lean); [receipt](proof-status.json). For the real quantities in the stated cross product, the corresponding identity is checked separately: **Checked claim torque-real-linearity:** Real planar torque is additive in applied force at a fixed point **Assumptions:** Real planar point coordinates; two real applied forces share that application point and torque origin. ```lean theorem torque_linear (rx ry fx fy gx gy : ℝ) : torque rx ry (fx + gx) (fy + gy) = torque rx ry fx fy + torque rx ry gx gy ``` **Limits:** No geometric differentiation or floating-point equivalence. Declaration: `Kenoma.MechanicsReal.torque_linear`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: aff41fbe28d5d546f1af36b1187c427cc536ea5c2853017d1539ac35ea645cdf. [Full checked source](proofs/MechanicsReal.lean); [receipt](mechanics-real-proof-status.json). It is unsafe to add torques computed around different origins without transforming them. If the new origin is at $\mathbf o$ relative to the old one, the position becomes $\mathbf r-\mathbf o$, and: $$ (\mathbf r-\mathbf o)\times\mathbf F =\mathbf r\times\mathbf F-\mathbf o\times\mathbf F. $$ **Checked claim torque-origin:** Changing the torque origin subtracts origin cross force. **Assumptions:** Exact integer planar coordinates and forces in common positive scales. ```lean theorem torque_origin_shift (rx ry ox oy fx fy : Int) : torque (rx - ox) (ry - oy) fx fy = torque rx ry fx fy - torque ox oy fx fy ``` **Limits:** This is an algebraic identity, not a claim that torque is independent of origin. Declaration: `Kenoma.torque_origin_shift`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: propext, Quot.sound; source SHA-256: 6b45c1d9a32fbd0cf6e034d3e4d15d26dc720215afe6845bbbb9d7de07bff2fd. [Full checked source](proofs/Mechanics.lean); [receipt](proof-status.json). ## Internal forces and couples Equal and opposite forces can have zero resultant force and a nonzero resultant torque. Think of two forces acting along different parallel lines: they form a couple. Force cancellation alone is not enough to infer moment cancellation. For a central pair between positions A and B, let the force at A be $k(\mathbf B-\mathbf A)$ and the force at B its negative. Their summed moment vanishes because both forces act along the joining line. The theorem checks this specifically for planar integer coordinates and integer k. **Checked claim central-pair:** Equal opposite central forces produce zero summed planar torque. **Assumptions:** Force at A is k(B-A); force at B is its negative; integer k and positions. ```lean theorem central_pair_torque (ax ay bx byy k : Int) : torque ax ay (k * (bx - ax)) (k * (byy - ay)) + torque bx byy (-(k * (bx - ax))) (-(k * (byy - ay))) = 0 ``` **Limits:** Noncentral pairs can form a couple. Tissue/contact models are not verified by this theorem. Declaration: `Kenoma.central_pair_torque`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: propext, Quot.sound; source SHA-256: 6b45c1d9a32fbd0cf6e034d3e4d15d26dc720215afe6845bbbb9d7de07bff2fd. [Full checked source](proofs/Mechanics.lean); [receipt](proof-status.json). This assumption should be inspected before applying it to a tissue model. A model that exchanges angular momentum through distributed stress or explicit bending moments needs the corresponding moment balance, not a point-force argument with missing terms. ## Connecting torque to energy The point load has gravitational potential $U=mgL\sin\theta$ relative to its horizontal position. Differentiating with respect to angle in **radians** gives $\tau_z=-dU/d\theta$. A finite-difference numerical test checks this relation for the implemented lever. It does not establish a floating-point theorem. This independent calculation is valuable because it can reveal a sign convention or degree/radian conversion error. ### Interactive 3D: Moment arm in three dimensions Change the planar lever angle and inspect the moment vector. **Evidence class:** Numerical demonstration. **Scope:** Planar mechanics rendered in 3D; no joint or anatomical inference. [Open the shared Kenoma GUI](examples.html?chapter=02-torque). # Energy reveals numerical error {#energy-reveals-numerical-error} ## Worked reading ### 1. Expose energy created by the update Use the same 1 kg, 40 N/m spring starting at x = 0.20 m and v = 0. At h = 0.05 s, explicit Euler multiplies energy by 1 + 40h² = 1.1 each step. After 40 steps, t = 2 s and E = 0.8 × 1.1⁴⁰. **Observe:** Energy grows to 36.2074 J, a maximum deviation of 4425.93%. Position is 1.27918 m, versus analytic 0.199316 m at the same 2 s. ### 2. Change the update, preserve the experiment Keep the initial state, step size and 2 s endpoint. Updating velocity before position changes the numerical method. Its endpoint energy looks much closer, but inspect the maximum over every completed step rather than trusting a single snapshot. **Observe:** Final energy is 0.766327 J, while maximum energy deviation is 18.7744%. Absolute position error is 0.00550736 m. Bounded-looking motion does not imply exact conservation. ### 3. Use both endpoint accelerations Velocity Verlet uses old and new acceleration. The same 40 steps reach the same physical time. At this endpoint the energy happens to lie very near 0.8 J; the maximum over all samples prevents that phase coincidence from hiding error. **Observe:** Final energy is 0.799632 J, but maximum energy deviation is 2.49928%. Position error is 0.00116381 m. These are measured numerical errors, not a conservation proof. ### 4. Refine at equal elapsed time Reduce h fivefold and use five times as many steps so the endpoint remains 2 s. Comparing equal step counts here would compare different experiments. The finer run uses the same physical model and no retuned constants. **Observe:** Maximum energy deviation falls to 0.0999895% and endpoint position error to 0.0000353055 m. Both improve in this experiment; this does not establish a universal error bound. Energy accounting can expose a trajectory that looks smooth while gaining energy from its numerical update. The definitions of kinetic energy and work are verified against Dourmashkin's notes, §§13.2-13.6. [Energy and work](#source-energy) The numerical experiment below is original code and analysis in this repository; it is a synthetic oscillator experiment, not new biological data. ## An ideal oscillator with a reference solution A mass attached to a linear spring has extension x and velocity v. There is no damping, gravity, contact, or active energy input. Its equation and total mechanical energy are: $$ m\ddot x=-kx,\qquad E=\tfrac12 mv^2+\tfrac12 kx^2. $$ **Text equation:** mass times acceleration equals negative stiffness times extension. Energy equals half mass times velocity squared plus half stiffness times extension squared. The default parameters are $m=1$ kg, $k=40$ N/m, $x_0=0.20$ m, and $v_0=0$ m/s. Initial energy is 0.80 J. The angular frequency is $\omega=\sqrt{k/m}$, and the reference trajectory is $x(t)=x_0\cos(\omega t)$, $v(t)=-\omega x_0\sin(\omega t)$. ### Laboratory 3 · Numerical energy ![A spring connects a wall to a mass marker. Extension is visually exaggerated and fitted to the view. The energy chart shows a solid numerical trace and a dashed initial-energy reference. Read numeric values when the chart rescales.](assets/energy.svg) Initial state: m = 1 kg, k = 40 N/m, x = 0.20 m, v = 0 m/s, E = 0.80 J. Default symplectic Euler step h = 0.02 s. Original schematic geometry. **Model:** Ideal undamped linear spring; fixed physics steps; 12 simulated seconds per trajectory; 120–2,400 fixed steps for the supported h. [Open this laboratory in the web edition](index.html#lab-energy). ## Three ways to take a step Let h be a positive time step in seconds, and $a_n=-kx_n/m$. **Explicit Euler** updates both values from the old state: $$ x_{n+1}=x_n+h v_n,\qquad v_{n+1}=v_n+h a_n. $$ **Symplectic Euler** updates velocity before position: $$ v_{n+1}=v_n+h a_n,\qquad x_{n+1}=x_n+h v_{n+1}. $$ **Velocity Verlet** includes the new acceleration: $$ x_{n+1}=x_n+h v_n+\tfrac12 h^2 a_n,\qquad v_{n+1}=v_n+\tfrac12 h(a_n+a_{n+1}). $$ The methods are implemented separately from rendering. Playback advances fixed simulation steps and reports their index and elapsed time; it never inserts the browser's frame duration into the physics formula. Play advances approximately one simulated second per wall-clock second. **Run to 12 s** finishes the current trajectory in bounded frame batches; either running mode can be paused and resumed. Each supported h reaches the same 12-second endpoint (120–2,400 steps), and every physics sample is retained even when the display redraws only once per frame. The readout reports completed/total steps, elapsed/target time, the maximum energy deviation over all samples and the current position error against the analytic reference. Download trace preserves all samples and these measurements. A parameter change starts a new trajectory. Reset reproduces the same sequence for a given method and step size. ## Why explicit Euler gains energy Substitute the explicit update into the quadratic energy and expand. The mixed terms cancel, leaving: $$ E_{n+1}=\left(1+\frac{k}{m}h^2\right)E_n. $$ For positive k, m, and h, every nonzero-energy step multiplies energy by a factor greater than one. Making h smaller delays the growth; it does not produce bounded energy over arbitrarily long time with fixed h. This is a paper-and-pencil derivation for the ideal oscillator. No Lean theorem in this edition checks that integrator identity. For the other two methods, the linear oscillator's usual bounded regime is $h\sqrt{k/m}<2$. Even inside that regime, neither method preserves the exact physical energy at every step. The observed energy oscillates, and phase error accumulates. A stable picture and an accurate time history are different checks. ## Original reproducible experiment Run each method with the same initial conditions over 12 simulated seconds. Compare h = 0.01, 0.02, and 0.05 s, measuring the maximum absolute relative energy deviation over **all** sampled steps and the final absolute position error against the analytic reference. No wall-clock speed claim is made. The table below is generated by executing `web/mechanics.mjs`, the same pure physics module used by the browser. | Method | h (s) | Steps | Max relative energy deviation (%) | Final position error (m) | |:--|--:|--:|--:|--:| | explicit | 0.01 | 1200 | 1.194e+04 | 1.849 | | explicit | 0.02 | 600 | 1.368e+06 | 23.11 | | explicit | 0.05 | 240 | 8.595e+11 | 5848 | | symplectic | 0.01 | 1200 | 3.266 | 0.004304 | | symplectic | 0.02 | 600 | 6.752 | 0.01165 | | symplectic | 0.05 | 240 | 18.78 | 0.0622 | | verlet | 0.01 | 1200 | 0.09999 | 0.00122 | | verlet | 0.02 | 600 | 0.4 | 0.005052 | | verlet | 0.05 | 240 | 2.5 | 0.03887 | The final position error can be small by phase coincidence; it should not be used alone to select a method. The energy maximum shows explicit Euler's growth even when a snapshot happens to cross the reference. Symplectic Euler has a larger oscillating energy deviation than Verlet for these settings. Both still require refinement studies for any intended application. **Try:** reset with explicit Euler and h = 0.05 s. Step, play or run to 12 s to see the energy increase. Reset with Verlet at the same h. Compare numeric energy with the dashed 0.80 J reference, then halve h and compare again. The plotted vertical range adapts to the computed energy; read its numeric maximum so that rescaling cannot disguise instability. ## A modest formal claim With a nonnegative exact integer mass, the numerator $m(v_x^2+v_y^2)$ is nonnegative. With positive unit scales and the factor one half, it corresponds to nonnegative kinetic energy. That claim says nothing about conserving energy from one step to the next. **Checked claim kinetic-sign:** The exact numerator m(vx²+vy²) of twice kinetic energy is nonnegative. **Assumptions:** Integer mass m ≥ 0; integer velocity coordinates; positive SI scale factors. ```lean theorem kinetic_numerator_nonnegative (m vx vy : Int) (hm : 0 ≤ m) : 0 ≤ twiceKinetic m vx vy ``` **Limits:** The factor 1/2 and unit scales are interpreted in prose; no integrator conservation or biological validation. Declaration: `Kenoma.kinetic_numerator_nonnegative`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: propext; source SHA-256: 6b45c1d9a32fbd0cf6e034d3e4d15d26dc720215afe6845bbbb9d7de07bff2fd. [Full checked source](proofs/Mechanics.lean); [receipt](proof-status.json). ## Approximation boundary The spring is linear at all extensions, including compression, and has no tensile-only constraint. It is therefore not a tendon model. An active muscle adds energy through a contraction law; a dissipative tissue removes energy; contact may exchange or dissipate energy. Before interpreting their energy residuals, include those terms and define the model's system boundary. Before adding those material mechanisms, continue to [the three property lessons](#measure-deformation-before-choosing-a-muscle-law). They measure an imposed shape, construct constant-volume kinematics, and calculate nonuniform strain with one declared axial law. This separates geometric observations from the force and energy models that will later produce them. ### Interactive 3D: Oscillator state and energy Compare integrators at equal elapsed time, then refine the step size and inspect maximum sampled energy error. **Evidence class:** Numerical demonstration. **Scope:** One-dimensional oscillator rendered in 3D; numerical drift is not a checked conservation theorem. [Open the shared Kenoma GUI](examples.html?chapter=03-energy). # Measure deformation before choosing a muscle law {#measure-deformation-before-choosing-a-muscle-law} ## Worked reading ### 1. Start with the reference tetrahedron Unit stretches and zero shear prescribe the identity map. Compare the determinant with volume measured independently from the closed boundary triangles. **Observe:** Both volume ratios are 1; Green strain is zero up to floating-point roundoff. The coincident surfaces are expected. ### 2. Lengthen one direction Only the X direction is stretched. The transverse stretches stay 1, so det F = 1.2 × 1 × 1 = 1.2. **Observe:** Both volume ratios become 1.2. Green strain norm is 0.22; these are imposed geometric changes, not a force response. ### 3. Change shape while keeping volume Restore axial stretch to 1 and impose shear 0.25. The triangular deformation matrix still has unit determinant, but its reference Y-directed edge becomes longer. **Observe:** J stays 1 while Green strain norm is about 0.179518 and Y-line stretch is about 1.03078. Constant volume does not mean zero strain. ### 4. Rotate without adding strain Rotate the same sheared geometry by 90 degrees. Rigid rotation changes world-space positions but preserves edge lengths and F-transpose F. **Observe:** The geometry rotates; J, Green strain norm and Y-line stretch match the previous step. No material law or equilibrium has been introduced. These progressive property lessons separate geometry, constitutive response and equilibrium. A shape that keeps its total volume can still have uneven local compression; a shape that looks muscular has not thereby passed a mechanical test. The anatomical capstone retains its failed cases and its force and geometry gates. Start here after [force](#force-changes-motion), [torque](#a-force-has-an-application-point) and [energy](#energy-reveals-numerical-error). First ask **what changed in the shape?** Then impose a simple volume relation. Finally introduce one axial force law to ask why different sections strain differently. No contact solver, anatomical mesh or finite-element assembly is needed for these three lessons. The [later material chapter](#from-a-spring-to-a-volume-of-tissue) adds energy, stress and equilibrium in three dimensions. | Quantity | Units | How to read it here | |:--|:--|:--| | Reference/current positions $X,x$; length $L$ | m | Positions before/after an imposed change; distance along the bar | | Cross-section $A$; boundary volume $V$ | m²; m³ | Area across the axial direction; volume enclosed by oriented faces | | Stretch $\lambda,b$; volume ratio $J$ | dimensionless | Current/reference length or volume; one means unchanged | | Deformation gradient $F$; strain $E_G,\epsilon$ | dimensionless | Local shape map; measures of deformation, not forces | | Axial resultant $N$ | N | Total tensile force through a section, not stress at a point | | Modulus $E$; active-stress offset $\sigma_0$ | Pa = N/m² | Parameters of the declared axial material law | | Activation coefficient $a$ | dimensionless, 0–1 | Static multiplier of the authored stress offset, not an integrated activation trajectory | | Compliance $C$ | m/N | Extension per applied force in the passive bar | The symbol $F$ below is a deformation matrix, not the force vector of Laboratory 1. The bar's $E$ is a modulus, not energy in joules; $E_G$ denotes Green strain. Stretches and strains have no units: stretch 1.2 means 20% longer, while axial strain 0.01 means 1% extension in the small-strain bar. These static property lessons do not advance time, integrate activation or calculate metabolic energy. ## 1. Measure a prescribed deformation **Question:** if we move the vertices ourselves, how do we measure stretch, shear and volume change? The reference tetrahedron has four vertices; its three edges from vertex zero are stored as the columns of $D_m$. The current edges form $D_s$. Multiplying by $D_m^{-1}$ removes the original edge scale, so $F$ maps a small reference edge to its current edge. You can begin with the numerical stretch and volume readouts before working through this matrix notation. For reference vertices $X_i$ and current vertices $x_i$, each in metres, construct edge matrices $D_m=[X_1-X_0, X_2-X_0, X_3-X_0]$ and $D_s=[x_1-x_0,x_2-x_0,x_3-x_0]$. A nondegenerate, positively oriented reference is required. The affine deformation gradient, local volume ratio and Green strain are $$F=D_sD_m^{-1},\qquad J=\det F,\qquad E_G=\frac12(F^TF-I).$$ The controls impose $F=R_z(\theta)U$ with $U=\begin{pmatrix}s_x&k&0\\0&s_y&0\\0&0&s_z\end{pmatrix}$, then add a common translation: $x=FX+t$. Column vectors are used; $U$ acts first, the rigid rotation second. The off-diagonal coefficient $k$ is entered directly; this is not a shear matrix multiplied after a separately defined stretch. The diagonal coefficients are not all material-line stretches when shear is present. The reference X, Y and Z line stretches are $s_x$, $\sqrt{s_y^2+k^2}$ and $s_z$, respectively; the browser independently measures them from the transformed edges. Rotation and translation leave those line lengths unchanged. Translation cancels from the edges. A rigid rotation has $E_G=0$; simple shear can have $J=1$ while $E_G\ne0$. Volume preservation does not mean absence of strain. The independent measurement uses the oriented boundary triangles. For any common origin $o$, with outward face ordering, $$V_{\partial}=\frac16\sum_{(a,b,c)}(a-o)\cdot[(b-a)\times(c-a)].$$ The browser computes this triangle sum without calling the determinant helper. It reports $V_{\partial}/V_{\partial,0}-J$, in dimensionless units, rather than assuming agreement. Negative signed volume or nonpositive $J$ rejects the candidate and retains the last valid displayed state. This four-node affine test does not certify curved P2 elements or a whole moving tissue envelope. ### Property lab 1 · Measure deformation ![Authored 80 × 60 × 50 mm reference. Gray is reference; blue is prescribed geometry. This lesson imposes kinematics and does not solve force equilibrium.](assets/property-deformation.svg) Authored 80 × 60 × 50 mm reference. Gray is reference; blue is prescribed geometry. This lesson imposes kinematics and does not solve force equilibrium. [Open the interactive lesson](index.html#lab-property-deformation). **Try and predict.** Set all three diagonal coefficients to 1, shear and rotation to 0. The measured $J$ and boundary-volume ratio should both be 1, and Green strain should be zero. Change only translation X to 30 mm: it moves the tetrahedron but changes neither measurement. Next set axial stretch to 1.2: expect $J=1.2$. Restore unit diagonal coefficients and set shear to 0.25: volume stays the same, but Green strain is nonzero. Rotation alone also keeps volume and strain unchanged; the components of $F$ can still change. The controls prescribe the vertices. This lab measures $F$, $J$, Green strain and an independent boundary volume; it solves no forces, material energy, contact or equilibrium. A valid positive volume is a geometry check, not evidence of a realistic muscle response. **Checked claim volume-edge-translation:** Adding one real translation to all four vertices leaves the tetrahedral edge matrix unchanged. **Assumptions:** Four real three-dimensional vertex vectors; the same translation acts on each vertex. A meaningful physical deformation gradient additionally requires a nondegenerate reference tetrahedron. ```lean theorem edge_translation_invariant (v : Fin 4 → Fin 3 → ℝ) (t : Fin 3 → ℝ) : edgeMatrix (fun j i => v j i + t i) = edgeMatrix v ``` **Limits:** No floating-point equivalence, boundary triangulation, inversion detection, equilibrium or biological claim is established. Declaration: `KenomaProperties.edge_translation_invariant`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 33945605131f1a0fc3568467cbc1026463867a8fa241fb25e2174c23a229f12e. [Full checked source](proofs/ContinuumProperties.lean); [receipt](property-proof-status.json). **Checked claim volume-det-compose:** The determinant of a product of real 3 by 3 matrices is the product of their determinants. **Assumptions:** Real square matrices; this supports F=Ds\*inverse(Dm) with separately assumed invertible reference geometry. ```lean theorem determinant_composition (A B : Matrix (Fin 3) (Fin 3) ℝ) : Matrix.det (A * B) = Matrix.det A * Matrix.det B ``` **Limits:** Does not certify JavaScript matrix multiplication/inversion, mesh orientation or boundary measurements. Declaration: `KenomaProperties.determinant_composition`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 33945605131f1a0fc3568467cbc1026463867a8fa241fb25e2174c23a229f12e. [Full checked source](proofs/ContinuumProperties.lean); [receipt](property-proof-status.json). ## 2. Exact isochoric kinematics **Question:** what lateral change would keep a rectangular block's volume exactly fixed while its axial length changes? *Isochoric* means constant volume. Here we impose the answer; no pressure or material stiffness chooses it. Prescribe $F=\operatorname{diag}(\lambda,b,b)$ with positive dimensionless stretches. Then $J=\lambda b^2$. In the isochoric construction $b=1/\sqrt\lambda$, so $J=1$ in exact real arithmetic. The interactive controls also allow independent stretches, which need not preserve volume. This is a kinematic construction, not a minimization or a muscle contraction law. For the rectangular reference, $L=\lambda L_0$, $A=b^2A_0$ and $AL=JV_0$. Cross-section area is the area normal to the axial direction, measured from two transverse edges. Exterior area is the sum of all boundary-triangle areas. They have the same units, square metres, but different mechanical meanings. Neither is automatically physiological cross-sectional area (PCSA). The independent boundary-volume measurement remains visible when the isochoric toggle is selected. ### Property lab 2 · Volume and cross-section ![Authored 80 × 60 × 50 mm reference. Gray is reference; blue is prescribed geometry. This lesson imposes kinematics and does not solve force equilibrium.](assets/property-isochoric.svg) Authored 80 × 60 × 50 mm reference. Gray is reference; blue is prescribed geometry. This lesson imposes kinematics and does not solve force equilibrium. [Open the interactive lesson](index.html#lab-property-isochoric). **Try and predict.** At axial stretch $\lambda=0.8$, the 0.08 m reference length becomes 0.064 m. The imposed lateral stretch is $b=1/\sqrt{0.8}\approx1.11803$, so the reference cross-section 0.003 m² grows to 0.00375 m². Their product remains 0.00024 m³. Switch to independent stretches and set $b=1$: the same shortening now gives $J=0.8$. Read cross-section area and exterior area separately; they need not change by the same factor. This volume-preserving motion is **prescribed kinematics**, not material-driven volume redistribution. The free-side compression example in [Laboratory 5](#tendon-tissue-coupling) later determines lateral stretch from a material law and boundary conditions, rather than imposing this square-root relation. Neither lesson specifies a complete deforming muscle. **Checked claim volume-diagonal:** The real axial/lateral diagonal deformation diag(lambda,b,b) has determinant lambda × b × b. **Assumptions:** Real stretches; physical use additionally requires lambda>0 and b>0. Unit determinant follows whenever the stated product equals one. ```lean theorem axial_determinant (lambda b : ℝ) : Matrix.det (axialMatrix lambda b) = lambda * b * b ``` **Limits:** A kinematic identity; no force equilibrium, finite-bulk incompressibility, material response or biological correctness follows. Declaration: `KenomaProperties.axial_determinant`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 33945605131f1a0fc3568467cbc1026463867a8fa241fb25e2174c23a229f12e. [Full checked source](proofs/ContinuumProperties.lean); [receipt](property-proof-status.json). **Checked claim volume-isochoric-sqrt:** For real lambda>0, b=1/sqrt(lambda) is positive and diag(lambda,b,b) has unit determinant. **Assumptions:** Positive real axial stretch and the exact real square-root construction. ```lean theorem isochoric_sqrt_construction (lambda : ℝ) (hlambda : 0 < lambda) : 0 < 1 / Real.sqrt lambda ∧ Matrix.det (axialMatrix lambda (1 / Real.sqrt lambda)) = 1 ``` **Limits:** Does not prove binary64 sqrt/division or measured browser volume is exact, and does not establish a passive or active equilibrium. Declaration: `KenomaProperties.isochoric_sqrt_construction`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 33945605131f1a0fc3568467cbc1026463867a8fa241fb25e2174c23a229f12e. [Full checked source](proofs/ContinuumProperties.lean); [receipt](property-proof-status.json). ## 3. Nonuniform cross-section: a reduced axial oracle **Question:** can one constant tensile force produce different strain along a bar? Here shape is no longer prescribed at every section. We assume a one-dimensional material law and axial balance, then calculate strain. Positive strain is extension; negative strain is compression. The coordinate $s$ runs along the reference bar; $N/A$ is axial stress in pascals. Larger area or modulus reduces passive strain at the same force. Take a small-strain bar with length $L$ in metres, positive area $A(s)$ in square metres, constant modulus $E$ in pascals, no distributed axial load, and a tensile-positive resultant $N$ in newtons. Force balance gives $dN/ds=0$. The passive law gives $\epsilon(s)=N/[EA(s)]$, so $$\Delta L=\int_0^L\epsilon(s)\,ds=N\int_0^L\frac{ds}{EA(s)}.$$ A1 is the reference area at s=0 and A2=rA1 is the end area at s=L. The ratio permits either direction of taper: for r<1, A2 is the narrow end; for r>1, A1 is the narrow end. The readout derives narrow/wide areas from the selected geometry. For linear **area** taper $A(s)=A_1[1+(r-1)s/L]$, the exact compliance is $L\ln(r)/[EA_1(r-1)]$, with limit $L/(EA_1)$ at $r=1$. Numerical midpoint integration is compared with that analytic integral. Linear area taper is a separate geometric assumption from a radius taper. The exterior surface influences surface traction and contact; it does not replace $A(s)$ in this axial law. Add a separately declared uniform active-stress offset $a\sigma_0$, still under this reduced small-strain law: $\epsilon=N/(EA)-a\sigma_0/E$. With both ends fixed, $\int\epsilon ds=0$ determines the constant $N$. Two equal-length segments with $A_2=2A_1$ and $a\sigma_0/E=0.01$ give $N=(4/3)A_1a\sigma_0$, narrow strain $+1/300$ and wide strain $-1/300$. Local extension and compression coexist even though total length is fixed. This offset model has no force–length/velocity dependence, transverse equilibrium, pennation, ECM, fluid or anatomical calibration; it is not a complete active muscle model. ### Property lab 3 · Uneven axial strain ![Small-strain constant-modulus bar; no distributed axial load. Strain by axial position, with blue extension and red compression. Area controls an axial resultant, not a complete muscle law.](assets/property-tapered.svg) Small-strain constant-modulus bar; no distributed axial load. Strain by axial position, with blue extension and red compression. Area controls an axial resultant, not a complete muscle law. [Open the interactive lesson](index.html#lab-property-tapered). **Try and predict.** In passive mode, keep the default geometry and modulus and change force from 0.3 to 0.6 N: every strain and the total extension double. Doubling the modulus instead halves them. In active fixed-end mode, choose two equal-length segments and keep area ratio 2, activation 1 and active stress 1,000 Pa at modulus 100,000 Pa. The narrow section extends by $1/300$ and the wide section compresses by $1/300$, while their total length change is zero. Passive force is disabled in that mode because the fixed-end compatibility determines the reaction; active controls are disabled in passive mode. This bar solves an axial resultant and axial strain under its stated assumptions. It does not determine lateral stretch, cross-section evolution, transverse stress, contact, three-dimensional fibre aggregation or muscle shape. The area profile is an input; neither zero net extension nor the active-stress offset supplies the missing transverse equilibrium. Refining midpoint cells improves the integral of this same reduced law, not its biological scope. The illustrative 5% small-strain warning uses the true endpoint extrema of this monotone positive-area law, independent of midpoint display resolution. It is a warning about this approximation, not material validation. The executable oracle is [the tapered-bar module](web/tapered-bar.mjs). Tests check the logarithmic integral, refinement and the two-segment fixed-end case. Its scope is numerical evidence for this declared reduced law; the kinematic Lean claims above do not prove its mechanics. Continue with [anatomical evidence](#anatomy-is-evidence) before assigning these quantities to a named muscle. When you reach [tissue and rendered skin](#tissue-and-rendered-skin), reuse the measurements above while adding a material law and boundary forces. The [next material-response lesson](#compression-bulk-shear-confinement) adds bulk/shear and unilateral confinement controls. [Load/hold/release](#dissipative-load-hold-release) now adds a bounded passive axial SLS lesson. [The two-block specimen](#serial-specimen-volume) then solves unequal 3D stretches and current areas under one force, with an explicit incompressible material constraint. Measured fibre-to-muscle aggregation and force–length/velocity lessons remain pending, as recorded in the [coverage chapter](#coverage-and-evidence). ## What the exact claims cover The freshly checked real-number proof bundle establishes edge translation invariance, determinant composition, the actual diagonal determinant and the positive square-root isochoric construction. The four claims above are compiled from their displayed real definitions against pinned mathlib. The edge and matrix identities do not prove the oriented boundary-triangle oracle, and the isochoric identity does not prove a free-side material equilibrium. Separate numerical and browser tests cover the implemented controls and boundary measurements. Neither class of test validates measured biological parameters or resolves the capstone's local compression and full nodal stationarity failures. ### Interactive 3D: Reference and deformed tetrahedron Change axial stretch and shear; compare determinant with triangle-measured volume. **Evidence class:** Prescribed kinematics. **Scope:** Prescribed affine map, not force equilibrium or tissue response. [Open the shared Kenoma GUI](examples.html?chapter=09a-properties). # Uneven stretch and local volume {#nonuniform-local-volume} ## Worked reading ### 1. Begin with uniform stretch Mean stretch is 1 and the uneven-stretch amplitude is zero. Local compensation is then the identity everywhere. **Observe:** Local J and both total volume ratios are 1 up to triangle-sum roundoff. ### 2. Let local volume changes cancel The endpoint axial stretches are 0.6 and 1.4. Without transverse compensation, J equals the local axial stretch; the average remains 1. **Observe:** Total continuum volume remains 1 while local J spans 0.6–1.4. A correct global volume cannot establish local incompressibility. ### 3. Compensate every material section Set transverse stretch to 1/sqrt(lambda) at each section. This makes the exact map locally isochoric, but eight straight mesh cells only approximate its curved boundary. **Observe:** Local J is 1 throughout. The measured mesh ratio is about 1.00248, an excess of 0.00247970 rather than an exact mesh-volume guarantee. ### 4. Refine the geometric measurement Keep the same continuum map and increase only longitudinal cells from 8 to 128. This tests the straight-boundary approximation, not a different material. **Observe:** Mesh-volume error falls to about 0.00000968811. The exact local and continuum volume ratios remain 1; the nonzero numerical discrepancy stays visible. The previous property lesson measured homogeneous deformations. Now prescribe a smooth deformation along one reference prism: neighbouring material sections can stretch differently while each point preserves its volume. This is an imposed geometric map, with no force balance, passive material response, activation or anatomical prediction. It is a different construction from the later serial specimen, whose two separate homogeneous blocks are joined by a spacer. ## A complete gradient, including shear {#nonuniform-complete-gradient} Let the material coordinate satisfy $0\le S\le L_0$, with $L_0>0$, mean stretch $m>0$ and dimensionless uneven-stretch amplitude $-10 the algebraic straight-cell volume ratio is at least one; this does not certify a mesh implementation. **Assumptions:** Exactly the parameters and hypotheses in the full Lean statement. ```lean theorem straight_cell_ratio_ge_one (r : ℝ) (hr : 0 < r) : 1 ≤ straightCellRatio r ``` **Limits:** Declared finite kinematics only; no formal derivative, integration, triangulation, floating-point or physical equilibrium refinement; no biological claim. Declaration: `KenomaNonuniform.straight_cell_ratio_ge_one`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 99029516cf26fca5a82cbd2971c13f9d9d1e6a10face1d71704a6185b7a731ea. [Full checked source](proofs/NonuniformIsochoric.lean); [receipt](nonuniform-real-proof-status.json). ## Accepted source and remaining dependencies {#nonuniform-evidence-boundaries} Independent acceptance applies to exact source `15c624c32378b9c773a3d0c25a65150804b68c90`, following mathematical, model, browser and PDF review of `8fd21a3177242fde3dca2a3dffa1c5f4c0350bdd`. Their sole difference corrects the browser receipt's description of the six Real contracts. The complete original contribution and its claim inventory are preserved unchanged. The book registry adds display metadata and copies the exact Lean source; all original 103 proof identities and anatomy references remain unchanged. [Source composition and independent acceptance](nonuniform/composition.json) accompany the portable edition. This lesson supplies no material law or equilibrium solve. New continuous passive-specimen, scalar tension/mass controller and anatomical-capstone sources remain excluded. The next anatomical dependency is displacement-space and material/pressure coupling adequacy at isolated matched-pose fixtures, against retained local compression and full-nodal residual failures, before force rematching or new trajectories. Prescribed local volume conservation does not resolve that dependency or establish anatomical completion. ### Interactive 3D: Uneven stretch and local volume Change the stretch gradient and compensation; inspect the existing closed prism mesh. **Evidence class:** Prescribed kinematics. **Scope:** Algebraic local-volume claims do not prove mesh integration or floating-point refinement. [Open the shared Kenoma GUI](examples.html?chapter=09aa-nonuniform-volume). # Connect fibre architecture to force without inventing strength {#architecture-to-force} ## Worked reading ### 1. Calculate one reference-cut force Use authored reference area 80 mm² and nominal stress 300 kPa. Their product is 24 N along the fibres. At zero pennation all of that force acts along the tendon direction. **Observe:** Reference and current-cut forces both read 24 N. This is analytic bookkeeping with prescribed stress, not measured muscle strength. ### 2. Change area and stress together Shorten to stretch 0.8 while imposing J=1. Current fibre-normal area becomes 80/0.8 = 100 mm² and Cauchy stress becomes 300 × 0.8 = 240 kPa. **Observe:** 100 mm² × 240 kPa still gives 24 N. Shortening alone does not change the prescribed nominal force in this example. ### 3. Project the force once Keep the same material cut and turn the fibres to 30 degrees. Tendon-directed force is the fibre force times cos(30 degrees). **Observe:** Axial and current-cut forces stay 24 N; tendon-directed force becomes about 20.7846 N. Seven drawn lines encode orientation, not a fibre count. ### 4. Check a familiar angle At 60 degrees the projection factor is one half. Projecting both an already projected area and the force again would apply the angle twice. **Observe:** Tendon-directed force is 12 N while axial force remains 24 N. The orange cut slab is a diagram; the reported area is analytic. The unresolved anatomical requirement is a source-bound map from fibre architecture and measured force to the active continuum coefficient. Kenoma currently fits model-reference actuator forces while its calibration states retain unresolved stationarity and compression. That fit must not be renamed physiological specific tension. After the prescribed local-volume map and before material response, this lesson supplies the bookkeeping prerequisite: distinguish fibre number from fibre area, parallel groups from sections in series, nominal from Cauchy stress, and projected from unprojected PCSA. It does not repair the continuum solve or supply a new anatomical dataset. All lab numbers are authored examples, not calibration inputs. ## Retain the failed calibration evidence At [PR11 commit 0bed56a](https://github.com/MrScripty/Kenoma/blob/0bed56a86e771b2187e1590e760357f31ec3ef37/education/book/chapters/15-anatomical-apparatus.md), the fixed-end fits use approximately 3.60, 8.71, and 20.38 MPa for brachialis, short biceps, and long biceps. The source documents corner volume ratios near 0.56–0.62 and free nodal force components of 64.07, 52.06, and 54.22 N at those frozen calibration states. A successful reduced force match is therefore not an equilibrated full-nodal material calibration. This book integration adds six scoped Real claim registrations and a portable analytic lab. No fit, material coefficient, calibration state, accepted trajectory, reference asset, or failure threshold is changed. Resolving local compression and full displacement/pressure stationarity remains an upstream gate. The analytic examples below cannot overrule it. ## Decide which area a measurement describes For a declared parallel reference bundle with volume V₀ in m³, representative fibre length Lf₀ in m, and contractile volume fraction φ₀, the idealization Acontractile₀ = φ₀ V₀ / Lf₀ gives area in m². It requires a meaningful representative length and fraction. A tapered whole belly, distributed fibre terminations, varying orientations, or nonuniform packing need a spatial integration and load-path model; inserting their total volume into this formula does not establish those conditions. PCSA definitions must travel with the values. [Murray, Buchanan and Delp (2000), Methods and Table 2](https://research.me.udel.edu/buchanan/PDF_Files/Murray,%20Buchanan,%20Delp,%20JB%202000.pdf) computes PCSA from volume divided by optimal fascicle length, then uses the pennation cosine separately in moment capacity. Its elbow architecture study used ten upper extremities from nine cadavers, with exclusions and different sample counts by muscle. In contrast, [Ward and Lieber (2005), equation 1](https://muscle2.ucsd.edu/pubs/pdf/Ward_JB_2005a.pdf) includes the cosine in PCSA. A projection included in an imported area must not be multiplied again. Use three explicit metadata fields before combining a force and area: - area convention: fibre-normal or already tendon-projected - stress basis: contractile area or an effective whole-muscle area - configuration: reference/optimal or current, with the stated stretch and volume ratio An effective whole-muscle specific tension may already include noncontractile fractions through its area definition. Multiplying it by φ₀ again double-counts that reduction. Conversely, a single-fibre measurement does not automatically define a whole-muscle effective stress. A smallest fibre diameter is not a measured circular cross-sectional area, and a fibre count fraction is not an area fraction. **Checked claim architecture-projection-once:** Projecting force once equals multiplying stress by an already projected area **Assumptions:** Area, nominal stress and cosine are real scalars. The same cosine is used once, either on force or on area; physical use separately requires a cosine in [0,1] and an explicitly declared PCSA/stress convention. ```lean theorem projection_once (area nominal cosine : ℝ) : (nominal * area) * cosine = nominal * (area * cosine) ``` **Limits:** A paper's PCSA definition, actual pennation, tendon routing or cancellation of transverse force. Declaration: `KenomaArchitectureForce.projection_once`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 36f96515d885c06b824c3b6aa3fb8e915175fe4c3dbb441f0a143448399f746c. [Full checked source](proofs/ArchitectureForce.lean); [receipt](architecture-force-real-proof-status.json). ## Sum parallel fibre groups by area For group k with Nk fibres, reference fibre area ak₀, nominal axial stress Pk, and current tendon-direction cosine ck, use A₀ = Σk Nk ak₀ T = Σk Pk Nk ak₀ Ttendon = Σk Pk Nk ak₀ ck This is a declared independent parallel-force decomposition. It omits passive matrix force, pressure traction, lateral exchange between groups, and curved aponeurosis geometry. It cannot infer recruitment or force–velocity properties from fibre typing alone. Two synthetic groups with equal counts of 50,000 and areas of 1,000 and 2,000 µm² have area shares 1/3 and 2/3. At nominal stresses of 100 and 300 kPa, total area is 150 mm² and force is 35 N. The count-average stress gives 30 N and is the wrong weighting for this example. Different angles likewise require force-weighted projections, not an unqualified average angle. [Mattiello-Sverzut and Martins (2023)](https://pmc.ncbi.nlm.nih.gov/articles/PMC9925190/) assessed isokinetic elbow performance in 32 volunteers; usable biceps morphology samples came from 26 participants (9, 8, and 9 across the three age groups). Fibre subtypes and smaller diameters describe that morphology subset, not all 32 participants. The study supports keeping type and size distinct; it does not provide a subject-matched spatial packing map for the atlas. [Bottinelli et al. (1996)](https://physoc.onlinelibrary.wiley.com/doi/10.1113/jphysiol.1996.sp021617) reports type- and temperature-dependent single skinned-fibre mechanics. Its 12 °C load-clamp protocol is not a body-temperature whole-biceps calibration. Neither paper's parameters are imported here. **Checked claim architecture-parallel-area-aggregation:** Total area times area-weighted nominal stress equals the two-group force sum **Assumptions:** All parameters are real and n1\*area1 + n2\*area2 > 0. The two-group force and area-weighted stress are exactly the displayed definitions. Nonnegative fibre counts, areas and stresses are separate physical-use conditions. ```lean theorem parallel_area_aggregation (n1 area1 stress1 n2 area2 stress2 : ℝ) (hArea : 0 < n1 * area1 + n2 * area2) : (n1 * area1 + n2 * area2) * areaWeightedStress n1 area1 stress1 n2 area2 stress2 = parallelForce n1 area1 stress1 n2 area2 stress2 ``` **Limits:** Measured fibre counts/areas, biological recruitment, lateral load sharing or the arbitrary-length JavaScript sum. Declaration: `KenomaArchitectureForce.parallel_area_aggregation`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 36f96515d885c06b824c3b6aa3fb8e915175fe4c3dbb441f0a143448399f746c. [Full checked source](proofs/ArchitectureForce.lean); [receipt](architecture-force-real-proof-status.json). **Checked claim architecture-two-group-projected-sum:** Two separate area/stress/cosine products equal the sum of separately projected group forces **Assumptions:** Counts, reference areas, nominal stresses and cosines are real scalars. The same two declared independent group terms occur on both sides; physical use separately requires meaningful nonnegative groups and cosines in [0,1]. ```lean theorem two_group_projected_sum (n1 area1 stress1 cosine1 n2 area2 stress2 cosine2 : ℝ) : (n1 * area1) * (stress1 * cosine1) + (n2 * area2) * (stress2 * cosine2) = (n1 * area1 * stress1) * cosine1 + (n2 * area2 * stress2) * cosine2 ``` **Limits:** A three-dimensional aponeurosis solution or a calibrated fibre orientation distribution. Declaration: `KenomaArchitectureForce.two_group_projected_sum`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 36f96515d885c06b824c3b6aa3fb8e915175fe4c3dbb441f0a143448399f746c. [Full checked source](proofs/ArchitectureForce.lean); [receipt](architecture-force-real-proof-status.json). ## Track the same material cut during shortening Let F be a locally homogeneous orientation-preserving deformation gradient, J = det F > 0, f₀ a reference unit fibre, λ = |F f₀| > 0, and f = F f₀ / λ. For a reference cut normal to f₀ with area A₀, the current oriented area vector is a = J F⁻ᵀ f₀ A₀. Its projection normal to the current fibre is A⊥ = a · f = J A₀ / λ. A⊥ is a projected material-cut area. In a shear-free straight bundle it is the familiar orthogonal cross-sectional area. With shear, the actual deformed cut may be oblique and have a different surface area. The formula is not a global statement about an anatomical imaging plane or a curved heterogeneous belly. Spatially varying F requires local integration. The existing active law in [anatomical-material.mjs](https://github.com/MrScripty/Kenoma/blob/0bed56a86e771b2187e1590e760357f31ec3ef37/education/web/anatomical-material.mjs) differentiates a full-stretch potential. With p = aactivation σ₀ fL(λ), its active first Piola tensor is p f ⊗ f₀, and its active Cauchy tensor is (p λ/J) f ⊗ f. Thus σfibre = p λ / J Tactive = σfibre A⊥ = p A₀. Both p and σfibre have units Pa, but they divide force by different areas. The lab calls the scalar p “nominal stress P” and keeps it fixed initially. With A₀ = 80 mm², p = 300 kPa, J = 1 and λ = 0.8, A⊥ grows to 100 mm² and σfibre falls to 240 kPa. Axial force stays 24 N. At 30° pennation the projected component is about 20.78 N. There is no fibre-count increase and no extra bulge multiplier. | Quantity | Default value | |:--|--:| | Reference contractile area | 80.00 mm² | | Current projected area | 100.00 mm² | | Nominal stress P | 300.00 kPa | | Cauchy fibre stress σ | 240.00 kPa | | Axial force | 24.00 N | | Tendon-directed component | 20.78 N | Authored default: geometric reference area 100 mm², contractile fraction 0.80, fibre stretch 0.80, volume ratio 1.00 and pennation 30°. The force–length multiplier is held at 1. The tendon-directed component is rounded to two decimals. [Open the interactive architecture-force lab](architecture-force/index.html). [Primary-source ledger](architecture-force/sources.json) · [Preserved contribution source](contributions/architecture-force/README.md) · [Book source binding](architecture-force/registration.json). **Try and predict.** With force–length held at 1, lower the stretch while holding J and the reference bundle fixed. Predict the new projected area and Cauchy stress before checking the unchanged axial force. Reset, change only pennation, then compare the axial force with its tendon-directed component. Finally enable the authored force–length curve: explain which assumption changed. Changing packing compares different reference bundles, not acute fibre creation. Holding Cauchy stress fixed instead would produce a different force as area changes. That is a different constitutive prescription, not a universal strength bonus. Enabling the existing authored fL curve in the lab explicitly changes p and therefore force. In the anatomical model, activation, length, passive stresses, pressure and attachments jointly matter; this calculation is only its active material-cut identity. [Raiteri, Cresswell and Lichtwark (2016)](https://pmc.ncbi.nlm.nih.gov/articles/PMC4974924/) examined human tibialis anterior with three-dimensional ultrasound and found spatial shape and architectural changes during isometric contraction. It motivates regional rather than uniform geometry. It is neither biceps anatomy nor proof of exact local J = 1. The volume controls here are prescribed and have no biological acceptance range. **Checked claim architecture-material-cut-force:** Declared Cauchy fibre stress times declared current projected cut area equals nominal stress times reference area **Assumptions:** All parameters are real. J > 0 and fibre stretch > 0. Current projected area is defined as A0\*J/stretch and Cauchy fibre stress as nominal\*stretch/J. Positivity of A0 and nonnegative nominal stress are additional physical-use conditions, not hypotheses needed by this identity. ```lean theorem material_cut_force (A0 nominal J stretch : ℝ) (hJ : 0 < J) (hstretch : 0 < stretch) : cauchyFiberStress nominal J stretch * currentProjectedArea A0 J stretch = nominal * A0 ``` **Limits:** The geometry or Nanson premises, a heterogeneous area integral, JavaScript arithmetic, equilibrium or physiology. Declaration: `KenomaArchitectureForce.material_cut_force`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 36f96515d885c06b824c3b6aa3fb8e915175fe4c3dbb441f0a143448399f746c. [Full checked source](proofs/ArchitectureForce.lean); [receipt](architecture-force-real-proof-status.json). ## Follow a variable cross section through a series load path Under a one-dimensional static section resultant convention, a cell between cuts i and i+1 obeys Ti+1 − Ti + Qi = 0, where Qi is net axial force from lateral or external loading on that cell. With no lateral load or inertia, axial force is the same at every cut. A 100–200–100 mm² reference-area sequence carrying 30 N therefore has nominal section stresses of 300–150–300 kPa. A thicker middle section does not manufacture an additional end force. If one assigns 300 kPa independently to each cut, the resulting 30–60–30 N sequence needs −30 N and +30 N lateral forces in the two intervening cells. Such exchange could belong to a resolved ECM/matrix path, but it must be represented and balanced. It cannot be inferred from the taper alone. The scalar sequence is a necessary force-balance example, not a compatible displacement field, three-dimensional equilibrium, shear-stress solution, or material fit. **Checked claim architecture-series-balance-telescopes:** Summing two declared cell balances cancels the shared internal section force **Assumptions:** Left, middle and right section forces and q1, q2 are real scalars. The adjacent cell expressions use one shared middle force with opposite signs. Zero cell balance and static equilibrium are additional premises, not conclusions. ```lean theorem series_balance_telescopes (left middle right q1 q2 : ℝ) : (middle - left + q1) + (right - middle + q2) = right - left + q1 + q2 ``` **Limits:** Equilibrium premises, compatible displacement, ECM stiffness or force generation. Declaration: `KenomaArchitectureForce.series_balance_telescopes`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 36f96515d885c06b824c3b6aa3fb8e915175fe4c3dbb441f0a143448399f746c. [Full checked source](proofs/ArchitectureForce.lean); [receipt](architecture-force-real-proof-status.json). Internal paired forces cancel in the whole-body resultant. Their power does not generally vanish: q v₁ + (−q) v₂ = q(v₁−v₂). An ECM coupling can store or dissipate energy when adjacent points move differently. A no-slip tie, compliant bond, frictional slip and damage law are distinct constitutive choices; none is supplied by the arithmetic identity. [Huijing and Baan (2003)](https://pubmed.ncbi.nlm.nih.gov/12571138/) found differing proximal/distal tendon forces in maximally active rat extensor muscles with connective tissues retained and controlled relative length changes. This is evidence for additional force paths, not a human-biceps coupling coefficient. [Zhang and Gao (2012)](https://pubmed.ncbi.nlm.nih.gov/22682257/) used a two-dimensional fibre/endomysium model to study shear transfer and tapered fibre ends. Its model supports the need to declare interface mechanics; it does not calibrate Kenoma's matrix. **Checked claim architecture-paired-exchange-power:** Paired internal force power equals force times relative velocity **Assumptions:** q, v1 and v2 are real scalars. The paired force on the second point is defined to be -q. Equal velocities, constitutive force laws and any dissipation inequality are not assumed or established. ```lean theorem paired_exchange_power (q v1 v2 : ℝ) : q * v1 + (-q) * v2 = q * (v1 - v2) ``` **Limits:** The force law, energy storage, dissipation sign, no-slip constraint or biological bonding. Declaration: `KenomaArchitectureForce.paired_exchange_power`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 36f96515d885c06b824c3b6aa3fb8e915175fe4c3dbb441f0a143448399f746c. [Full checked source](proofs/ArchitectureForce.lean); [receipt](architecture-force-real-proof-status.json). ## Density and fluid mechanics remain separate inputs Mass density maps volume to mass, not area directly to force. Ward and Lieber's fixation/hydration experiment reported preparation-dependent human muscle density and warned of PCSA errors from mismatched assumptions. Their fixed-tissue results are not live biceps density measurements. A later mass-based estimate must retain species, tissue preparation, hydration and the density uncertainty rather than silently treating 1,060 kg/m³ as universal. [Sleboda and Roberts (2020)](https://pmc.ncbi.nlm.nih.gov/articles/PMC6983394/) applied a pressure cuff during isolated bullfrog semimembranosus contractions. The effect on measured force changed with muscle length, and physical ECM analogues helped interpret the result. The experiment does not identify a human biceps pressure law or a unique mechanism. It does show why fluid–matrix interactions cannot be represented by “more blood equals more strength.” Intracellular/interstitial fluid, blood inside vessels, solid-matrix stress, incompressibility pressure and measured intramuscular pressure are different quantities. The original [cat fast/slow muscle pressure and perfusion study](https://pubmed.ncbi.nlm.nih.gov/6542507/) varied perfusion conditions and examined isometric endurance. Its experimental scope requires vascular boundary conditions and timescale-dependent physiology; a bulk penalty contains neither. No numerical perfusion, permeability, ECM bonding, blood-volume or edema parameter is imported in this lesson. Exercise pump and chronic growth are not acute material-area transformations. For a future coupled fluid model, record the conserved constituents, fluid pressure definitions, permeability and boundary conditions, vascular compartments, compressibility assumptions, and the drain/undrain time scale. Validation must distinguish local from global volume, and conservation from accurate geometry. A shared external skin/fat envelope must enclose the assembled tissues and obey its own interface/contact conditions; seven separately expanding bellies do not define it. ## Verification and next acceptance gate {#architecture-force-evidence} The preserved contribution has twelve Node contracts for scalar units and transformations, explicit PCSA/packing conventions, heterogeneous sums, taper equilibrium and lateral force balance. Its repository-contract tests compare the active-stress map with the unchanged material operator, including shear and rigid rotation. Seven SymPy identities separately check declared algebra, including cofactor projection and exchange power. Symbolic simplification and unit tests are not Lean kernel proofs. The six original claim IDs and theorem names are registered in this book candidate. `ArchitectureForce.lean` is copied byte-for-byte from the independently qualified contribution. The cards state explicit assumptions and retain the original exclusions; the fresh book checker must compile every registered family before issuing book proof receipts. The historical nonuniform-volume integration was 103 + 6 = 109 declarations. Adding these six architecture-force contracts gives a 115-declaration source inventory across fourteen files: 30 integer and 85 Real declarations. Source registration alone does not establish a freshly checked 115-declaration book, a rendered PDF or hosted release. The bounded standalone contribution checks in [run 37743673184](https://github.com/MrScripty/Kenoma/actions/runs/37743673184), at exact commit `143ac8863cd8a5be736e2c455cac9605c2e20a1f`, compiled all six contracts and passed real Chromium controls at 1280×1000 desktop and 393×852 mobile sizes, including the no-JavaScript fallback. The recorded agent visual review passed all five JPEG quality-85 captures. That evidence applies to the standalone source; it does not qualify this integrated book. Its original automated `pending human inspection` marker remains historical evidence, unchanged. The portable lab adds default values for print and no-JavaScript reading while preserving the model and control code. [Original contribution sources](contributions/architecture-force/README.md), [primary-source ledger](architecture-force/sources.json) and [book assembly binding](architecture-force/registration.json) keep source, test and evidence scopes distinct. Statements in the preserved standalone documents about pending registration describe that earlier stage. Integrated desktop/mobile controls, PDF readability, complete proof closure, owner release review and any publication remain separate gates. The full book build also launches numerical experiments; it is not a render-only check. The next anatomical implementation gate is still an equilibrated, locally admissible calibration specimen with an adequate displacement/pressure space. Only after that gate should a source-bound architecture dataset be mapped into σ₀ or a replacement law. Every proposed parameter should carry the source, specimen/protocol, area/stress convention, units, uncertainty, transformation and destination equation. Independent attachment, tendon, cartilage, fat and shared-skin validation remain necessary for the full anatomical arm goal. ### Interactive 3D: Fibres, cuts and projected force Change pennation and material stretch; compare reference and current cut forces. **Evidence class:** Analytic bookkeeping. **Scope:** Authored areas/stresses; one projection only; no contraction or calibrated muscle prediction. [Open the shared Kenoma GUI](examples.html?chapter=09ab-architecture-force). # Let material stiffness and boundaries choose the lateral shape {#compression-bulk-shear-confinement} ## Worked reading ### 1. Compare unloaded boundary conditions Start at unit height with shear modulus 1500 Pa and bulk modulus 50000 Pa. Neither free sides nor unilateral walls need a reaction in the reference state. **Observe:** Both J values and lateral stretch are 1; plate forces and wall reaction are zero. ### 2. Impose the same height reduction Shorten height to 0.8. The free specimen solves zero lateral traction and expands sideways; the confined specimen is prevented from widening. **Observe:** Free lateral stretch is about 1.11463 and J is 0.993914, compared with confined J=0.8. Plate forces are about 4.53637 N and 42.0887 N, respectively. ### 3. Change bulk stiffness without changing height Increase bulk modulus fivefold while keeping the same geometry, shear modulus and boundary conditions. The free specimen can preserve more volume by expanding; the walls prevent that route. **Observe:** Free J rises to about 0.998781 and plate force to 4.56728 N. Confined J stays 0.8 while its force rises to 202.089 N; stiffness does not override the prescribed walls. ### 4. Read the residual before trusting a shape Return to bulk modulus 50000 Pa but stop bisection after eight iterations. The specimen still has positive volume and looks plausible, yet its free-side traction is not balanced. **Observe:** Free lateral residual is about 24.0254 Pa, above the unchanged 0.00001 Pa criterion, so Free converged is false. Increase the cap manually to 64 to recover the second step. **Question:** when a block is shortened between plates, must its volume stay exactly fixed? The preceding [isochoric lesson](#measure-deformation-before-choosing-a-muscle-law) imposed that answer. Here a material law and lateral boundary conditions choose the shape. Compare both conditions at one prescribed height, then change one stiffness at a time. This is an authored, homogeneous elastic specimen, not measured muscle. The reference width, height and depth are $W_0=0.08$ m, $H_0=0.06$ m and $D_0=0.05$ m; $V_0=0.00024$ m³. Ideal frictionless plates prescribe height stretch $0.5\le h\le1$. The single unknown lateral stretch $b>0$ acts equally in X and Z: $$F=\operatorname{diag}(b,h,b),\qquad J=b^2h,\qquad I_1=2b^2+h^2.$$ This diagonal homogeneous ansatz rules out bulging, shear localization, buckling and spatially varying fields. Uniform stress makes the lateral traction condition meaningful within this ansatz; this is not a mesh solve or a proof of the unrestricted specimen's preferred deformation. ## An elastic energy, finite stiffness and units Reuse the existing [homogeneous tissue energy](web/tissue.mjs), leaving the earlier labs' equations and calibration unchanged: $$U(b,h)=V_0\left[\frac{\mu}{2}(J^{-2/3}I_1-3)+\frac{K}{2}(J-1)^2\right].$$ Here $\mu$ and $K$ are shear and bulk **parameters of this declared energy**, each in Pa = J/m³. They characterize the reference response; finite-deformation tangent stiffness need not equal these constants. Controls permit $500\le\mu\le5000$ Pa and $0\le K\le250000$ Pa. These are bounded teaching choices, not fitted biological ranges. The $K=0$ endpoint deliberately removes resistance to pure volume change. A finite bulk term penalizes $J\ne1$ with finite energy; it does not impose $J=1$. The shear term penalizes distortional shape change and vanishes under positive isotropic scaling. Neither term supplies plasticity, damage, viscosity, fluid transport, fibre architecture or activation. The constitutive framework has an original-author reference: [A. F. Bower, *Applied Mechanics of Solids*, §3.5](https://solidmechanics.org/Text/Chapter3_5/Chapter3_5.php) describes hyperelastic stress as an energy derivative and distinguishes nominal stress from force per deformed area. The formula and boundary reduction here are the book's illustrative model. No experimental response curve is reproduced or calibrated from that source. | Quantity | Units | Meaning | |:--|:--|:--| | $h,b,J$ | dimensionless | Height stretch, lateral stretch, volume ratio | | $U$ | J | Stored elastic energy for the whole reference block | | $P_x,P_y,R$ | Pa | Nominal stresses and inward wall reaction per reference side area | | $N$ | N | Compressive force on one height plate | | $p$ | Pa | Plate force divided by its current area | | $g_x,g_z$ | m | Clearance between specimen and each lateral wall | ## Derive the reduced equilibrium The nominal stress components computed from this energy are $$P_x=\mu J^{-2/3}\left(b-\frac{I_1}{3b}\right)+K(J-1)\frac{J}{b},\qquad P_y=\mu J^{-2/3}\left(h-\frac{I_1}{3h}\right)+K(J-1)\frac{J}{h}.$$ Both lateral directions vary with $b$, hence $\partial U/\partial b=2V_0P_x$; $\partial U/\partial h=V_0P_y$. Finite-difference tests check these derivatives and the reduced plate force. **Free sides** require zero lateral traction, $P_x=0$. The numerical root bracket is $h\le b\le1/\sqrt h$: the left endpoint has zero shear contribution and nonpositive bulk contribution; the right has $J=1$ and nonnegative shear contribution. Analytic endpoints handle $K=0$ and $h=1$. This bracket supports the implemented root search; no Lean proof of existence, uniqueness, convergence or global optimality is claimed. **Unilateral confinement** places smooth rigid walls at the reference X/Z faces. Walls prevent outward expansion but allow inward pull-away: $b\le1$. They apply inward compressive reaction $R\ge0$ and cannot pull the block outward. The reduced wall contract is $$P_x+R=0,\qquad b\le1,\qquad R\ge0,\qquad R(1-b)=0.$$ At $b=1$, if $P_x<0$, use $b=1$ and $R=-P_x$. Otherwise solve the free-traction root on the restricted bracket $[h,1]$ and use $R=0$. The separate bracket keeps even a finite approximation inside the walls. At weak bulk stiffness, the specimen can shrink away from the walls; forcing $b=1$ in that case would require an unmodeled tensile attachment. Plate force and pressure follow from the same nominal stress, not from displayed arrows: $$N=-W_0D_0P_y,\qquad p=\frac{N}{W_0D_0b^2}.$$ The sign convention makes compression positive. Each X wall carries $N_x=RH_0D_0$; each Z wall carries $N_z=RW_0H_0$. Their current-area pressure is $R/(bh)$. Per-wall clearances are $g_x=W_0(1-b)/2$ and $g_z=D_0(1-b)/2$. The reported complementarity work is $2(N_xg_x+N_zg_z)$ in joules, accounting for both walls in each direction. ### Property lab 4 · Compression, bulk stiffness and confinement ![Solved homogeneous 80 × 60 × 50 mm reference block at height stretch 0.8, shear parameter 1,500 Pa and bulk parameter 50,000 Pa. Free: J = 0.993914, plate force 4.53637 N. Rigid unilateral walls: J = 0.8, plate force 42.0887 N. Dashed outlines are reference; gold lines are frictionless plates. Front view at one fixed physical scale; depth also scales by lateral stretch b.](assets/property-material.svg) Solved homogeneous 80 × 60 × 50 mm reference block at height stretch 0.8, shear parameter 1,500 Pa and bulk parameter 50,000 Pa. Free: J = 0.993914, plate force 4.53637 N. Rigid unilateral walls: J = 0.8, plate force 42.0887 N. Dashed outlines are reference; gold lines are frictionless plates. Front view at one fixed physical scale; depth also scales by lateral stretch b. [Open the interactive lesson](index.html#lab-property-material). ## Predict, change one input, and inspect the residual At default $h=0.8$, $\mu=1500$ Pa and $K=50000$ Pa, the plate spacing is 0.048 m in both panels. These values come from a fresh reduced solve: | Boundary condition | Lateral stretch $b$ | Volume ratio $J$ | Plate force (N) | Stored energy (J) | |:--|--:|--:|--:|--:| | Free lateral surfaces | 1.11462688 | 0.99391447 | 4.53637103 | 0.02497727 | | Unilateral rigid walls | 1 | 0.8 | 42.08871498 | 0.25142075 | **Try and predict.** Raise only $K$ to 250000 Pa. The free block approaches $J=1$ without imposing it: $J\approx0.99878057$, while its plate force is about 4.56728 N. Active rigid walls retain $b=1$ and $J=h=0.8$, so the plate force rises to about 202.08871 N. Confinement changes the work required to reach the same height; increasing finite bulk stiffness cannot restore volume while all three stretches are fixed. Restore $K=50000$ Pa and raise only $\mu$ to 5000 Pa. Read the force, lateral expansion, and separate bulk/shear energy contributions. Height remains shared. Every comparison changes only the named input; no time or activation state is hidden in this static lesson. **Counterexample.** Set $K=0$. The solved block has $b=h$, $J=h^3$ and zero stored energy/plate force up to roundoff: at $h=0.8$, $J=0.512$. Isotropic collapse costs no distortional energy in this deliberately degenerate law. It is not a plausible soft-muscle response or plastic failure. At $K=500$ Pa, both solutions shrink laterally to $b\approx0.90043115$, with zero wall reaction and positive clearance. Confinement does not manufacture tensile attachment. **Feasibility check.** The “Test isochoric wall candidate” button tries $b=1/\sqrt h$ in the confined geometry. For $h<1$ it has positive $J=1$ but penetrates the lateral walls and is rejected without changing the solved state. Positive volume is necessary but does not establish boundary feasibility. **Numerical check.** Select eight bisections. Geometry remains positive and wall-feasible, but the signed free residual generally fails the displayed criterion $|P_x+R|\le10^{-5}$ Pa. Restore 32 or 64 and compare the bracket width and residual. The criterion belongs to this new lesson; it changes none of the existing labs' acceptance limits. “Residual criterion met” refers only to this reduced lateral equation. Invalid, blank, nonfinite or out-of-domain inputs retain the prior displayed state. Finally restore $h=1$: $b=1$, $J=1$, energy and force return to zero. This model has no history or irreversible state, so it cannot demonstrate plastic deformation or dissipative load/hold/release. Reset deliberately restores all authored defaults. ## Real properties: checked algebra and unfinished formal obligations The specimen uses **real** stretches, stresses and energies. Five real-domain algebra claims below are compiled against the pinned mathlib dependencies before this book is built. Constitutive derivatives and equilibrium existence, uniqueness and optimality remain **unfinished**. The separate integer contracts do not substitute for these real claims or their remaining obligations. | Real claim and assumptions | Derivation in this lesson | Real formal status | |:--|:--|:--| | $b=1$, $00$, $K\geq0$ imply $V_0K(J-1)^2/2\geq0$; for $K>0$ it vanishes exactly at $J=1$ | A real square is nonnegative; a product with positive factors vanishes only when the square does | Checked real bulk algebra | | $g>0$ and $Rg=0$ imply $R=0$ | Divide the assumed complementarity equation by nonzero real $g$ | Checked real implication; complementarity is assumed, not certified | | $dU/db=2V_0P_x$, $dU/dh=V_0P_y$ for positive stretches | Differentiate the stated energy with $dJ/db=2bh$ and $dJ/dh=b^2$ | Unfinished; real powers and derivatives need formal support | | Lateral virtual work factors as $2V_0(P_x+R)\delta b$ | Add the two equal lateral stress and wall contributions | Checked real factorization; does not establish equilibrium | **Checked claim material-real-confined-volume:** Real b=1 and 0=0, K>=0 imply VK(J-1)\^2/2>=0 **Assumptions:** Real reference volume V>=0 and bulk coefficient K>=0; any real J. ```lean theorem finite_bulk_energy_nonnegative (V K J : ℝ) (hV : 0 ≤ V) (hK : 0 ≤ K) : 0 ≤ bulkEnergy V K J ``` **Limits:** Only the bulk term is covered; fractional-power shear and derivatives remain unfinished. Declaration: `Kenoma.MaterialReal.finite_bulk_energy_nonnegative`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 2e30769e073b719b66cfcb38c527d7319034fcf55f2723771a54405337e53258. [Full checked source](proofs/MaterialResponseReal.lean); [receipt](material-real-proof-status.json). **Checked claim material-real-bulk-zero:** Real V>0, K>0 imply bulk energy zero iff J=1 **Assumptions:** Real V>0 and K>0; any real J. ```lean theorem positive_bulk_zero_energy (V K J : ℝ) (hV : 0 < V) (hK : 0 < K) : bulkEnergy V K J = 0 ↔ J = 1 ``` **Limits:** Does not assert loaded equilibrium has J=1, or establish incompressibility. Declaration: `Kenoma.MaterialReal.positive_bulk_zero_energy`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 2e30769e073b719b66cfcb38c527d7319034fcf55f2723771a54405337e53258. [Full checked source](proofs/MaterialResponseReal.lean); [receipt](material-real-proof-status.json). **Checked claim material-real-separated-wall:** Real positive gap and assumed Rg=0 imply R=0 **Assumptions:** Real reaction R and gap g>0 with assumed complementarity R\*g=0. ```lean theorem separated_wall_zero_reaction (reaction gap : ℝ) (hg : 0 < gap) (hc : reaction * gap = 0) : reaction = 0 ``` **Limits:** Complementarity is assumed, not certified for the numerical wall solve or collisions. Declaration: `Kenoma.MaterialReal.separated_wall_zero_reaction`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 2e30769e073b719b66cfcb38c527d7319034fcf55f2723771a54405337e53258. [Full checked source](proofs/MaterialResponseReal.lean); [receipt](material-real-proof-status.json). **Checked claim material-real-lateral-work:** Real lateral stress and wall work factor as 2V(Px+R)delta **Assumptions:** Real reference volume, nominal stress, wall reaction and lateral variation; stress/energy derivative association supplied separately. ```lean theorem lateral_virtual_work (V stress reaction delta : ℝ) : 2 * V * stress * delta + 2 * V * reaction * delta = 2 * V * (stress + reaction) * delta ``` **Limits:** No derivative, root existence, uniqueness or stationarity certificate. Declaration: `Kenoma.MaterialReal.lateral_virtual_work`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 2e30769e073b719b66cfcb38c527d7319034fcf55f2723771a54405337e53258. [Full checked source](proofs/MaterialResponseReal.lean); [receipt](material-real-proof-status.json). The earlier real determinant and square-root identities support the kinematic volume formula. They do not prove this constitutive law, wall solution, equilibrium existence/uniqueness or global optimality. A release build must compile any future real-domain claim with its supported pinned dependencies before presenting it as checked. ## Discrete arithmetic contracts and separate numerical evidence The five declarations below are freshly compiled with pinned Lean 4.19.0 and bundled Std. They concern **exact scaled integers**, with positive external SI scaling factors. These are separate implementation arithmetic checks; real stretches, stresses and energies are not their quantified domain. The unfinished derivative and equilibrium obligations above remain separate. **Checked claim material-confined-volume:** With both lateral stretch numerators fixed at their reference scale, a smaller height numerator gives a smaller volume numerator. **Assumptions:** Exact integers s and h; s > 0 and h < s. Physical interpretation additionally takes h > 0 and stretches b=s/s=1, height=h/s. Volume numerator is b_numer² × h_numer over s³. ```lean theorem confined_volume (s h : Int) (hs : 0 < s) (hh : h < s) : volumeNumerator s h < volumeNumerator s s ``` **Limits:** No real determinant, constitutive equilibrium, finite-element volume or floating-point result is proved. Declaration: `Kenoma.Material.confined_volume`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: propext; source SHA-256: 8ce7f4b5bf4b68f9eeb0d85b06925f417995f945b64498a4533347ead1864092. [Full checked source](proofs/MaterialResponse.lean); [receipt](material-proof-status.json). **Checked claim material-bulk-sign:** The exact scaled bulk-penalty numerator k × delta² is nonnegative for k ≥ 0. **Assumptions:** Integer k and delta; delta represents a scaled volume-ratio departure, and unit/denominator scale factors are positive. ```lean theorem finite_bulk_penalty_nonnegative (k delta : Int) (hk : 0 ≤ k) : 0 ≤ bulkPenaltyNumerator k delta ``` **Limits:** The full real energy, fractional-power shear term and its derivatives are not formalized. A finite penalty is not a hard volume constraint. Declaration: `Kenoma.Material.finite_bulk_penalty_nonnegative`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: propext; source SHA-256: 8ce7f4b5bf4b68f9eeb0d85b06925f417995f945b64498a4533347ead1864092. [Full checked source](proofs/MaterialResponse.lean); [receipt](material-proof-status.json). **Checked claim material-bulk-zero:** For a strictly positive bulk coefficient, the exact bulk-penalty numerator is zero exactly when its volume-departure numerator is zero. **Assumptions:** Exact integer k > 0 and integer delta; positive external scaling factors. ```lean theorem positive_bulk_zero_penalty (k delta : Int) (hk : 0 < k) : bulkPenaltyNumerator k delta = 0 ↔ delta = 0 ``` **Limits:** Does not assert that a loaded equilibrium has zero penalty, or prove incompressibility, a real solver or biological validity. Declaration: `Kenoma.Material.positive_bulk_zero_penalty`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 8ce7f4b5bf4b68f9eeb0d85b06925f417995f945b64498a4533347ead1864092. [Full checked source](proofs/MaterialResponse.lean); [receipt](material-proof-status.json). **Checked claim material-separated-wall:** An assumed exact complementarity product with strictly positive wall gap forces zero wall reaction. **Assumptions:** Integer reaction and gap; gap > 0 and reaction × gap = 0. Physical reaction nonnegativity and positive SI scales are separate inputs. ```lean theorem separated_wall_zero_reaction (reaction gap : Int) (hg : 0 < gap) (hc : reaction * gap = 0) : reaction = 0 ``` **Limits:** Complementarity is assumed, not derived or certified for the JavaScript root. No continuous collision or spatial contact guarantee. Declaration: `Kenoma.Material.separated_wall_zero_reaction`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: propext, Quot.sound; source SHA-256: 8ce7f4b5bf4b68f9eeb0d85b06925f417995f945b64498a4533347ead1864092. [Full checked source](proofs/MaterialResponse.lean); [receipt](material-proof-status.json). **Checked claim material-lateral-work:** The two lateral stress and wall-reaction contributions factor as 2 × V₀ × (Pₓ + R) in exact scaled arithmetic. **Assumptions:** Integer volume, stress and reaction numerators with compatible positive external SI scales. The association with an energy derivative is assumed separately. ```lean theorem lateral_virtual_work (volume stress reaction : Int) : 2 * volume * stress + 2 * volume * reaction = 2 * volume * (stress + reaction) ``` **Limits:** Does not prove the real energy derivative, stationarity, root existence, uniqueness, global optimality or force validity. Declaration: `Kenoma.Material.lateral_virtual_work`. Lean 4.19.0; mathlib not used; bundled Std only; transitive axioms: propext; source SHA-256: 8ce7f4b5bf4b68f9eeb0d85b06925f417995f945b64498a4533347ead1864092. [Full checked source](proofs/MaterialResponse.lean); [receipt](material-proof-status.json). Numerical tests independently derive a stationarity equation in $J$, check energy derivatives and SI conversions, sweep the bounded controls, compare feasible energy samples, and exercise finite caps, wall onset, zero bulk and invalid candidates. Browser tests execute the generated controls, verify exported states and SVG dimensions at a common physical scale, and check rollback, reset, mobile/print and no-JavaScript alternatives. These tests establish behavior for this declared implementation, not global optimality, mesh accuracy, material calibration or biology. Continue with [anatomical evidence](#anatomy-is-evidence) before attaching these parameters to a named muscle. [Laboratory 5](#tendon-tissue-coupling) later reuses the free-side law in a coupled hinge example. The unfinished anatomical capstone, measured fibre-to-muscle aggregation, force–length/velocity lessons retain their separate limits in the [coverage chapter](#coverage-and-evidence). ### Interactive 3D: Free and confined compression Change height stretch and inspect free versus confined lateral response. **Evidence class:** Numerical demonstration. **Scope:** Existing homogeneous one-lateral-DOF equilibrium; not unrestricted 3D material stability. [Open the shared Kenoma GUI](examples.html?chapter=09b-material-response). # Load, hold, release: storage and viscous loss {#dissipative-load-hold-release} ## Worked reading ### 1. Load the specimen A one-second ramp raises the axial force to 0.6 N. Work splits into recoverable storage and viscous loss; both quantities come from the existing standard-linear-solid protocol. **Observe:** Extension is about 1.68159 mm. Work 0.000531635 J equals storage 0.000434748 J plus loss 0.0000968864 J up to roundoff. ### 2. Hold force and observe creep Keep force at 0.6 N during the hold. Extension keeps increasing, so the load continues doing work as the viscous branch evolves. **Observe:** Extension grows to about 2.32895 mm while force remains 0.6 N. Storage plus accumulated loss still matches the displayed external work. ### 3. Change what the fixture holds Replay from the same initial state and loading ramp, but hold extension after 1 s. With no further extension during the hold, no additional external work is done. **Observe:** Extension stays 1.68159 mm; force relaxes to about 0.402942 N. Work remains 0.000531635 J while storage decreases and loss increases. ### 4. Release and inspect finite recovery Return to the force-hold protocol and inspect its end after unloading from 3–4 s and recovery from 4–7 s. Zero applied force does not imply instantaneous recovery. **Observe:** Force is zero, but residual extension is about 0.189097 mm and storage about 0.00000773842 J. Loss is 0.000511623 J; the finite run does not claim complete recovery. The [axial bar lesson](#measure-deformation-before-choosing-a-muscle-law) made area and elastic strain visible. Keep its passive force balance, area profiles and equilibrium modulus, then add one internal strain that takes time to change. The learning objective is to distinguish **creep under held force** from **stress relaxation under held extension**, and account for recoverable storage, signed external work and viscous loss throughout unloading. The [bulk/shear compression lesson](#compression-bulk-shear-confinement) remains a separate finite-deformation model. This lesson follows the earlier small-strain axial bar: fixed material reference area $A(x)>0$, homogeneous axial coefficients, no body force, inertia, transverse equilibrium or active stress. Displacement and strain have tensile-positive signs. It uses a standard linear solid: an equilibrium spring in parallel with one Maxwell spring–dashpot branch. Roylance's [MIT teaching notes, §4.2](https://ocw.mit.edu/courses/3-11-mechanics-of-materials-fall-1999/d173f95347f59d59dd9b7387ab4303e7_MIT3_11F99_visco.pdf) present this arrangement and distinguish creep from relaxation. [COMSOL's constitutive theory](https://doc.comsol.com/6.3/doc/com.comsol.help.sme/sme_ug_theory.06.029.html) describes the same one-branch topology and viscosity/time-scale relation. These sources motivate the model; the coefficients below are authored demonstrations, not measurements of human tissue. ## One law for the image and the ledger Let $\epsilon$ be total axial strain and $v$ the viscous strain in the dashpot. The Maxwell spring strain is $\epsilon-v$. With fixed $E_0>0$, $E_1\ge0$ and $\eta>0$, $$\sigma=E_0\epsilon+E_1(\epsilon-v),\qquad \eta\dot v=E_1(\epsilon-v).$$ Here $E_0,E_1$ have units Pa and $\eta$ has units Pa s. This adds memory to the passive axial law. Setting $E_1=0$ recovers $\sigma=E_0\epsilon$ and the earlier bar's same midpoint strain, displacement and stored energy for identical geometry and load. The stored energy density and viscous loss rate density are $$\psi=\tfrac12E_0\epsilon^2+\tfrac12E_1(\epsilon-v)^2,\qquad d=\eta\dot v^2\ge0.$$ Differentiation and the Maxwell equation give the local balance $$\sigma\dot\epsilon=\dot\psi+d.$$ For the whole bar, $U=\int_0^L A\psi\,dx$, $\dot D=\int_0^L A d\,dx$ and external power is $N\dot\delta$. Work $W=\int N\dot\delta\,dt$ is signed; unloading can return energy to the apparatus. $D$ is cumulative lost mechanical energy and cannot decrease. Starting from rest gives $W=U+D$, with the observed finite-precision residual displayed separately. ## Constant force balance and an internal state With constant resultant $N$, $\sigma(x)=N/A(x)$. Uniform coefficients and an initially unstrained bar imply $\epsilon=c/A$ and $v=z/A$, where $c,z$ have units m². Define the geometric compliance factor $C_g=\int_0^L dx/A(x)$, with units 1/m. Then $$\delta=C_gc,\qquad N=(E_0+E_1)c-E_1z,$$ $$U=\tfrac12C_g\{E_0c^2+E_1(c-z)^2\},\qquad \dot D=C_g\eta\dot z^2.$$ Under imposed force, $$c=\frac{N+E_1z}{E_0+E_1},\qquad \dot z=\frac{E_1}{\eta(E_0+E_1)}(N-E_0z).$$ Holding force therefore permits increasing extension. Holding extension fixes $c$; then $\dot z=E_1(c-z)/\eta$ and force relaxes. For elapsed hold time $s$, $$z(s)=c+(z_0-c)e^{-E_1s/\eta}.$$ The relaxation time is $\eta/E_1$ and the force-controlled creep time is $\eta(E_0+E_1)/(E_0E_1)$ when $E_1>0$. With the default equal moduli, these are 1 s and 2 s. Increasing viscosity delays response; it does not imply a monotone change in energy lost during every finite protocol. The runtime integrates the scalar state exactly for each constant-extension interval and each linear force ramp. It separately integrates boundary work and squared viscous rate; loss is **not** filled in from the energy residual. Stable exponential differences avoid cancellation near $E_1=0$. Each step clips at protocol boundaries before changing the imposed condition. The bar uses explicit midpoint area quadrature. For a linear taper, the independent factor is $C_g=L\log(r)/(A_1(r-1))$ with limit $L/A_1$ at $r=1$; for two equal-length segments, $C_g=L(1+1/r)/(2A_1)$. The displayed refinement error compares midpoint extension to this exact profile integral. ## Run the same finite protocol Default reference: $L=0.2$ m, $A_1=0.0003$ m², area ratio $r=2$, $E_0=E_1=100{,}000$ Pa, $\eta=100{,}000$ Pa s and 32 midpoint cells. Load ramps from 0 to 0.6 N over 1 s, holds for 2 s, unloads from the actual reaction to zero over 1 s, then recovers at zero force for 3 s. Switching to extension hold captures the extension reached at the end of loading. The unloading ramp begins at the relaxed reaction. Both switches preserve extension and internal state continuously. ![Default force-controlled load, hold, unload and recovery. Axial displacement is magnified tenfold; reference scale stays fixed.](assets/property-dissipative.svg) ### Property lab 5 · Creep, relaxation and viscous loss Small-strain quasistatic axial standard linear solid: equilibrium spring in parallel with a Maxwell branch. Ramp, hold, unload and zero-force recovery expose history dependence. A force hold gives creep; a held extension gives force relaxation. Authored coefficients; no transverse equilibrium or muscle calibration. [Open the interactive protocol](index.html#lab-dissipative-bar). | Hold | Time (s) | Force (N) | Extension (mm) | Stored U (mJ) | Signed W (mJ) | Loss D (mJ) | |:--|--:|--:|--:|--:|--:|--:| | creep | 0.0 | 0.000000 | 0.000000 | 0.000000 | 0.000000 | 0.000000 | | creep | 1.0 | 0.600000 | 1.681586 | 0.434748 | 0.531635 | 0.096886 | | creep | 3.0 | 0.600000 | 2.371154 | 0.625806 | 0.945376 | 0.319569 | | creep | 4.0 | 0.000000 | 0.847472 | 0.155430 | 0.519361 | 0.363931 | | creep | 7.0 | 0.000000 | 0.189097 | 0.007738 | 0.519361 | 0.511623 | | relaxation | 0.0 | 0.000000 | 0.000000 | 0.000000 | 0.000000 | 0.000000 | | relaxation | 1.0 | 0.600000 | 1.681586 | 0.434748 | 0.531635 | 0.096886 | | relaxation | 3.0 | 0.395869 | 1.681586 | 0.308339 | 0.531635 | 0.223296 | | relaxation | 4.0 | 0.000000 | 0.630197 | 0.085948 | 0.336306 | 0.250357 | | relaxation | 7.0 | 0.000000 | 0.140616 | 0.004279 | 0.336306 | 0.332027 | During force hold, compare the extension at 1 and 3 s. During extension hold, compare those forces instead. During the latter hold, boundary work stays constant while spring storage decreases and $D$ rises. At 4 s the applied force is zero, yet extension and stored energy remain positive. Recovery consumes that storage through viscous loss. At finite time 7 s a residual extension remains; the figure does not declare full recovery. Try viscosity 20,000 and 500,000 Pa s, then change the ramp duration while retaining the same force target. Compare the same protocol boundary times and read $U$, $W$, $D$ and the residual separately. Set the Maxwell branch off: there is no viscous loss, force hold no longer creeps, and restoring zero force restores zero strain and storage. Reverse the taper or use two equal-length areas; the strain field and extension change through $A(x)$ while the same constitutive law remains in force. The scene uses a fixed physical reference scale, explicitly magnifies axial displacement tenfold, and colors strain against a fixed ±5% scale. Thickness is schematic; there is no predicted lateral contraction. Changing a model or protocol parameter deliberately starts a new experiment and clears time, memory and energy history. Invalid edits retain the prior valid state. Reset restores the authored defaults. Step and Play advance physical time; Run completes the bounded protocol in small animation-frame batches. Export includes the initial row and every accepted observation. Controls restrict positive geometry, equilibrium modulus at least 100,000 Pa, force at most 0.6 N and area ratio at least 0.5. The true narrow-end strain remains at most 4% in these tensile protocols, below the unchanged 5% small-strain warning used in the earlier axial lesson. The runtime rejects inconsistent constitutive state, imposed-force schedules, held extension or energy ledger rather than transferring an arbitrary state to new coefficients. ## What the real proofs establish The eleven declarations below quantify real local constitutive variables. They check storage and loss signs, the storage derivative given path derivatives, power balance **assuming** the Maxwell equation, the zero-branch elastic limit, and the exact held-strain exponential's derivative, bounds and weak monotonicity. They do not prove the force-controlled bar reduction, midpoint quadrature, JavaScript arithmetic or exported discrete energy ledger. Independent numerical and actual-control checks cover those implementation obligations separately. No anatomical calibration, force–velocity muscle law or completed capstone follows from this example. **Checked claim dissipative-real-storage-sign:** Local real stored energy is nonnegative. **Assumptions:** Real E0>=0, E1>=0; any real total strain eps and viscous strain v. ```lean theorem storage_nonnegative (E0 E1 eps v : ℝ) (h0 : 0 ≤ E0) (h1 : 0 ≤ E1) : 0 ≤ storage E0 E1 eps v ``` **Limits:** U=E0\*eps\^2/2+E1\*(eps-v)\^2/2. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.storage_nonnegative`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). **Checked claim dissipative-real-dissipation-sign:** Local real dissipation rate eta\*vdot\^2 is nonnegative. **Assumptions:** Real eta>=0; any real viscous-strain rate vdot. ```lean theorem dissipation_nonnegative (eta vdot : ℝ) (heta : 0 ≤ eta) : 0 ≤ dissipationRate eta vdot ``` **Limits:** Ddot=eta\*vdot\^2. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.dissipation_nonnegative`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). **Checked claim dissipative-real-storage-derivative:** The real storage time derivative equals E0\*eps\*epsdot+E1\*(eps-v)\*(epsdot-vdot). **Assumptions:** Fixed real E0,E1; supplied real strain paths eps(t),v(t) with HasDerivAt eps epsdot t and HasDerivAt v vdot t. ```lean theorem storage_hasDerivAt (E0 E1 t epsdot vdot : ℝ) (eps v : ℝ → ℝ) (heps : HasDerivAt eps epsdot t) (hv : HasDerivAt v vdot t) : HasDerivAt (fun s => storage E0 E1 (eps s) (v s)) (storageRate E0 E1 (eps t) (v t) epsdot vdot) t ``` **Limits:** Derivative of U for fixed constitutive coefficients and supplied path derivatives. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.storage_hasDerivAt`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). **Checked claim dissipative-real-power-balance:** Real stress power equals storage rate plus dissipation under the Maxwell equation. **Assumptions:** Real E0,E1,eps,v,eta,epsdot,vdot; assumed constitutive constraint eta\*vdot=E1\*(eps-v). ```lean theorem local_power_balance (E0 E1 eps v eta epsdot vdot : ℝ) (hMaxwell : eta * vdot = E1 * (eps - v)) : stress E0 E1 eps v * epsdot = storageRate E0 E1 eps v epsdot vdot + dissipationRate eta vdot ``` **Limits:** sigma\*epsdot=Udot+Ddot; the constitutive constraint is an explicit assumption. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.local_power_balance`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). **Checked claim dissipative-real-elastic-recovery:** Setting E1=0 recovers sigma=E0\*eps and U=E0\*eps\^2/2. **Assumptions:** Real E0,eps,v; the Maxwell spring coefficient E1 is exactly zero. ```lean theorem zero_branch_recovers_elastic (E0 eps v : ℝ) : stress E0 0 eps v = E0 * eps ∧ storage E0 0 eps v = E0 / 2 * eps ^ 2 ``` **Limits:** Zero-branch elastic reference; no whole-bar geometry or numerical equivalence is asserted. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.zero_branch_recovers_elastic`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). **Checked claim dissipative-real-viscous-derivative:** The exact held-strain exponential has derivative E1\*(eps-v(t))/eta. **Assumptions:** Fixed real held strain eps, initial viscous strain v0, E1, eta!=0; any real elapsed time t. ```lean theorem viscous_strain_hasDerivAt (eps v0 E1 eta t : ℝ) (heta : eta ≠ 0) : HasDerivAt (fun s => viscousStrain eps v0 E1 eta s) (E1 * (eps - viscousStrain eps v0 E1 eta t) / eta) t ``` **Limits:** v(t)=eps+(v0-eps)\*exp(-E1\*t/eta); constant strain and coefficients only. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.viscous_strain_hasDerivAt`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). **Checked claim dissipative-real-viscous-bounds:** Forward held-strain viscous strain stays between v0 and eps. **Assumptions:** Real held strain eps and initial v0; E1>=0, eta>0 and elapsed time t>=0. ```lean theorem viscous_strain_bounded (eps v0 E1 eta t : ℝ) (hE : 0 ≤ E1) (heta : 0 < eta) (ht : 0 ≤ t) : min v0 eps ≤ viscousStrain eps v0 E1 eta t ∧ viscousStrain eps v0 E1 eta t ≤ max v0 eps ``` **Limits:** min(v0,eps)<=v(t)<=max(v0,eps); no general changing-load trajectory is certified. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.viscous_strain_bounded`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). **Checked claim dissipative-real-viscous-monotone:** Viscous strain is nondecreasing toward the held strain when v0<=eps. **Assumptions:** Real fixed eps,v0; E1>=0, eta>0 and v0<=eps; ordered real comparison times s<=t. ```lean theorem viscous_strain_monotone (eps v0 E1 eta : ℝ) (hE : 0 ≤ E1) (heta : 0 < eta) (hstart : v0 ≤ eps) : Monotone (fun t => viscousStrain eps v0 E1 eta t) ``` **Limits:** Weak monotonicity includes E1=0 and v0=eps; no asymptotic-limit or numerical step proof. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.viscous_strain_monotone`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). **Checked claim dissipative-real-viscous-antitone:** Viscous strain is nonincreasing toward the held strain when eps<=v0. **Assumptions:** Real fixed eps,v0; E1>=0, eta>0 and eps<=v0; ordered real comparison times s<=t. ```lean theorem viscous_strain_antitone (eps v0 E1 eta : ℝ) (hE : 0 ≤ E1) (heta : 0 < eta) (hstart : eps ≤ v0) : Antitone (fun t => viscousStrain eps v0 E1 eta t) ``` **Limits:** Weak monotonicity includes E1=0 and eps=v0; no asymptotic-limit or numerical step proof. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.viscous_strain_antitone`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). **Checked claim dissipative-real-held-stress-bounds:** Forward held-strain stress lies between E0\*eps and its initial value when v0<=eps. **Assumptions:** Real E0,eps,v0; E1>=0, eta>0, t>=0 and v0<=eps; sigma(t)=E0\*eps+E1\*(eps-v(t)). ```lean theorem held_stress_bounded (E0 E1 eps v0 eta t : ℝ) (hE : 0 ≤ E1) (heta : 0 < eta) (ht : 0 ≤ t) (hstart : v0 ≤ eps) : E0 * eps ≤ stress E0 E1 eps (viscousStrain eps v0 E1 eta t) ∧ stress E0 E1 eps (viscousStrain eps v0 E1 eta t) ≤ stress E0 E1 eps v0 ``` **Limits:** Relative bounds require the stated initial ordering; no assertion of positive stress for arbitrary real strain. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.held_stress_bounded`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). **Checked claim dissipative-real-held-stress-decay:** Held-strain stress is nonincreasing when v0<=eps. **Assumptions:** Real E0,eps,v0; E1>=0, eta>0 and v0<=eps; ordered real comparison times s<=t. ```lean theorem held_stress_antitone (E0 E1 eps v0 eta : ℝ) (hE : 0 ≤ E1) (heta : 0 < eta) (hstart : v0 ≤ eps) : Antitone (fun t => stress E0 E1 eps (viscousStrain eps v0 E1 eta t)) ``` **Limits:** Stress relaxation under constant imposed strain; no changing-load or force-controlled creep trajectory proof. Real local constitutive law only; no numerical or JavaScript refinement, axial-bar or quadrature solve, discrete energy-ledger, calibration or biological validation. Declaration: `Kenoma.DissipativeBarReal.held_stress_antitone`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: 7368497bd84dcb8ab8e020270a4823d233424601b0225e546393114b7141c972. [Full checked source](proofs/DissipativeBarReal.lean); [receipt](dissipative-real-proof-status.json). Continue to [anatomical evidence](#anatomy-is-evidence) before deciding which properties a named tissue would need. The anatomical capstone and its calibration obligations remain separate. Continue with [unequal blocks under one force](#serial-specimen-volume) to connect finite force-driven stretches, current areas and local incompressibility in a separate two-block 3D assembly. The SLS law and energy history above remain unchanged. ### Interactive 3D: Load, hold and recovery specimen Scrub the existing finite SLS protocol and compare work, storage and loss. **Evidence class:** Numerical demonstration. **Scope:** One-dimensional small-strain bar extruded for viewing; transverse area is not solved. [Open the shared Kenoma GUI](examples.html?chapter=09c-dissipative-response). # One force, unequal stretches, and local volume {#serial-specimen-volume} ## Worked reading ### 1. Begin with two separate unloaded blocks The second reference cross-section is twice the first. A massless spacer transmits the same axial force and allows the blocks to slide laterally at their ideal fixtures. **Observe:** Both stretches and measured volume ratios are 1; current areas are 300 and 600 mm². The gap and grey connector represent the spacer, not missing tissue. ### 2. Transmit one tensile force Apply +0.1 N to both blocks. The narrower block needs twice the nominal stress, so the same neo-Hookean law gives it the greater stretch. **Observe:** Stretches are about 1.07983 and 1.03844; current areas shrink to 277.821 and 577.788 mm². Each measured volume ratio remains 1. ### 3. Reverse the signed load Apply −0.1 N using the same bilateral fixtures. The narrower block now shortens more and expands more laterally; neither block changes its local volume. **Observe:** Stretches become about 0.931143 and 0.964301; areas become 322.185 and 622.212 mm². The shared force does not imply equal stress or equal strain. ### 4. Expose finite root error Restore tension but reduce the bisection cap to eight. Incompressibility remains imposed exactly while axial force balance is only approximated. **Observe:** The maximum force residual is about 0.00164715 N, above the 1e-10 N criterion, so Converged is false even though both volumes are preserved. **Question:** can blocks of the same material carry the same force, stretch by different amounts, and each preserve volume? The [reduced axial bar](#measure-deformation-before-choosing-a-muscle-law) already demonstrates uneven strain from an input area profile, including local extension and compression under fixed ends. It predicts no lateral deformation. This lesson adds a different, explicitly three-dimensional specimen and a constitutive law whose force, current area and local volume agree. ## Two blocks and an explicit interface Use two separate, homogeneous rectangular blocks in axial series. Each has a square reference section and reference length $L_0=0.025$ m. Their reference areas are $A_1=0.0003$ m² and $A_2=rA_1$, with default $r=2$. Ideal **bilateral axial traction fixtures** transmit signed force and permit tangential sliding at the loading faces. They can pull or push; ordinary frictionless compression platens alone could not provide the tensile case. A massless spacer has fixed length 0.012 m. Its positions move with the block ends. The two blocks may therefore change lateral size independently. The gold fixture connection is excluded from material volume. This is an assembly of separate blocks, not a continuous stepped or tapered solid with an unmodeled material interface. The solved deformation is homogeneous within each block. Buckling, shear localization and the preferred deformation among unrestricted 3D fields are outside this homogeneous model. With no body load, the intervening massless fixture balances the two opposing axial resultants, so $N_1=N_2=N$. Positive $N$ is tension and negative $N$ is compression. The equilibrium equation uses **reference** area for nominal stress, and current area for Cauchy stress; these are different stress measures. ## Material response and the volume constraint Each block is an incompressible isotropic neo-Hookean solid with authored shear parameter $\mu=1500$ Pa. Its energy per reference volume is $$W(F)=\frac\mu2(I_1-3),\qquad J=\det F=1.$$ Incompressibility is a **local material constraint**. It is not a finite bulk penalty, and constant force does not establish it. The earlier [bulk/shear confinement lesson](#compression-bulk-shear-confinement) retains its different finite-bulk law and boundary conditions. The material framework and the role of incompressibility pressure are described by [A. F. Bower, *Applied Mechanics of Solids*, §§3.5.4–3.5.6](https://solidmechanics.org/Text/Chapter3_5/Chapter3_5.php). The following homogeneous reduction and assembly are the model used here. For axial stretch $\lambda_i>0$ and equal transverse stretches $b_i>0$, $$F_i=\operatorname{diag}(\lambda_i,b_i,b_i),\qquad J_i=\lambda_i b_i^2=1,\qquad b_i=\lambda_i^{-1/2}.$$ The full Cauchy stress is $\sigma_i=-p_iI+\mu B_i$, where $B_i=F_iF_i^T$. Free lateral faces require $\sigma_{yy}=\sigma_{zz}=0$, giving $p_i=\mu b_i^2=\mu/\lambda_i$. This $p_i$ is an **incompressibility multiplier**, not measured axial plate pressure. At rest it is $\mu$, while the complete stress tensor is zero. The resulting axial Cauchy and nominal stresses are $$\sigma_{xx,i}=\mu(\lambda_i^2-\lambda_i^{-1}),\qquad P_i=\frac{\sigma_{xx,i}}{\lambda_i} =\mu(\lambda_i-\lambda_i^{-2}),\qquad N=A_iP_i.$$ The executable root solves this last equation separately for both blocks. It does not assign stretches from a visual taper. The reduced energy and its derivative use the same material law: $$W(\lambda)=\frac\mu2(\lambda^2+2/\lambda-3) =\frac{\mu}{2\lambda}(\lambda-1)^2(\lambda+2),\qquad \frac{dW}{d\lambda}=P(\lambda).$$ Thus $U_i=A_iL_0W(\lambda_i)$, and differentiating with respect to current block length $L_i=L_0\lambda_i$ gives $dU_i/dL_i=A_iP_i=N$. The response is elastic and history-free; no time integration, activation or viscous loss is added. ## Solve, measure, and compare For positive stretch and $\mu>0$, $$\frac{dP}{d\lambda}=\mu(1+2/\lambda^3)>0.$$ The force curve is strictly increasing, with zero force at $\lambda=1$. The narrower section has larger nominal tensile stress and larger stretch for $N>0$. With $N<0$ it has more negative stress and smaller stretch: it compresses more. Both blocks have the same material; this difference comes from geometry. The current geometry is calculated from the solved stretches: $$L_i=L_0\lambda_i,\qquad A_{i,\mathrm{current}}=A_i b_i^2=A_i/\lambda_i, \qquad V_i=A_iL_0,\qquad \sigma_{xx,i}=N/A_{i,\mathrm{current}}.$$ The 3D meshes use these actual lengths, widths and depths without displacement magnification. Gray wire outlines mark the reference blocks; the camera uses a shared physical scale across parameter edits. Front/oblique views change the camera, not the model. Exported vertices drive a separate closed-triangle volume measurement. Measured cross-sectional edges, length and boundary volume are reported beside $J_i$; the volume oracle does not simply return one. ![Solved default tension, rest and compression at one physical scale. Dashed outlines are reference blocks; the moving gold spacer is excluded from material volume.](assets/property-serial.svg) ### Property lab 6 · Force, current area and local volume Two separate homogeneous square prisms in axial series, with ideal bilateral traction-distributing fixtures that allow lateral sliding. A fixed-length massless spacer moves with their ends. This is an assembly of two blocks, not a continuous stepped solid. [Open the physical-scale assembly](index.html#lab-serial-specimen). Default forces, areas, stretches and independent measured volumes are generated from the same executable law: | Load (N) | Block | Stretch λ | Axial strain | Area (mm²) | Volume (mm³) | Force residual (N) | |--:|--:|--:|--:|--:|--:|--:| | 0.100 | 1 | 1.079830 | 0.079830 | 277.821 | 7500.000 | 2.22e-15 | | 0.100 | 2 | 1.038443 | 0.038443 | 577.788 | 15000.000 | 1.6e-15 | | 0.000 | 1 | 1.000000 | 0.000000 | 300.000 | 7500.000 | 0 | | 0.000 | 2 | 1.000000 | 0.000000 | 600.000 | 15000.000 | 0 | | -0.100 | 1 | 0.931143 | -0.068857 | 322.185 | 7500.000 | -2.39e-15 | | -0.100 | 2 | 0.964301 | -0.035699 | 622.212 | 15000.000 | 5.58e-15 | **Try and predict.** Reverse $N$ from +0.1 to -0.1 N. Both blocks shorten and widen, and the narrower block has the larger compression. Set $N=0$: both stretches, areas and lengths return to their reference values, and stress and energy vanish. Set $r=1$: equal material and area give equal stretches. Reverse the ratio to $r=0.5$: block 2 becomes the narrow section and now strains more. Increase only $\mu$: at the same force the stretches move closer to one. Reference length changes total extension, volume and energy, but does not change local stress or stretch at fixed area and force. **Local-volume counterexample.** The test button constructs an unused candidate with unchanged axial stretches but local volume ratios 1.10 and $1-0.10/r$. Their reference-volume-weighted total is still one. Nevertheless, each block violates $J_i=1$, and its free-side traction no longer vanishes. The candidate is rejected and the prior solved mesh and state remain visible. A correct total volume cannot hide a violation of this local material law. Controls bound $500\le\mu\le5000$ Pa, $0.0003\le A_1\le0.001$ m², $0.5\le r\le4$, $-0.1\le N\le0.1$ N, and $0.01\le L_0\le0.04$ m. Every target force lies within the fixed positive bracket $0.6\le\lambda\le1.75$: at the smallest $A_i\mu=0.075$ N its endpoint forces are approximately -0.163333 and +0.106760 N. Bisection uses a visible 8–64 iteration cap. The force criterion is $|A_iP_i-N|\le10^{-10}$ N for **each** block. Eight iterations can leave a valid positive-volume shape with unequal approximate resultants; the UI reports each computed resultant and residual, rather than calling it shared-force equilibrium. Restore 48 or 64 and compare. Invalid edits retain the prior valid specimen; Reset restores the authored defaults and reference camera. ## Exact real claims and independent implementation checks Twelve declarations below quantify the actual real homogeneous law. They prove the energy factor, sign and zero state; its derivative; stress identities and signs; strict monotonicity and conditional positive-root uniqueness; area-times- length volume; and same-force ordering for unequal areas in tension and compression. Root existence, numerical bisection, pressure elimination, the matrix/mesh volume measurement and JavaScript arithmetic are not certified by these declarations. The real kinematic identities in the first property lessons remain separate. **Checked claim serial-real-energy-factor:** The real homogeneous neo-Hookean energy has the exact nonnegative-factor form. **Assumptions:** Real mu; lambda>0. ```lean theorem energy_factor (mu l : ℝ) (hl : 0 < l) : energy mu l = mu / (2 * l) * (l - 1) ^ 2 * (l + 2) ``` **Limits:** W=mu/(2\*lambda)\*(lambda-1)\^2\*(lambda+2); signs are not assumed in this algebraic identity. Real local homogeneous incompressible material law only; no JavaScript refinement, numerical root or mesh-volume validation, continuous stepped-solid interface, global stability, bulk-penalty calibration or anatomical claim. Declaration: `Kenoma.SerialSpecimenReal.energy_factor`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: b0b4ccb250f7a10561c66fc32def5aad4f3ec900eeb3575a3e8bd4aacf0f3fbe. [Full checked source](proofs/SerialSpecimenReal.lean); [receipt](serial-real-proof-status.json). **Checked claim serial-real-energy-sign:** Real homogeneous stored energy is nonnegative. **Assumptions:** Real mu>=0 and lambda>0. ```lean theorem energy_nonnegative (mu l : ℝ) (hm : 0 ≤ mu) (hl : 0 < l) : 0 ≤ energy mu l ``` **Limits:** W=mu/2\*(lambda\^2+2/lambda-3); this is local energy, not global specimen stability. Real local homogeneous incompressible material law only; no JavaScript refinement, numerical root or mesh-volume validation, continuous stepped-solid interface, global stability, bulk-penalty calibration or anatomical claim. Declaration: `Kenoma.SerialSpecimenReal.energy_nonnegative`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: b0b4ccb250f7a10561c66fc32def5aad4f3ec900eeb3575a3e8bd4aacf0f3fbe. [Full checked source](proofs/SerialSpecimenReal.lean); [receipt](serial-real-proof-status.json). **Checked claim serial-real-energy-zero:** Real homogeneous stored energy vanishes exactly at lambda=1. **Assumptions:** Real mu>0 and lambda>0. ```lean theorem energy_zero_iff (mu l : ℝ) (hm : 0 < mu) (hl : 0 < l) : energy mu l = 0 ↔ l = 1 ``` **Limits:** The zero-energy state of this one-parameter homogeneous law is unique; no global minimization is certified. Real local homogeneous incompressible material law only; no JavaScript refinement, numerical root or mesh-volume validation, continuous stepped-solid interface, global stability, bulk-penalty calibration or anatomical claim. Declaration: `Kenoma.SerialSpecimenReal.energy_zero_iff`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: b0b4ccb250f7a10561c66fc32def5aad4f3ec900eeb3575a3e8bd4aacf0f3fbe. [Full checked source](proofs/SerialSpecimenReal.lean); [receipt](serial-real-proof-status.json). **Checked claim serial-real-energy-derivative:** The exact real derivative of W with respect to lambda equals nominal axial stress P. **Assumptions:** Fixed real mu; lambda>0. ```lean theorem energy_hasDerivAt (mu l : ℝ) (hl : 0 < l) : HasDerivAt (energy mu) (nominalStress mu l) l ``` **Limits:** HasDerivAt W P lambda, with P=mu\*(lambda-1/lambda\^2); no numerical differentiation is certified. Real local homogeneous incompressible material law only; no JavaScript refinement, numerical root or mesh-volume validation, continuous stepped-solid interface, global stability, bulk-penalty calibration or anatomical claim. Declaration: `Kenoma.SerialSpecimenReal.energy_hasDerivAt`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: b0b4ccb250f7a10561c66fc32def5aad4f3ec900eeb3575a3e8bd4aacf0f3fbe. [Full checked source](proofs/SerialSpecimenReal.lean); [receipt](serial-real-proof-status.json). **Checked claim serial-real-stress-identities:** Nominal stress factors through lambda-1, and axial Cauchy stress equals lambda\*P. **Assumptions:** Real mu and lambda>0. ```lean theorem nominal_factor_and_cauchy (mu l : ℝ) (hl : 0 < l) : nominalStress mu l = mu * (l - 1) * (l ^ 2 + l + 1) / l ^ 2 ∧ cauchyStress mu l = l * nominalStress mu l ``` **Limits:** P=mu\*(lambda-1)\*(lambda\^2+lambda+1)/lambda\^2; sigma=mu\*(lambda\^2-1/lambda)=lambda\*P. Lateral pressure and matrix stress equations are not proved here. Real local homogeneous incompressible material law only; no JavaScript refinement, numerical root or mesh-volume validation, continuous stepped-solid interface, global stability, bulk-penalty calibration or anatomical claim. Declaration: `Kenoma.SerialSpecimenReal.nominal_factor_and_cauchy`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: b0b4ccb250f7a10561c66fc32def5aad4f3ec900eeb3575a3e8bd4aacf0f3fbe. [Full checked source](proofs/SerialSpecimenReal.lean); [receipt](serial-real-proof-status.json). **Checked claim serial-real-stress-sign:** Nominal stress is tensile, zero or compressive exactly when lambda is above, equal to or below one. **Assumptions:** Real mu>0 and lambda>0. ```lean theorem nominal_sign (mu l : ℝ) (hm : 0 < mu) (hl : 0 < l) : (0 < nominalStress mu l ↔ 1 < l) ∧ (nominalStress mu l = 0 ↔ l = 1) ∧ (nominalStress mu l < 0 ↔ l < 1) ``` **Limits:** All three sign equivalences concern this homogeneous local law. Real local homogeneous incompressible material law only; no JavaScript refinement, numerical root or mesh-volume validation, continuous stepped-solid interface, global stability, bulk-penalty calibration or anatomical claim. Declaration: `Kenoma.SerialSpecimenReal.nominal_sign`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: b0b4ccb250f7a10561c66fc32def5aad4f3ec900eeb3575a3e8bd4aacf0f3fbe. [Full checked source](proofs/SerialSpecimenReal.lean); [receipt](serial-real-proof-status.json). **Checked claim serial-real-stress-difference:** The real nominal-stress difference has an exact positive-factor identity. **Assumptions:** Real mu; positive stretches u>0 and v>0. ```lean theorem nominal_difference (mu u v : ℝ) (hu : 0 < u) (hv : 0 < v) : nominalStress mu v - nominalStress mu u = mu * (v - u) * (1 + (u + v) / (u ^ 2 * v ^ 2)) ``` **Limits:** P(v)-P(u)=mu\*(v-u)\*(1+(u+v)/(u\^2\*v\^2)); this row states an algebraic identity. Real local homogeneous incompressible material law only; no JavaScript refinement, numerical root or mesh-volume validation, continuous stepped-solid interface, global stability, bulk-penalty calibration or anatomical claim. Declaration: `Kenoma.SerialSpecimenReal.nominal_difference`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: b0b4ccb250f7a10561c66fc32def5aad4f3ec900eeb3575a3e8bd4aacf0f3fbe. [Full checked source](proofs/SerialSpecimenReal.lean); [receipt](serial-real-proof-status.json). **Checked claim serial-real-stress-monotone:** Real nominal stress is strictly increasing on positive axial stretches. **Assumptions:** Fixed real mu>0; stretches in (0,infinity). ```lean theorem nominal_strictMono (mu : ℝ) (hm : 0 < mu) : StrictMonoOn (nominalStress mu) (Set.Ioi 0) ``` **Limits:** StrictMonoOn P (Set.Ioi 0); no global multiaxial stability is certified. Real local homogeneous incompressible material law only; no JavaScript refinement, numerical root or mesh-volume validation, continuous stepped-solid interface, global stability, bulk-penalty calibration or anatomical claim. Declaration: `Kenoma.SerialSpecimenReal.nominal_strictMono`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: b0b4ccb250f7a10561c66fc32def5aad4f3ec900eeb3575a3e8bd4aacf0f3fbe. [Full checked source](proofs/SerialSpecimenReal.lean); [receipt](serial-real-proof-status.json). **Checked claim serial-real-root-unique:** A fixed axial force has at most one positive homogeneous stretch root. **Assumptions:** Real mu>0, reference area A>0 and any real N; u>0,v>0 with A\*P(u)=N and A\*P(v)=N. ```lean theorem homogeneous_root_unique (mu A N u v : ℝ) (hm : 0 < mu) (hA : 0 < A) (hu : 0 < u) (hv : 0 < v) (hNu : A * nominalStress mu u = N) (hNv : A * nominalStress mu v = N) : u = v ``` **Limits:** Uniqueness only; existence, bisection brackets, termination and residual accuracy are not proved. Real local homogeneous incompressible material law only; no JavaScript refinement, numerical root or mesh-volume validation, continuous stepped-solid interface, global stability, bulk-penalty calibration or anatomical claim. Declaration: `Kenoma.SerialSpecimenReal.homogeneous_root_unique`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: b0b4ccb250f7a10561c66fc32def5aad4f3ec900eeb3575a3e8bd4aacf0f3fbe. [Full checked source](proofs/SerialSpecimenReal.lean); [receipt](serial-real-proof-status.json). **Checked claim serial-real-volume:** The imposed current area and length preserve each block reference volume exactly. **Assumptions:** Real reference area A and length L; lambda>0; current area is A/lambda and current length is L\*lambda. ```lean theorem area_length_volume (A L l : ℝ) (hl : 0 < l) : (A / l) * (L * l) = A * L ``` **Limits:** (A/lambda)\*(L\*lambda)=A\*L. Incompressibility and these geometric formulas are assumptions; mesh boundary integration and det(F) are not certified. Real local homogeneous incompressible material law only; no JavaScript refinement, numerical root or mesh-volume validation, continuous stepped-solid interface, global stability, bulk-penalty calibration or anatomical claim. Declaration: `Kenoma.SerialSpecimenReal.area_length_volume`. Lean 4.19.0; pinned mathlib v4.19.0; commit c44e0c8ee63ca166450922a373c7409c5d26b00b; locked transitive dependencies; transitive axioms: propext, Classical.choice, Quot.sound; source SHA-256: b0b4ccb250f7a10561c66fc32def5aad4f3ec900eeb3575a3e8bd4aacf0f3fbe. [Full checked source](proofs/SerialSpecimenReal.lean); [receipt](serial-real-proof-status.json). **Checked claim serial-real-tension-order:** Under equal tensile force, the narrower reference block stretches more. **Assumptions:** Common real mu>0; 00; positive stretches lambda1,lambda2 satisfying A1\*P(lambda1)=A2\*P(lambda2)=N. ```lean theorem same_force_tension_order (mu A1 A2 N l1 l2 : ℝ) (hm : 0 < mu) (hA1 : 0 < A1) (hA : A1 < A2) (hN : 0 < N) (hl1 : 0 < l1) (hl2 : 0 < l2) (h1 : A1 * nominalStress mu l1 = N) (h2 : A2 * nominalStress mu l2 = N) : 1 < l2 ∧ l2 < l1 ``` **Limits:** 10; 0