comp
plain-language theorem explainer
Composition of vantage functors is defined by chaining state maps and transition maps of two strain-preserving functors between vantage categories. Researchers formalizing the equivalence of Inside, Act, and Outside perspectives in Recognition Science cite this when building composite mappings. The definition proceeds by direct record construction of the functor fields using function composition and simp to discharge the identity and strain axioms.
Claim. Given vantage categories $V_1, V_2, V_3$ and functors $G: V_2 → V_3$, $F: V_1 → V_2$ that preserve the strain functional $J$, the composite $G ∘ F: V_1 → V_3$ is the functor whose state map is $G ∘ F$, whose transition map is $G ∘ F$, and which preserves identities and strain values by construction.
background
A VantageCategory is a structure whose objects are states, whose morphisms are transitions equipped with identity and composition operations, and whose strain functional J assigns a cost to each state. A VantageFunctor between two vantage categories supplies a state map and a transition map that preserve identities and send states of equal J-cost to states of equal J-cost. The module sets the three vantages (Inside, Act, Outside) as formally equivalent categories linked by such functors, making precise the claim that physics, meaning, and qualia are three views of one structure. Upstream composition operations on J-automorphisms and on homomorphisms supply the algebraic pattern used here.
proof idea
The definition is a direct record construction: the state map is the ordinary function composition of the two state maps, and the transition map is the pointwise composition of the two transition maps. The identity-preservation field is obtained by applying simp to the identity fields of G and F; the strain-preservation field is obtained by applying simp to the strain-preservation fields of G and F.
why it matters
This definition supplies the composition operation required to chain vantage functors, which is invoked in downstream results such as the convexity theorem for the J-action and the energy-conservation theorem for Newtonian trajectories. It completes the categorical infrastructure that realizes the module claim of three equivalent vantages linked by strain-preserving functors. The construction mirrors the composition law already present in the CostAlgebra for J-automorphisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.