module module high

`IndisputableMonolith.RRF.Core.Recognition`

RRF.Core.Recognition re-exports the fundamental recognition pairing from the Recognition module. Researchers building RRF models cite it to access the MP principle as a single import. The module performs only re-exports and contains no independent proofs.

claimRe-export of the recognition pairing satisfying T1 (MP): nothing cannot recognize itself.

background

The module imports IndisputableMonolith.Recognition, whose doc-comment identifies the content as T1 (MP): Nothing cannot recognize itself. This supplies the core recognition pairing used throughout the Recognition Science derivation. RRF.Core serves as an umbrella that re-exports all core RRF definitions with only definitional content and no physical constants or hypotheses.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the recognition pairing to the parent RRF.Core umbrella file. It carries forward T1 (MP) into the RRF layer of the framework. RRF.Core itself contains only definitional content with no physical constants, no hypotheses, and no heavy mathlib.

scope and limits

Does not introduce physical constants.
Does not contain hypotheses.
Does not perform heavy mathlib operations.
Does not add independent theorems beyond re-exports.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.RRF.Core module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Recognition module_import

declarations in this module (13)

abbrev Recognize L26
abbrev MP L29
theorem mp_holds L32
abbrev NothingCannotRecognizeItself L35
theorem nothing_cannot_recognize_itself L37
abbrev RecognitionStructure L41
abbrev Chain L44
abbrev RecogLedger L47
def phi L50
def chainFlux L54
abbrev AtomicTick L58
theorem T2_atomicity L61
theorem chainFlux_zero_of_balanced L66