structure definition def or abbrev

`MinimalLedger`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  75structure MinimalLedger (X : Type*) where
  76  /-- The charge of an element. -/
  77  charge : X → ℤ
  78  /-- Conservation: sum of charges is zero in any valid transaction. -/
  79  conserved : ∀ (txn : List X), (txn.map charge).sum = 0
  80
  81/-- Hypothesis class: MP forces ledger structure.
  82
  83This is a PHYSICAL HYPOTHESIS, not a mathematical theorem.
  84It captures the claim that recognition pairing forces conservation.
  85-/

depends on (15)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Hypothesis in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
forces in IndisputableMonolith.Foundation.MagnitudeOfMismatch decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
MP in IndisputableMonolith.Recognition decl_use
MP in IndisputableMonolith.RRF.Core.Recognition decl_use