insideVantage
plain-language theorem explainer
The inside vantage definition instantiates the VantageCategory structure to model qualia as experiences and sensations with trivial state space and zero cost. Researchers formalizing the equivalence of physics and consciousness under the Recognition framework cite this when constructing the three-vantage model. The construction is a direct record instantiation of the category axioms with placeholder data.
Claim. Let $C_ {inside}$ be the category whose objects form the singleton set, whose morphisms between any pair of objects form the singleton set, whose identity and composition maps send every pair to the unique element of that singleton, and whose strain functional $J$ is the constant zero map.
background
A VantageCategory consists of a type of states, a type of transitions between states, identity and composition operations that satisfy the category axioms, and a strain functional $J$ that assigns a cost to each state. The module sets the three vantages (Outside for physics, Act for meaning, Inside for qualia) as formally equivalent via functors that preserve $J$, which expresses that physics, meaning, and qualia are three views of one structure. Upstream results supply the algebraic composition and identity operations on cost automorphisms that ensure $J$ behaves consistently under these maps.
proof idea
The definition constructs the VantageCategory record directly by assigning the unit type to states and to transitions, the constant unit element to identities and compositions, and the zero function to the strain $J$. It applies the structure constructor with no additional lemmas or tactics.
why it matters
This supplies the concrete Inside instance required by the vantage equivalence theorem and the hard problem dissolution theorem in the same module. It advances the module claim that the hard problem dissolves because qualia are physics viewed from inside rather than caused by it. The definition touches the open question of constructing non-trivial functors between the vantages that preserve the strain functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.