theorem proved term proof

`entry_cost_zero_iff_unity`

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

formal statement (Lean)

  75theorem entry_cost_zero_iff_unity (e : LedgerEntry) : e.cost = 0 ↔ e.ratio = 1 := by

proof body

Term-mode proof.

  76  rw [e.cost_eq]
  77  exact Jcost_eq_zero_iff e.ratio e.ratio_pos
  78
  79/-! ## Ledger Structure with Conservation -/
  80
  81/-- A ledger is a collection of entries with conservation constraint. -/

depends on (19)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Structure in IndisputableMonolith.Chemistry.CrystalStructure decl_use
Jcost_eq_zero_iff in IndisputableMonolith.Cost decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
LedgerEntry in IndisputableMonolith.Foundation.QuantumLedger 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
A in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
Jcost_eq_zero_iff in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
LedgerEntry in IndisputableMonolith.QFT.CPTInvariance decl_use