Category of Rational Action Agents

Category of RationalAction agents (fixed S, A types) with score-proportionality as morphisms.

If agent₂'s scores are k times agent₁'s scores (for k > 0), Luce scale invariance (RationalAction.scaleBy_policy) guarantees identical policies. This makes the category a groupoid: every morphism is invertible (with inverse constant 1/k).

The key downstream consumer is RSA/Structural/ModelMorphism.lean, where proportional S1 scores imply identical L1 posteriors.

structure Core.Categorical.AgentObj (S : Type u_1) (A : Type u_2) [Fintype A] : Type (max u_1 u_2)

Bundled rational action agent: an object in the agent category.

• agent : RationalAction S A

  The underlying rational action agent.

structure Core.Categorical.AgentMor {S : Type u_1} {A : Type u_2} [Fintype A] (ra₁ ra₂ : AgentObj S A) : Type

A morphism between agents: a score proportionality witness.

AgentMor ra₁ ra₂ asserts that ra₂'s scores are k times ra₁'s scores for some positive constant k. By Luce invariance, this guarantees that both agents have identical policies.

• k : ℝ

  The proportionality constant.

• k_pos : 0 < self.k

  The constant is positive.

• proportional (s : S) (a : A) : ra₂.agent.score s a = self.k * ra₁.agent.score s a

  Scores are proportional: score₂(s,a) = k · score₁(s,a).

theorem Core.Categorical.AgentMor.ext {S : Type u_1} {A : Type u_2} [Fintype A] {ra₁ ra₂ : AgentObj S A} {m₁ m₂ : AgentMor ra₁ ra₂} (h : m₁.k = m₂.k) : m₁ = m₂

theorem Core.Categorical.AgentMor.ext_iff {S : Type u_1} {A : Type u_2} [Fintype A] {ra₁ ra₂ : AgentObj S A} {m₁ m₂ : AgentMor ra₁ ra₂} : m₁ = m₂ ↔ m₁.k = m₂.k

def Core.Categorical.AgentMor.id {S : Type u_1} {A : Type u_2} [Fintype A] (ra : AgentObj S A) : AgentMor ra ra

Identity morphism: scores are 1 × themselves.

Equations

• Core.Categorical.AgentMor.id ra = { k := 1, k_pos := Core.Categorical.AgentMor.id._proof_1, proportional := ⋯ }

def Core.Categorical.AgentMor.comp {S : Type u_1} {A : Type u_2} [Fintype A] {ra₁ ra₂ ra₃ : AgentObj S A} (f : AgentMor ra₁ ra₂) (g : AgentMor ra₂ ra₃) : AgentMor ra₁ ra₃

Composition: if score₂ = k₁ · score₁ and score₃ = k₂ · score₂, then score₃ = (k₂ · k₁) · score₁.

Equations

• f.comp g = { k := g.k * f.k, k_pos := ⋯, proportional := ⋯ }

noncomputable def Core.Categorical.AgentMor.inv {S : Type u_1} {A : Type u_2} [Fintype A] {ra₁ ra₂ : AgentObj S A} (f : AgentMor ra₁ ra₂) : AgentMor ra₂ ra₁

Inverse morphism: if score₂ = k · score₁, then score₁ = (1/k) · score₂.

Equations

• f.inv = { k := f.k⁻¹, k_pos := ⋯, proportional := ⋯ }

instance Core.Categorical.instCategoryAgentObj {S : Type u_1} {A : Type u_2} [Fintype A] : CategoryTheory.Category.{0, max u_2 u_1} (AgentObj S A)

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Categorical.AgentMor.preserves_policy {S : Type u_1} {A : Type u_2} [Fintype A] {ra₁ ra₂ : AgentObj S A} (m : AgentMor ra₁ ra₂) (s : S) (a : A) : ra₁.agent.policy s a = ra₂.agent.policy s a

Luce invariance: a morphism preserves the policy.

If scores are proportional, both agents assign the same probability to every action in every state.

theorem Core.Categorical.AgentMor.comp_preserves_policy {S : Type u_1} {A : Type u_2} [Fintype A] {ra₁ ra₂ ra₃ : AgentObj S A} (f : AgentMor ra₁ ra₂) (g : AgentMor ra₂ ra₃) (s : S) (a : A) : ra₁.agent.policy s a = ra₃.agent.policy s a

Composition of morphisms preserves policy preservation.