structure definition def or abbrev

`PrimitiveCostHypotheses`

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

formal statement (Lean)

  53structure PrimitiveCostHypotheses (F : ℝ → ℝ) : Prop where
  54  reciprocal : IsReciprocalCost F
  55  normalized : IsNormalized F
  56  composition : SatisfiesCompositionLaw F
  57  calibrated : IsCalibrated F
  58  continuous : ContinuousOn F (Set.Ioi 0)
  59

used by (3)

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

primitive_to_uniqueness_aczel in IndisputableMonolith.Cost.AczelClassification decl_use
primitive_to_uniqueness_of_kernel in IndisputableMonolith.Cost.AczelClassification decl_use
PublicCostLayer in IndisputableMonolith.Foundation.DimensionalConstraints.CostLayer decl_use

depends on (11)

Lean names referenced from this declaration's body.

reciprocal in IndisputableMonolith.Algebra.CostAlgebra decl_use
IsCalibrated in IndisputableMonolith.Cost.FunctionalEquation decl_use
IsNormalized in IndisputableMonolith.Cost.FunctionalEquation decl_use
IsReciprocalCost in IndisputableMonolith.Cost.FunctionalEquation decl_use
SatisfiesCompositionLaw in IndisputableMonolith.Cost.FunctionalEquation decl_use
IsNormalized in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use
reciprocal in IndisputableMonolith.Foundation.LedgerForcing decl_use
normalized in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use