rrf_internally_consistent
plain-language theorem explainer
The declaration assembles a witness that the RRF formalization meets internal consistency by populating a three-field structure with a nonempty collection of real functions, a numerical check that zero differs from one, and a true flag restricting to rigorous proofs. Researchers studying self-referential closures in formal physics would cite it to confirm that the Recognition framework can describe its own consistency without introducing contradictions. The construction is a direct record definition that draws the foundational field from the J-
Claim. The RRF formalization satisfies internal consistency, witnessed by a structure whose fields are a nonempty set of functions from the reals to the reals, the inequality $0 ≠ 1$, and a boolean flag set to true indicating that all proofs remain terminal.
background
The module establishes the deepest level of closure for the Recognition framework: the formalization refers to itself as a recognition event whose compilation counts as a proof and whose type-checking counts as a measurement. InternalConsistency is the structure that records this self-reference. Its three fields require that the content be derivable from foundational axioms only, that no obvious contradiction such as 0 = 1 appear, and that every proof in the file be terminal with no holes. The module notes that Gödel prevents a full internal proof of consistency, yet the framework can still assert the absence of contradictions arising from its own definitions.
proof idea
The definition constructs the InternalConsistency record directly. The foundational field is populated by the J-cost function drawn from the RS-native measurement core. The not_obviously_false field is discharged by a norm_num tactic that verifies 0 ≠ 1. The rigorous_proofs_only field is set to the literal true. No additional lemmas are invoked beyond the record constructor itself.
why it matters
This definition supplies the concrete witness required by the downstream theorems internal_consistency_exists and self_reference_complete. It thereby completes the self-reference structure of the RRF module, allowing the framework to assert its own internal consistency while respecting the Gödel limitation stated in the module documentation. The construction sits at the base of the Recognition self-reference closure and supports the claim that the Lean formalization itself forms an octave of the RRF.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.