  89
  90/-- The **canonical cost algebra** J is the initial object in RecAlg.
  91    For any calibrated cost algebra C, there is a unique morphism J → C. -/
  92noncomputable def initialObject : RecAlgObj := canonicalCostAlgebra
  93
  94/-- From the initial object to any calibrated object,
  95    there exists a morphism (the identity-on-ℝ₊ map, when `C.cost = J`). -/
  96noncomputable def initial_morphism_exists :
  97    ∀ C : RecAlgObj, C.cost = J → RecAlgHom initialObject C := by
  98  intro C hC
  99  exact {
 100    map := fun x => x
 101    pos := fun _ h => h
 102    multiplicative := fun _ _ _ _ => rfl
 103    preserves_cost := fun x hx => by
 104      simpa [initialObject, canonicalCostAlgebra] using congrArg (fun f => f x) hC
 105  }
 106
 107/-! ## §3. The Paper-Facing Category `CostAlg⁺` -/
 108
 109/-- The explicit one-parameter family `F_κ(x) = ½(x^κ + x^{-κ}) - 1`
 110    appearing in the broad cost category. On `ℝ_{>0}` this is the full
 111    continuous solution family to the calibrated d'Alembert law before
 112    imposing `κ = 1`. -/
 113noncomputable def costFamily (κ : ℝ) (x : ℝ) : ℝ :=
 114  (x ^ κ + x ^ (-κ)) / 2 - 1
 115
 116/-- The canonical `κ = 1` family recovers the J-cost on positive reals. -/
 117theorem costFamily_one_eq_J {x : ℝ} (hx : 0 < x) : costFamily 1 x = J x := by
 118  unfold costFamily CostAlgebra.J
 119  rw [Real.rpow_one, Real.rpow_neg (le_of_lt hx), Real.rpow_one]
 120  simp [IndisputableMonolith.Cost.Jcost]
 121
 122/-- The family is normalized at `x = 1`. -/

papers checked against this theorem

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