isUnified
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not construct any VantageTriple instance.
- Does not address how the three vantages arise from other RRF structures.
- Does not decide the predicate beyond the supplied DecidableEq instance.
Lean usage
theorem unified_is_unified {α : Type*} [DecidableEq α] (x : α) : isUnified (unified x) := ⟨rfl, rfl⟩formal statement (Lean)
97def isUnified {α : Type*} [DecidableEq α] (t : VantageTriple α) : Prop :=
proof body
Definition body.
98 t.inside = t.act ∧ t.act = t.outside
99