isUnified
plain-language theorem explainer
The isUnified predicate asserts that the three components of a VantageTriple are identical. Researchers working on the RRF framework cite it when verifying consistency across subjective, dynamic, and objective views of a phenomenon. The definition reduces directly to checking equality of the inside, act, and outside fields via conjunction.
Claim. For a VantageTriple $t$ with components $t_inside$, $t_act$, $t_outside$, the predicate holds precisely when $t_inside = t_act$ and $t_act = t_outside$.
background
In the RRF framework every phenomenon admits three vantages: inside (subjective/qualia), act (dynamic/process), and outside (objective/physics). The VantageTriple structure packages one value for each vantage to express that they represent the same underlying entity. The module states that all three must be consistent for existence to be actual.
proof idea
The definition is given directly as the conjunction of two field equalities on the input VantageTriple.
why it matters
This predicate is invoked by unified_is_unified to show the canonical constructor yields a unified triple and by trivialVantageTriple_unified in the Trivial model. It supports the module claim that consistency across the three vantages is required for actual existence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.