rrf_is_fixed_point
plain-language theorem explainer
Researchers studying self-referential closure in formal physics cite the RRF fixed point definition to show that the current formalization accurately describes itself. The construction identifies currentRRF as the description and verifies self-similarity by reflexivity. This supplies the concrete witness needed for nonempty existence and internal consistency arguments in the Recognition framework.
Claim. Let $D$ be the current RRF description with core witness $φ$. Then $D$ satisfies the fixed-point condition that its description equals itself, so $D$ is a DescriptiveFixedPoint.
background
The module treats the Lean formalization itself as a recognition event whose compilation and type-checking constitute measurements. RRF is the function type (Fin 4 → ℝ) → ℝ that serves as the local non-sealed recognition field interface. DescriptiveFixedPoint is the structure pairing an RRFDescription with a self-similarity proof that the description equals itself. currentRRF instantiates this description using the golden ratio φ as core witness together with counts of theorems and hypotheses.
proof idea
The definition is a direct construction. It populates the description field with currentRRF and the self_similar field with the reflexivity proof rfl. No lemmas beyond built-in equality are applied.
why it matters
This definition supplies the witness for the theorem rrf_fixed_point_exists asserting nonempty DescriptiveFixedPoint and populates the is_fixed_point component of self_reference_complete. It realizes the self-referential closure described in the module, where the formalization is an octave of the RRF itself. The construction supports the framework's claim that internal consistency can be proved even while full self-consistency remains out of reach, 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.