initial_morphism_exists

formal source

  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`. -/
 123theorem costFamily_unit (κ : ℝ) : costFamily κ 1 = 0 := by
 124  unfold costFamily
 125  simp
 126