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

universalStructure

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)

  84def universalStructure : UniversalStructure := {

proof body

Definition body.

  85  State := ℝ,  -- Real numbers as universal state space
  86  recognizes := fun x y => x = y,  -- Identity recognition
  87  has_self_recognition := ⟨0, rfl⟩,
  88  strain := fun x => x^2,  -- Quadratic strain
  89  strain_nonneg := fun x => sq_nonneg x,
  90}
  91
  92/-! ## The Embedding Theorems -/
  93
  94/-- Physics can be embedded. -/

used by (6)

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

depends on (5)

Lean names referenced from this declaration's body.