VantageEquiv
plain-language theorem explainer
VantageEquiv packages mutually inverse VantageFunctors between two vantage categories that preserve the strain functional J on states. Researchers formalizing the equivalence of physical, meaningful, and qualitative descriptions cite it to make the three-vantage claim precise. The declaration is a direct structure definition with four fields that enforce functor maps and state-level invertibility.
Claim. An equivalence between vantage categories $V_1$ and $V_2$ consists of a functor $F: V_1 → V_2$ and an inverse functor $G: V_2 → V_1$ such that $G(F(x)) = x$ and $F(G(y)) = y$ for all states $x, y$, where both functors satisfy $J_2(F(x)) = J_1(x)$ and likewise for $G$.
background
A VantageCategory is a category whose objects are states, whose morphisms are transitions, and which is equipped with a strain functional J that assigns a cost to each state. A VantageFunctor between two vantage categories maps states and transitions, preserves identities, and satisfies the strain-preservation equation $J_2(F(x)) = J_1(x)$ for every state $x$ (see the sibling definition VantageFunctor).
proof idea
This is a structure definition that directly assembles a pair of VantageFunctors together with the two inverse equations on their state maps. No lemmas or tactics are applied; the four fields encode the standard notion of categorical equivalence restricted to strain-preserving maps.
why it matters
VantageEquiv supplies the type used by equilibria_iso (equivalent vantages have isomorphic equilibria), hard_problem_dissolves (qualia are physics viewed from inside), and the placeholder vantages_equivalent theorem. It realizes the module claim that functors F: Outside → Act → Inside → Outside preserve J, thereby dissolving the explanatory gap as a category error.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.