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)
93theorem closed_iff_net_zero (L : LedgerConstraint State) (x : State) :
94 L.isClosed x ↔ L.net x = 0 := by
proof body
Term-mode proof.
95 simp [isClosed, net, sub_eq_zero]
96
97end LedgerConstraint
98
99/-- Combined strain and ledger: the full RRF state evaluation. -/
depends on (10)
Lean names referenced from this declaration's body.
-
State
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
RRF
in IndisputableMonolith.Foundation.Hamiltonian
decl_use
-
State
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
L
in IndisputableMonolith.Recognition
decl_use
-
L
in IndisputableMonolith.Recognition.Cycle3
decl_use
-
isClosed
in IndisputableMonolith.RRF.Core.Strain
decl_use
-
LedgerConstraint
in IndisputableMonolith.RRF.Core.Strain
decl_use
-
net
in IndisputableMonolith.RRF.Core.Strain
decl_use
-
net
in IndisputableMonolith.RRF.Foundation.Ledger
decl_use