recAlg_id_right

formal source

  80  simp [recAlg_comp, recAlg_id, CostMorphism.comp, CostMorphism.id, Function.comp]
  81
  82/-- **PROVED: Identity is right-neutral (on underlying maps).** -/
  83theorem recAlg_id_right {C₁ C₂ : RecAlgObj} (f : RecAlgHom C₁ C₂) :
  84    (recAlg_comp f (recAlg_id C₁)).map = f.map := by
  85  ext x
  86  simp [recAlg_comp, recAlg_id, CostMorphism.comp, CostMorphism.id, Function.comp]
  87
  88/-! ## §2. The Initial Object -/
  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 : ℝ) : ℝ :=