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

CostAlgPlusHom

show as:
view Lean formalization →

Morphisms in the positive cost algebra category are parameterized by positive real exponents α satisfying the scaling α κ₂ = κ₁ on object parameters. Researchers formalizing order-preserving maps on cost families or building categorical models of recognition algebras cite this structure. The definition is direct, with extensionality and preservation properties obtained by case analysis on fields followed by simplification and application of power map lemmas.

claimA morphism from object $C_1$ to object $C_2$ consists of a real number $α > 0$ such that $α · κ_2 = κ_1$, where each $C_i$ is a positive-parameter cost family with parameter $κ_i > 0$.

background

The RecognitionCategory module defines the positive branch of cost algebras. Objects are structures CostAlgPlusObj carrying a positive real parameter κ together with the attached cost function given by costFamily κ. This selects the order-preserving branch of cost families; the negative branch is excluded because it reverses order. Upstream results from CostAlgebra supply J-automorphisms together with their multiplicativity and cost-preservation theorems, plus the initial object whose parameter is calibrated to 1.

proof idea

The structure is introduced by the three fields α, positivity of α, and the intertwining equation. The extensionality theorem proceeds by cases on the two morphisms and the equality hypothesis on α, followed by simplification. The map, positivity, multiplicativity, and cost-preservation theorems are one-line wrappers that invoke powerMap lemmas and the costFamily composition with power maps.

why it matters in Recognition Science

The structure supplies the morphisms for the CostAlg⁺ category that organizes order-preserving transformations of cost families. It directly supports the identity and composition operations that mirror J-automorphism composition, and it references the initial object with κ = 1 whose cost recovers the canonical J-cost. In the Recognition framework this algebraic layer precedes the lifting to full recognition categories and the forcing chain steps that fix J-uniqueness and the eight-tick octave.

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