pith. machine review for the scientific record. sign in
def definition def or abbrev

GeometricStrain

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  28noncomputable def GeometricStrain (r : ℝ) : ℝ :=

proof body

Definition body.

  29    if h : r > 0 then
  30      -- Use floor(log_phi(r) + 1/2) as a proxy for the nearest integer rung
  31      let n := Int.floor (Real.log r / Real.log phi + 1/2)
  32      Jcost (r / (phi ^ (n : ℝ)))
  33    else
  34      1.0 -- Arbitrary positive value for non-positive scales
  35
  36/-- **DEFINITION: System Stability (S_sys)**
  37    Stability is higher when geometric strain is lower. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.