identity
plain-language theorem explainer
The identity functor on any vantage category sends states and transitions to themselves while preserving the strain functional J. Researchers formalizing equivalence of physical, active, and qualia descriptions cite it as the base case for vantage functors. The definition constructs the functor structure directly by assigning the identity map to both objects and morphisms, then discharges the functoriality and preservation axioms by reflexivity.
Claim. For any vantage category $V$ (a category whose objects are states, morphisms are transitions, and whose strain functional $J$ assigns a cost to each state), the identity functor $id_V : V → V$ is the structure with $map_state(x) = x$, $map_trans(f) = f$, $map_id$ the reflexivity proof that the image of the identity transition is the identity, and $preserves_strain$ the reflexivity proof that $J$ is unchanged under the identity map.
background
A vantage category consists of a type of states, a type of transitions between states, an identity transition for each state, a composition operation on transitions, and a strain functional $J$ that assigns a real-valued cost to each state. A vantage functor between two such categories is a map on states and on transitions that sends identities to identities and preserves the value of $J$ on every state. The module establishes that the three vantages (Inside, Act, Outside) are formally equivalent by exhibiting functors that preserve strain, thereby making precise the claim that physics, meaning, and qualia are three views of one structure.
proof idea
Direct definition of the VantageFunctor structure. The map on states and the map on transitions are both set to the identity function. The two required axioms (preservation of identity transitions and preservation of strain) are witnessed by the reflexivity tactic rfl applied to the appropriate expressions.
why it matters
This definition supplies the identity morphism in the category of vantage categories and is invoked by downstream constructions including totalEnergy in the Hamiltonian module, the numerical band theorem for J(φ) in VisualBeauty, the CostAlgebraData structure, costCompose_factored, CostMorphism, defectDist, and equivZModTwo. It fills the trivial case of the vantage-equivalence claim stated in the module documentation, supporting the dissolution of the hard problem by showing that qualia are physics viewed from the Inside vantage. It sits at the base of the 40 uses that propagate the strain-preserving functoriality into algebraic and dynamical statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.