theorem proved term proof

`trivial_is_minimizer`

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)

  37theorem trivial_is_minimizer : trivialStrain.isMinimizer () :=

proof body

Term-mode proof.

  38  StrainFunctional.equilibria_are_minimizers () trivial_balanced
  39
  40/-- Trivial ledger: zero debit and credit. -/

depends on (7)

Lean names referenced from this declaration's body.

and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
isMinimizer in IndisputableMonolith.RRF.Core.Glossary decl_use
equilibria_are_minimizers in IndisputableMonolith.RRF.Core.Strain decl_use
isMinimizer in IndisputableMonolith.RRF.Core.Strain decl_use
StrainFunctional in IndisputableMonolith.RRF.Core.Strain decl_use
trivial_balanced in IndisputableMonolith.RRF.Models.Trivial decl_use
trivialStrain in IndisputableMonolith.RRF.Models.Trivial decl_use