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)
59theorem add_balanced (t₁ t₂ : Transaction) :
60 (add t₁ t₂).debit + (add t₁ t₂).credit = 0 := (add t₁ t₂).balanced
proof body
Term-mode proof.
61
62end Transaction
63
64/-! ## Full Ledger -/
65
66/-- A ledger: a sequence of transactions that globally balance. -/
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
balanced
in IndisputableMonolith.Foundation.LedgerForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
that
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
Transaction
in IndisputableMonolith.RRF.Foundation.Ledger
decl_use