IndisputableMonolith.RRF.Core.Vantage

   1import Mathlib.Data.Fintype.Card
   2
   3
   4/-!
   5# RRF Core: Vantage
   6
   7The three fundamental perspectives on the One Thing.
   8
   9In RRF, every phenomenon can be viewed from three vantages:
  10- **Inside**: The subjective/qualia view (what it feels like)
  11- **Act**: The dynamic/process view (what is happening)
  12- **Outside**: The objective/physics view (what is observed)
  13
  14These are not three different things, but three views of the same thing.
  15The key insight: all three must be consistent for existence to be actual.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace RRF.Core
  20
  21/-- The three fundamental vantages on reality.
  22
  23- `inside`: The subjective perspective (qualia, meaning, experience)
  24- `act`: The dynamic perspective (recognition, process, becoming)
  25- `outside`: The objective perspective (physics, measurement, observation)
  26-/
  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⟩
  38  complete := fun v => by cases v <;> decide
  39
  40/-- The number of vantages. -/
  41theorem card_vantage : Fintype.card Vantage = 3 := rfl
  42
  43/-- Every vantage has a complement pair. -/
  44def complements (v : Vantage) : Vantage × Vantage :=
  45  match v with
  46  | inside  => (act, outside)
  47  | act     => (inside, outside)
  48  | outside => (inside, act)
  49
  50/-- Cyclic successor (for the 3-phase rhythm). -/
  51def succ (v : Vantage) : Vantage :=
  52  match v with
  53  | inside  => act
  54  | act     => outside
  55  | outside => inside
  56
  57/-- Cyclic predecessor. -/
  58def pred (v : Vantage) : Vantage :=
  59  match v with
  60  | inside  => outside
  61  | act     => inside
  62  | outside => act
  63
  64theorem succ_pred_id (v : Vantage) : succ (pred v) = v := by
  65  cases v <;> rfl
  66
  67theorem pred_succ_id (v : Vantage) : pred (succ v) = v := by
  68  cases v <;> rfl
  69
  70/-- Three applications of succ returns to start. -/
  71theorem succ_succ_succ (v : Vantage) : succ (succ (succ v)) = v := by
  72  cases v <;> rfl
  73
  74end Vantage
  75
  76/-- A triple of values indexed by vantage.
  77    Used to express that X_inside, X_act, X_outside are the same underlying X. -/
  78structure VantageTriple (α : Type*) where
  79  inside  : α
  80  act     : α
  81  outside : α
  82
  83namespace VantageTriple
  84
  85/-- Project a value by vantage. -/
  86def get {α : Type*} (t : VantageTriple α) (v : Vantage) : α :=
  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. -/
  93def unified {α : Type*} (x : α) : VantageTriple α :=
  94  { inside := x, act := x, outside := x }
  95
  96/-- Predicate: the triple is unified (all equal). -/
  97def isUnified {α : Type*} [DecidableEq α] (t : VantageTriple α) : Prop :=
  98  t.inside = t.act ∧ t.act = t.outside
  99
 100theorem unified_is_unified {α : Type*} [DecidableEq α] (x : α) :
 101    isUnified (unified x) := ⟨rfl, rfl⟩
 102
 103end VantageTriple
 104
 105end RRF.Core
 106end IndisputableMonolith
 107