pith. machine review for the scientific record. sign in
structure definition def or abbrev high

CostAlgPlusHom

show as:
view Lean formalization →

CostAlgPlusHom structures morphisms in the CostAlg⁺ category as positive real exponents α satisfying the scaling α κ₂ = κ₁ between object parameters. Recognition Science algebraists cite this when assembling the category of cost families from the J-cost. The definition encodes the three fields directly without further reduction.

claimA morphism from object $C_1$ to object $C_2$ in the category of positive-parameter cost families consists of a real number $α > 0$ satisfying $α κ_2 = κ_1$, where $κ_i$ is the positive parameter of $C_i$.

background

Objects of CostAlg⁺ are structures CostAlgPlusObj carrying a positive real parameter κ together with a positivity witness; each object is equipped with the cost function costFamily κ. Morphisms are required to be order-preserving, which excludes the negative branch of the cost families. The construction appears in the RecognitionCategory module after imports of CostAlgebra (supplying J-automorphisms and their multiplicative and cost-preservation properties) and PhiRing.

proof idea

The declaration is a plain structure definition that directly records the three fields: the exponent α, the proof α > 0, and the equality α ⋅ C₂.κ = C₁.κ. No lemmas are invoked inside the structure; the subsequent extensionality theorem applies cases on the two morphisms and simp to conclude equality from matching α values.

why it matters in Recognition Science

CostAlgPlusHom supplies the hom-sets needed to turn the collection of CostAlgPlusObj into a category, with identity and composition defined immediately afterward. It implements the paper's order-preserving morphism classification for cost families. In the Recognition Science framework the construction supports the initial object with κ = 1 and the cost-preservation theorems that feed into the larger Recognition Category.

scope and limits

formal statement (Lean)

 332structure CostAlgPlusHom (C₁ C₂ : CostAlgPlusObj) where
 333  α : ℝ
 334  α_pos : 0 < α
 335  intertwines : α * C₂.κ = C₁.κ
 336
 337/-- Extensionality for `CostAlg⁺` morphisms: the exponent `α` determines the
 338    morphism completely. -/
 339@[ext] theorem CostAlgPlusHom.ext
 340    {C₁ C₂ : CostAlgPlusObj} {f g : CostAlgPlusHom C₁ C₂}
 341    (hα : f.α = g.α) : f = g := by

proof body

Definition body.

 342  cases f
 343  cases g
 344  cases hα
 345  simp
 346
 347/-- The underlying positive-reals map of a `CostAlg⁺` morphism. -/
 348noncomputable def CostAlgPlusHom.map {C₁ C₂ : CostAlgPlusObj}
 349    (f : CostAlgPlusHom C₁ C₂) (x : ℝ) : ℝ :=
 350  powerMap f.α x
 351
 352/-- A `CostAlg⁺` morphism maps positive reals to positive reals. -/
 353theorem CostAlgPlusHom.map_pos {C₁ C₂ : CostAlgPlusObj}
 354    (f : CostAlgPlusHom C₁ C₂) {x : ℝ} (hx : 0 < x) :
 355    0 < f.map x :=
 356  powerMap_pos f.α hx
 357
 358/-- A `CostAlg⁺` morphism is multiplicative. -/
 359theorem CostAlgPlusHom.map_mul {C₁ C₂ : CostAlgPlusObj}
 360    (f : CostAlgPlusHom C₁ C₂) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
 361    f.map (x * y) = f.map x * f.map y :=
 362  powerMap_mul f.α hx hy
 363
 364/-- A `CostAlg⁺` morphism preserves the explicit cost family. -/
 365theorem CostAlgPlusHom.preserves_cost {C₁ C₂ : CostAlgPlusObj}
 366    (f : CostAlgPlusHom C₁ C₂) {x : ℝ} (hx : 0 < x) :
 367    C₂.cost (f.map x) = C₁.cost x := by
 368  simpa [CostAlgPlusObj.cost, f.intertwines] using
 369    (costFamily_comp_powerMap C₂.κ f.α hx)
 370
 371/-- Identity morphism in `CostAlg⁺`. -/
 372def CostAlgPlusHom.id (C : CostAlgPlusObj) : CostAlgPlusHom C C where
 373  α := 1
 374  α_pos := by norm_num
 375  intertwines := by ring
 376
 377/-- Composition of `CostAlg⁺` morphisms. -/
 378def CostAlgPlusHom.comp {C₁ C₂ C₃ : CostAlgPlusObj}
 379    (g : CostAlgPlusHom C₂ C₃) (f : CostAlgPlusHom C₁ C₂) :
 380    CostAlgPlusHom C₁ C₃ where
 381  α := f.α * g.α
 382  α_pos := mul_pos f.α_pos g.α_pos
 383  intertwines := by
 384    calc
 385      (f.α * g.α) * C₃.κ = f.α * (g.α * C₃.κ) := by ring
 386      _ = f.α * C₂.κ := by rw [g.intertwines]
 387      _ = C₁.κ := by rw [f.intertwines]
 388
 389/-- The canonical object of `CostAlg⁺` is the calibrated `κ = 1` cost. -/

depends on (40)

Lean names referenced from this declaration's body.

… and 10 more