outsideVantage
plain-language theorem explainer
The outsideVantage definition supplies the placeholder category for the Outside vantage, representing physics via geometry and observables with trivial states and zero strain cost. Researchers working on RRF vantage equivalence or hard-problem dissolution cite this structure when building the functors that identify the three views. The definition proceeds by direct assignment of the VantageCategory fields to unit types and the constant-zero J functional.
Claim. The Outside vantage is the category whose states are the unit type, whose transitions are the constant unit type, whose identity and composition maps return the unit element, and whose strain functional satisfies $J(x)=0$ for every state $x$.
background
The RRF Foundation module formalizes three equivalent vantages—Outside (physics: geometry, energy, observables), Act (meaning), and Inside (qualia)—as categories whose morphisms preserve the strain functional J. A VantageCategory is a structure containing a state type, a transition type family, identity and composition operations, and a strain record whose J field assigns a cost to each state. The supplied definition instantiates the Outside vantage as a trivial instance of this structure, consistent with the module claim that functors exist between the three views that preserve J.
proof idea
Direct definition that populates every field of the VantageCategory structure: State is set to Unit, Trans to the constant Unit type, id and comp to the unit element, and strain.J to the zero function. No lemmas or tactics are invoked; the construction is a one-line scaffolding assignment.
why it matters
This definition supplies the concrete Outside vantage required by the downstream vantages_equivalent theorem, which asserts nonempty VantageEquiv instances among outsideVantage, actVantage, and insideVantage. It is the physics-side input to hard_problem_dissolves, whose statement is that an equivalence implies qualia are physics viewed from Inside rather than caused by it. In the Recognition Science setting the construction realizes the three-view claim that physics, meaning, and qualia are formally identical under J-preserving functors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.