unified
plain-language theorem explainer
The definition constructs a VantageTriple in which the inside, act, and outside components coincide on a single input value. Workers on the three-perspective model in Recognition Science cite it to establish the base case of vantage consistency before deriving constants or mass-to-light ratios. The construction is a direct record literal that assigns the input to each field.
Claim. For any type $A$ and element $x$ of $A$, the map sends $x$ to the triple whose inside, act, and outside entries are each equal to $x$.
background
The RRF.Core.Vantage module treats every phenomenon as three consistent views of one underlying item: inside (subjective qualia), act (dynamic process), and outside (objective observation). VantageTriple is the structure that packages these three fields of common type $A$. The supplied definition supplies the special case in which the three fields are identical, which the module doc calls the condition for actual existence.
proof idea
Direct record construction: the body is the literal VantageTriple with inside, act, and outside each set to the parameter $x$. No lemmas or tactics are invoked.
why it matters
This supplies the base consistency object used by ml_derivation_complete and C006_certificate in the downstream modules. It anchors the zero-parameter status claim by letting derivations proceed from a single value rather than external inputs. The construction directly implements the module's statement that the three vantages must agree for existence to be actual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.