pith. sign in
module module high

IndisputableMonolith.RRF.Core.Recognition

show as:
view Lean formalization →

The RRF.Core.Recognition module re-exports the fundamental recognition pairing that encodes T1 MP. Researchers constructing RRF core definitions cite it to access the base recognition axiom without duplication. The module performs a direct re-export from the parent Recognition module and contains no independent proofs.

claimThe recognition pairing satisfying MP: no entity $x$ recognizes itself, re-exported as the base object for RRF core structures.

background

The upstream Recognition module states T1 MP as 'Nothing cannot recognize itself'. This module imports that result and re-exports sibling definitions including Recognize, MP, RecognitionStructure, Chain, RecogLedger, phi, chainFlux, AtomicTick, and T2_atomicity. The local setting is the Recognition Science framework in which all physics derives from a single functional equation via the forcing chain T0-T8, with the recognition composition law as the central algebraic identity.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the T1 MP recognition pairing that feeds directly into the RRF.Core umbrella file. The downstream module collects all core RRF definitions and states that it contains only definitional content with no physical constants, no hypotheses, and no heavy mathlib. The re-export therefore closes the definitional layer before constants such as $c=1$, $\hbar=\phi^{-5}$, and $G=\phi^5/\pi$ are introduced in later stages of the forcing chain.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)