net — Recognition explainer

formal statement (Lean)

 107def net (L : Ledger) : ℤ := L.total_debit + L.total_credit

proof body

Definition body.

 108
 109/-- Ledger net is always zero. -/

used by (36)

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

GradedLedger in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
OctaveLoop in IndisputableMonolith.Applied.CoherenceTechnology decl_use
rs_pattern in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
allConditionsNeeded in IndisputableMonolith.Cosmology.MatterAntimatter decl_use
cproj_from_J_second_deriv in IndisputableMonolith.CPM.LawOfExistence decl_use
defect_eq_ortho_of_subspace_case in IndisputableMonolith.CPM.LawOfExistence decl_use
knet_from_cone_projection in IndisputableMonolith.CPM.LawOfExistence decl_use
just_no_debt in IndisputableMonolith.Ethics.MoralDebt decl_use
empty_ledger_cost in IndisputableMonolith.Foundation.LedgerForcing decl_use
flow_contribution_reciprocal in IndisputableMonolith.Foundation.LedgerForcing decl_use
ledger_balanced in IndisputableMonolith.Foundation.LedgerForcing decl_use
paired_log_sum_zero in IndisputableMonolith.Foundation.LedgerForcing decl_use
loops_eq_face_pairs_D3 in IndisputableMonolith.Foundation.WindingCharges decl_use
c_coercive_approx in IndisputableMonolith.Gravity.CoerciveProjection decl_use
CoarseGrainingStableClass in IndisputableMonolith.Mathematics.HodgeConjecture decl_use
globally_minimal_gives_cycle in IndisputableMonolith.Mathematics.HodgeHarmonicForms decl_use
finiteEulerLedger_balanced in IndisputableMonolith.NumberTheory.ConcreteEulerLedger decl_use
sensorEulerLedger_balanced in IndisputableMonolith.NumberTheory.ConcreteEulerLedger decl_use
sensorEulerLedger_cost_formula in IndisputableMonolith.NumberTheory.ConcreteEulerLedger decl_use
zeroWindingData in IndisputableMonolith.NumberTheory.ContourWinding decl_use
DirectedEulerLedgerSystem in IndisputableMonolith.NumberTheory.DirectedEulerLedger decl_use
SampledRing in IndisputableMonolith.NumberTheory.SampledTrace decl_use
canonicalTrajectory in IndisputableMonolith.Papers.GCIC.DiscreteGauge decl_use
ValidTrajectory in IndisputableMonolith.Papers.GCIC.DiscreteGauge decl_use
rs_lensing_correction_bounded in IndisputableMonolith.Relativity.ILG.ClusterLensing decl_use
RecogLedger in IndisputableMonolith.RRF.Core.Recognition decl_use
closed_iff_net_zero in IndisputableMonolith.RRF.Core.Strain decl_use
isClosed in IndisputableMonolith.RRF.Core.Strain decl_use
net in IndisputableMonolith.RRF.Core.Strain decl_use
append in IndisputableMonolith.RRF.Foundation.Ledger decl_use

… and 6 more

depends on (7)

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
net in IndisputableMonolith.RRF.Core.Strain decl_use