Uneven stretch.
Where does the volume go?

The same reference scale, before and after

The declared map and its limits

λ(S) = λ̄ [1 + a(2S/L₀ − 1)]
x(S) = λ̄ [(1 − a)S + aS²/L₀]
y = b(S)Y,  z = b(S)Z
b(S) = 1/√λ(S) with compensation; b = 1 otherwise
dλ/dS = 2λ̄a/L₀
b′(S) = −(dλ/dS)/(2λ(S)^(3/2)) with compensation

F = [ λ      0  0 ]
    [ b′Y    b  0 ]
    [ b′Z    0  b ]
J = det F = λb²

λ > 0 makes the axial map monotone. Compensation gives J = 1 for the exact continuum map. The off-diagonal terms b′Y and b′Z describe the additional shear away from the centerline; a nonuniform stretch is not a sequence of unrelated uniform blocks. The reported engineering strain λ − 1 is the axial-line strain at Y = Z = 0.

With compensation off and mean stretch one, total volume is still unchanged because expansion and contraction cancel. Local J then differs from one. A near-unity total-volume number alone therefore does not establish local volume preservation.

Finite boundary triangles approximate the exact curved map. Their volume error is reported and should decrease with refinement. These geometric results do not establish a passive equilibrium, a muscle law, pressure, or anatomical completion.

Six freshly checked Real contracts

Lean checks the declared matrix determinant, positive interval stretch and an algebraic straight-cell error formula. The derivative, change-of-variables argument, mesh topology and floating-point implementation are separate audit obligations. This accepted extension added six scoped contracts to the original 103, giving 109 at its historical integration. The current book registry contains 115 declarations, including six architecture-force contracts.

Download complete Lean source · Exact statement inventory · Source-bound check receipt · Kernel dependency report · Separate model audit

theorem gradient_determinant (lambda b shearY shearZ : ℝ) :
    Matrix.det (gradientField lambda b shearY shearZ) = lambda * b * b

theorem positive_stretch_on_interval (m a L S : ℝ)
    (hm : 0 < m) (hL : 0 < L) (haLower : -1 < a) (haUpper : a < 1)
    (hS : 0 ≤ S) (hSL : S ≤ L) : 0 < stretch m a L S

theorem pointwise_isochoric_gradient (lambda shearY shearZ : ℝ)
    (hlambda : 0 < lambda) :
    0 < transverse lambda ∧
      Matrix.det (gradientField lambda (transverse lambda) shearY shearZ) = 1

theorem nonuniform_isochoric_on_interval (m a L S shearY shearZ : ℝ)
    (hm : 0 < m) (hL : 0 < L) (haLower : -1 < a) (haUpper : a < 1)
    (hS : 0 ≤ S) (hSL : S ≤ L) :
    0 < transverse (stretch m a L S) ∧
      Matrix.det (gradientField (stretch m a L S)
        (transverse (stretch m a L S)) shearY shearZ) = 1

theorem straight_cell_error_factorization (r : ℝ) (hr : 0 < r) :
    straightCellRatio r - 1 =
      (r - 1) ^ 2 * (r ^ 2 + 3 * r + 1) / (6 * r ^ 2)

theorem straight_cell_ratio_ge_one (r : ℝ) (hr : 0 < r) :
    1 ≤ straightCellRatio r

Complete checked Lean source

import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring

/-!
Prescribed finite kinematics over Real. The matrix is the declared gradient
field, including off-axis shear. These contracts prove its algebraic determinant
and positive stretch on the stated material interval. They do not formally
derive the gradient, prove a change-of-variables integral, triangulation
correctness, floating-point refinement, equilibrium or biological validity.
-/
noncomputable section

namespace KenomaNonuniform

def stretch (m a L S : ℝ) : ℝ := m * (1 + a * (2 * (S / L) - 1))

def transverse (lambda : ℝ) : ℝ := 1 / Real.sqrt lambda

def gradientField (lambda b shearY shearZ : ℝ) : Matrix (Fin 3) (Fin 3) ℝ :=
  ![![lambda, 0, 0], ![shearY, b, 0], ![shearZ, 0, b]]

theorem gradient_determinant (lambda b shearY shearZ : ℝ) :
    Matrix.det (gradientField lambda b shearY shearZ) = lambda * b * b := by
  simp [gradientField, Matrix.det_fin_three, mul_assoc]

theorem positive_stretch_on_interval (m a L S : ℝ)
    (hm : 0 < m) (hL : 0 < L) (haLower : -1 < a) (haUpper : a < 1)
    (hS : 0 ≤ S) (hSL : S ≤ L) : 0 < stretch m a L S := by
  have ht0 : 0 ≤ S / L := div_nonneg hS hL.le
  have ht1 : S / L ≤ 1 := (div_le_one hL).mpr hSL
  have hinner : 0 < 1 + a * (2 * (S / L) - 1) := by
    rcases le_total 0 a with ha | ha
    · have hprod := mul_nonneg ha ht0
      nlinarith
    · have hprod := mul_nonneg (neg_nonneg.mpr ha) (sub_nonneg.mpr ht1)
      nlinarith
  exact mul_pos hm hinner

theorem pointwise_isochoric_gradient (lambda shearY shearZ : ℝ)
    (hlambda : 0 < lambda) :
    0 < transverse lambda ∧
      Matrix.det (gradientField lambda (transverse lambda) shearY shearZ) = 1 := by
  constructor
  · exact one_div_pos.mpr (Real.sqrt_pos.mpr hlambda)
  · rw [gradient_determinant]
    calc
      lambda * transverse lambda * transverse lambda =
          lambda * (Real.sqrt lambda * Real.sqrt lambda)⁻¹ := by
        simp only [transverse, one_div, mul_assoc, mul_inv]
      _ = 1 := by
        rw [Real.mul_self_sqrt hlambda.le]
        exact mul_inv_cancel₀ (ne_of_gt hlambda)

theorem nonuniform_isochoric_on_interval (m a L S shearY shearZ : ℝ)
    (hm : 0 < m) (hL : 0 < L) (haLower : -1 < a) (haUpper : a < 1)
    (hS : 0 ≤ S) (hSL : S ≤ L) :
    0 < transverse (stretch m a L S) ∧
      Matrix.det (gradientField (stretch m a L S)
        (transverse (stretch m a L S)) shearY shearZ) = 1 := by
  exact pointwise_isochoric_gradient _ _ _
    (positive_stretch_on_interval m a L S hm hL haLower haUpper hS hSL)

def straightCellRatio (r : ℝ) : ℝ :=
  (1 + r ^ 2) * (1 + 1 / r + 1 / r ^ 2) / 6

theorem straight_cell_error_factorization (r : ℝ) (hr : 0 < r) :
    straightCellRatio r - 1 =
      (r - 1) ^ 2 * (r ^ 2 + 3 * r + 1) / (6 * r ^ 2) := by
  unfold straightCellRatio
  field_simp [ne_of_gt hr]
  ring

theorem straight_cell_ratio_ge_one (r : ℝ) (hr : 0 < r) :
    1 ≤ straightCellRatio r := by
  have hnum : 0 ≤ (r - 1) ^ 2 * (r ^ 2 + 3 * r + 1) :=
    mul_nonneg (sq_nonneg _) (by nlinarith [sq_nonneg r])
  have hden : 0 ≤ 6 * r ^ 2 := mul_nonneg (by norm_num) (sq_nonneg r)
  have herr := div_nonneg hnum hden
  rw [← straight_cell_error_factorization r hr] at herr
  linarith

end KenomaNonuniform

#print axioms KenomaNonuniform.gradient_determinant
#print axioms KenomaNonuniform.positive_stretch_on_interval
#print axioms KenomaNonuniform.pointwise_isochoric_gradient
#print axioms KenomaNonuniform.nonuniform_isochoric_on_interval
#print axioms KenomaNonuniform.straight_cell_error_factorization
#print axioms KenomaNonuniform.straight_cell_ratio_ge_one

Exact source and toolchain

Source revision 277b7683956033c821ae69c5f0284da93c4cffc2

Lean (version 4.19.0, x86_64-unknown-linux-gnu, commit 6caaee842e94, Release)

Source SHA-256 99029516cf26fca5a82cbd2971c13f9d9d1e6a10face1d71704a6185b7a731ea

Claim-map SHA-256 8cb883bbf102e897ff7f291bc3b46daf22bc4731b95c69d6f4aff109d2b5d43b

Kernel dependency report

'KenomaNonuniform.gradient_determinant' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaNonuniform.positive_stretch_on_interval' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaNonuniform.pointwise_isochoric_gradient' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaNonuniform.nonuniform_isochoric_on_interval' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaNonuniform.straight_cell_error_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
'KenomaNonuniform.straight_cell_ratio_ge_one' depends on axioms: [propext, Classical.choice, Quot.sound]

Separate model and geometry audit

Symbolic differentiation recovers every entry of the declared gradient. Ninety parameter/refinement cases compare closed oriented meshes against high-precision boundary volumes and an independent regular-polygon/frustum route. Surface topology and nondegenerate faces are checked separately.

Independent peer acceptance applies to exact source 15c624c32378b9c773a3d0c25a65150804b68c90; this candidate preserves its mathematical and model source bytes. These routes do not prove force equilibrium, a muscle law or anatomical completion.

{
  "states": 90,
  "closedOrientedMeshes": 90,
  "maximumBoundaryDifferenceM3": 2.574980159653073e-18,
  "maximumReferenceDifferenceM3": 2.4936649967166602e-18,
  "maximumIndependentCellRatioDifference": 8.348877145181177e-14,
  "refinementFamilies": 6,
  "minimumReductionFactorRequired": 3.7
}