pith. machine review for the scientific record. sign in

IndisputableMonolith.RRF.Core

IndisputableMonolith/RRF/Core.lean · 38 lines · 0 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: ready · generated 2026-05-15 09:13:05.449067+00:00

   1import IndisputableMonolith.RRF.Core.DisplayChannel
   2import IndisputableMonolith.RRF.Core.Glossary
   3import IndisputableMonolith.RRF.Core.Octave
   4import IndisputableMonolith.RRF.Core.Recognition
   5import IndisputableMonolith.RRF.Core.Strain
   6import IndisputableMonolith.RRF.Core.Vantage
   7
   8
   9/-!
  10# RRF Core
  11
  12Umbrella file for RRF Core definitions.
  13
  14This module re-exports all core RRF definitions. It contains only definitional
  15content—no physical constants, no hypotheses, no heavy mathlib.
  16
  17## Contents
  18
  19- `Vantage`: The three perspectives {inside, act, outside}
  20- `Strain`: Strain functionals and ledger constraints
  21- `DisplayChannel`: Observation channels and quality equivalence
  22- `Octave`: Scales of manifestation
  23- `Recognition`: Re-exports from existing Recognition module
  24- `Glossary`: Canonical terminology and type aliases
  25-/
  26
  27namespace IndisputableMonolith
  28namespace RRF
  29
  30/-!
  31## RRF Core Status
  32
  33RRF Core is purely definitional and foundational.
  34-/
  35
  36end RRF
  37end IndisputableMonolith
  38

source mirrored from github.com/jonwashburn/shape-of-logic