Vantage
Vantage enumerates the three irreducible perspectives on any phenomenon in Recognition Science: subjective experience, dynamic process, and objective measurement. RRF core developers cite this when decomposing statements into vantage triples that must remain consistent. The declaration is an inductive enumeration whose Fintype instance is discharged by exhaustive case analysis on the three constructors.
claimLet $V$ be the type whose elements are the subjective perspective $I$, the dynamic perspective $A$, and the objective perspective $O$.
background
The RRF module treats every phenomenon as a single underlying reality viewed from three vantages. Inside captures qualia and subjective experience. Act captures recognition and becoming. Outside captures physics and measurement. The module doc states that all three views must be consistent for existence to be actual. The declaration depends on Fintype from Mathlib to record that exactly three elements exist.
proof idea
The inductive definition introduces three constructors. The Fintype instance lists the three elements explicitly and discharges completeness by case analysis on each constructor, using the decide tactic.
why it matters in Recognition Science
This supplies the vantage type referenced by Glossary.V, card_vantage, complements, get, pred, succ, and the identity theorems pred_succ_id and succ_pred_id. It realizes the three-perspective requirement stated in the module doc. The complements definition downstream shows each vantage pairs with the remaining two, closing the finite structure needed for later RRF constructions.
scope and limits
- Does not assign numerical values or metrics to any vantage.
- Does not prove mutual consistency of the three perspectives.
- Does not extend the type beyond exactly three elements.
- Does not connect the vantages to specific physical constants or equations.
formal statement (Lean)
27inductive Vantage : Type where
28 | inside : Vantage
29 | act : Vantage
30 | outside : Vantage
31 deriving DecidableEq, Repr, Inhabited
32
33namespace Vantage
34
35/-- Vantage is finite with exactly 3 elements. -/
36instance : Fintype Vantage where
37 elems := ⟨[inside, act, outside], by decide⟩
proof body
Definition body.
38 complete := fun v => by cases v <;> decide
39
40/-- The number of vantages. -/