`public_cost_layer`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.DimensionalConstraints.CostLayer
domain: Foundation
line: 52 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.DimensionalConstraints.CostLayer on GitHub at line 52.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  49      C < Foundation.LawOfExistence.defect x
  50
  51/-- The public cost layer is available in the current public framework. -/
  52theorem public_cost_layer : PublicCostLayer := by
  53  refine
  54    { unique_on_pos := ?_
  55      log_closed_form := Cost.Jlog_as_cosh
  56      normalized := Cost.Jcost_unit0
  57      reciprocal := ?_
  58      nonnegative := ?_
  59      zero_iff_one := ?_
  60      null_barrier := Foundation.LawOfExistence.nothing_cannot_exist }
  61  · intro F hF hKernel x hx
  62    exact Cost.FunctionalEquation.primitive_to_uniqueness_of_kernel F hF hKernel x hx
  63  · intro x hx
  64    exact Cost.Jcost_symm hx
  65  · intro x hx
  66    exact Cost.Jcost_nonneg hx
  67  · intro x hx
  68    exact Cost.Jcost_eq_zero_iff x hx
  69
  70end CostLayer
  71end DimensionalConstraints
  72end Foundation
  73end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.