IndisputableMonolith.RRF.Core.Glossary

   1import IndisputableMonolith.RRF.Core.DisplayChannel
   2import IndisputableMonolith.RRF.Core.Octave
   3import IndisputableMonolith.RRF.Core.Strain
   4import IndisputableMonolith.RRF.Core.Vantage
   5
   6/-!
   7# RRF Core: Glossary
   8
   9Official symbols and canonical terminology for the Reality Recognition Framework.
  10
  11This file serves as the single source of truth for RRF vocabulary.
  12All other modules should use these names consistently.
  13
  14## Key Symbols
  15
  16| Symbol | Lean Name | Meaning |
  17|--------|-----------|---------|
  18| J | `StrainFunctional.J` | Strain/cost functional |
  19| V | `Vantage` | {inside, act, outside} |
  20| R | `Recognize` | Recognition pairing |
  21| O | `Octave` | A scale of manifestation |
  22| C | `DisplayChannel` | Observation channel |
  23| L | `LedgerConstraint` | Double-entry constraint |
  24| φ | (Hypotheses only) | Golden ratio scaling |
  25| τ | (Hypotheses only) | Base timescale |
  26
  27## Terminology
  28
  29- **Recognition**: The fundamental act by which distinctions become actual
  30- **Vantage**: One of three perspectives {inside, act, outside}
  31- **Strain**: Deviation from balance (J → 0 is the law)
  32- **Octave**: A scale/level of manifestation
  33- **Display Channel**: A way of observing states
  34- **Ledger**: Conservation accounting (debit = credit)
  35-/
  36
  37
  38namespace IndisputableMonolith
  39namespace RRF.Core
  40
  41/-! ## Canonical Type Aliases -/
  42
  43/-- J: The strain/cost of a state. -/
  44abbrev J {State : Type*} (S : StrainFunctional State) := S.J
  45
  46/-- V: The vantage type. -/
  47abbrev V := Vantage
  48
  49/-- isBalanced: Zero-strain predicate. -/
  50abbrev isBalanced {State : Type*} := StrainFunctional.isBalanced (State := State)
  51
  52/-- isMinimizer: Strain minimizer predicate. -/
  53abbrev isMinimizer {State : Type*} := StrainFunctional.isMinimizer (State := State)
  54
  55/-! ## Key Properties (as propositions) -/
  56
  57/-- The "J → 0" law: strain minimization is the fundamental drive. -/
  58def JMinimizationLaw {State : Type*} (S : StrainFunctional State) : Prop :=
  59  ∃ x, S.isBalanced x
  60
  61/-- Ledger closure: the double-entry constraint holds. -/
  62def LedgerClosure {State : Type*} (L : LedgerConstraint State) (x : State) : Prop :=
  63  L.isClosed x
  64
  65/-- Channel equivalence: two channels induce the same state ordering. -/
  66abbrev ChannelEquiv {State Obs₁ Obs₂ : Type*} :=
  67  QualityEquiv (State := State) (Obs₁ := Obs₁) (Obs₂ := Obs₂)
  68
  69/-! ## RRF Consistency Conditions
  70
  71For a state to be "real" (recognized), it must satisfy:
  721. Strain minimization (or at least local minimum)
  732. Ledger closure
  743. Consistent observation across channels
  75-/
  76
  77/-- A state is RRF-consistent if it has low strain and closed ledger. -/
  78def isConsistent {State : Type*}
  79    (SL : StrainLedger State) (x : State) : Prop :=
  80  SL.strain.isBalanced x ∧ SL.ledger.isClosed x
  81
  82/-- The set of RRF-consistent states. -/
  83def consistentStates {State : Type*} (SL : StrainLedger State) : Set State :=
  84  { x | isConsistent SL x }
  85
  86end RRF.Core
  87end IndisputableMonolith
  88