get
plain-language theorem explainer
The get definition projects one component from a VantageTriple according to a chosen vantage. Researchers modeling unified phenomena in Recognition Science cite it when accessing consistent subjective, dynamic, or objective values from the same underlying entity. The implementation is a direct case split on the vantage constructor that selects the matching field.
Claim. For a triple $t = (t_0, t_1, t_2)$ indexed by the three vantages and a vantage $v$, the projection returns the component of $t$ at $v$: $t_0$ when $v$ is the inside vantage, $t_1$ when $v$ is the act vantage, and $t_2$ when $v$ is the outside vantage.
background
The RRF core module treats every phenomenon as three consistent views of one entity: the inside vantage captures subjective qualia and experience, the act vantage captures dynamic process and recognition, and the outside vantage captures objective measurement and physics. The VantageTriple structure packages three values of identical type α, one per vantage, to record that they describe the same underlying object. The Vantage inductive type enumerates exactly these three constructors and carries decidable equality.
proof idea
The definition is a one-line wrapper that performs case analysis on the vantage argument. It returns the inside field when the vantage is inside, the act field when the vantage is act, and the outside field when the vantage is outside.
why it matters
This accessor supplies the uniform projection required by the three-vantage consistency principle stated in the module. It is invoked downstream in stellar mass-to-light calculations, noble-gas shell closures, SAT clause encoding, and cellular-automaton backpropagation. The construction directly supports the RRF requirement that inside, act, and outside representations remain identical for actual existence, linking to the broader forcing chain where D = 3 and the phi-ladder organize mass and energy scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.