RRFDescription
plain-language theorem explainer
RRFDescription packages attributes of the RRF formalization as a structure with a real core witness, natural-number counts of theorems and hypotheses, and a nonempty model witness in the function space from reals to reals. Researchers studying self-referential closure in Recognition Science cite it when building meta-level descriptions. The declaration is a plain structure definition introducing four fields with no proof content.
Claim. A structure consisting of a core witness $c : ℝ$, a theorem count $n_t : ℕ$, a model witness given by a nonempty collection of maps $ℝ → ℝ$, and a hypothesis count $n_h : ℕ$.
background
The upstream RRF is the local non-sealed recognition field interface defined as $(Fin 4 → ℝ) → ℝ$. This module treats the Lean formalization itself as a recognition event whose compilation and type-checking constitute measurements. The module setting emphasizes that the RRF formalization forms an octave of the RRF and that internal consistency can be established even though full self-consistency lies beyond Gödel limits.
proof idea
This is a structure definition that introduces four fields with no lemmas applied and no tactic steps.
why it matters
The definition supplies the type used by currentRRF (instantiated with golden ratio φ as core witness), DescriptiveFixedPoint, and MetaRRF in the same module. It realizes the self-description layer of the Recognition framework at the deepest closure level, aligning with the module's emphasis on the framework referring to its own consistency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.