def definition def or abbrev

`mkEntry`

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

formal statement (Lean)

  60noncomputable def mkEntry (id : ℕ) (r : ℝ) (hr : 0 < r) (p : Fin 8) : LedgerEntry := {

proof body

Definition body.

  61  id := id
  62  ratio := r
  63  ratio_pos := hr
  64  cost := Jcost r
  65  phase := p
  66  cost_eq := rfl
  67}
  68
  69/-- The J-cost of an entry is non-negative. -/

depends on (18)

Lean names referenced from this declaration's body.

id in IndisputableMonolith.Algebra.CostAlgebra decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
id in IndisputableMonolith.Foundation.ArithmeticOf decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
phase in IndisputableMonolith.Foundation.EightTick 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
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use
LedgerEntry in IndisputableMonolith.QFT.CPTInvariance decl_use
id in IndisputableMonolith.RRF.Core.Octave decl_use