VantageTriple
plain-language theorem explainer
VantageTriple packages three copies of a value of type α to index the inside, act, and outside perspectives on one underlying entity. RRF model builders cite it when they need to enforce that subjective, process, and objective descriptions coincide. The declaration is a bare structure with three fields and no proof obligations.
Claim. A VantageTriple over a type $α$ consists of three elements $x_∈, x_a, x_o ∈ α$ that represent the inside, active, and outside vantages on the same object.
background
The RRF core treats every phenomenon as admitting three vantages: inside (subjective/qualia), act (dynamic/process), and outside (objective/physics). These are not distinct objects but three views of one thing; consistency across them is required for existence to be actual. VantageTriple is the data structure that packages one value from each vantage so that later definitions can test or enforce equality.
proof idea
Direct structure definition introducing the three fields inside, act, and outside. No lemmas or tactics are invoked; the declaration itself supplies the type.
why it matters
It is the immediate parent of get, unified, and isUnified in the same module, and is instantiated in the trivial model via trivialVantageTriple. The structure therefore supplies the concrete representation needed for the RRF claim that all three vantages must agree. In the larger Recognition framework it operationalizes the requirement that inside, act, and outside descriptions coincide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.