DescriptiveFixedPoint
plain-language theorem explainer
The structure encodes a self-referential description of the recognition reference frame in which the description equals itself. Foundational researchers in Recognition Science cite this when closing the self-reference loop of the formalization. It is introduced directly as a structure with a description field and a trivial equality witness.
Claim. A self-referential fixed point of the recognition reference frame description consists of a record containing a real-valued core witness, a natural-number theorem count, a nonempty model witness, and a hypothesis count, together with the assertion that the description equals itself.
background
The module sets the recognition reference frame as its own description, the deepest closure level in the framework. An RRFDescription records the core witness in the reals (tied to the golden ratio), the count of proved theorems, a nonempty model witness for consistency, and the hypothesis count. Upstream interfaces include the RRF abbreviation as a map from Fin 4 to reals to reals, ledger factorizations, and simplicial edge lengths that supply the surrounding metric and forcing structures.
proof idea
This is a direct structure definition. The self-similar field is witnessed by reflexivity on the equality of the description to itself.
why it matters
It supplies the fixed-point object used by the theorem asserting existence of the RRF fixed point and by the complete self-reference structure. This realizes the module claim that the formalization is an octave of the RRF itself, providing internal consistency without external proof, consistent with the Gödel-like structure noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.