pith. machine review for the scientific record. sign in
def definition def or abbrev high

get

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  86def get {α : Type*} (t : VantageTriple α) (v : Vantage) : α :=

proof body

Definition body.

  87  match v with
  88  | Vantage.inside  => t.inside
  89  | Vantage.act     => t.act
  90  | Vantage.outside => t.outside
  91
  92/-- A unified triple: all three vantages see the same value. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (11)

Lean names referenced from this declaration's body.