RRF.Core.Strain
IndisputableMonolith.RRF.Core.Strain
No prose has been written for this declaration yet. The Lean source and graph data below render without it.
generate prose now
From the project-wide theorem graph. These declarations reference this one in their body.
IndisputableMonolith.RRF.Core
IndisputableMonolith.RRF.Core.Glossary
IndisputableMonolith.RRF.Core.Octave
IndisputableMonolith.RRF.Foundation.VantageCategory
IndisputableMonolith.RRF.Theorems.OrderPreservation
StrainFunctional
NonNeg
isBalanced
equilibria
hasUniqueMin
strictlyBetter
weaklyBetter
isMinimizer
equilibria_are_minimizers
LedgerConstraint
isClosed
net
closed_iff_net_zero
StrainLedger
isValid
validStates