IndisputableMonolith.RRF.Core
IndisputableMonolith/RRF/Core.lean · 38 lines · 0 declarations
show as:
view math explainer →
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