trivialVantageTriple_unified
plain-language theorem explainer
The trivial model of the Recognition Recognition Field constructs a vantage triple on the unit state whose inside, act, and outside components coincide. Consistency checks for the RRF axiom bundle cite this result to confirm the unification predicate holds in the minimal case. The proof is a direct term application of the general lemma that the unified constructor always yields an isUnified triple.
Claim. In the trivial model, let $t$ be the vantage triple with components drawn from the unit state. Then $t.inside = t.act = t.outside$, i.e., the predicate isUnified holds for $t$.
background
The trivial model is the simplest structure satisfying the RRF axioms, with a single state (the unit type) and zero J-cost everywhere. A VantageTriple is a structure whose three fields (inside, act, outside) are required to represent the same underlying value when the unification predicate holds. The predicate isUnified is defined to hold exactly when those three fields are equal. This result depends on the general theorem that the unified constructor produces an isUnified triple for any element of the underlying type.
proof idea
The proof is a one-line term that applies the lemma unified_is_unified directly to the sole inhabitant of TrivialState. That lemma states that for any x the triple built by unified x satisfies isUnified by reflexivity on the three fields.
why it matters
This declaration verifies that the trivial model satisfies the isUnified condition on its vantage triple, thereby confirming one core RRF axiom in the minimal case. It supports the module's claim that the Recognition Recognition Field framework is internally consistent. No downstream uses are recorded, so the result functions as a self-contained consistency check rather than an input to further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.