InternalConsistency
plain-language theorem explainer
InternalConsistency bundles three assertions that the RRF formalization derives from foundational axioms, avoids the obvious falsehood 0=1, and restricts itself to rigorous proofs. Researchers examining self-referential closures in formal physics would cite it to confirm the framework compiles without contradiction. The declaration is realized directly as a structure whose fields are instantiated from prior definitions such as Jcost and numerical checks.
Claim. A witness for internal consistency of the recognition field formalization consists of a nonempty collection of functions from the reals to the reals, the proposition that zero is not equal to one, and a boolean flag asserting that all proofs remain rigorous.
background
The RRF Foundation Self-Reference module treats the Lean formalization itself as a recognition event whose compilation counts as a measurement. Upstream, the consistent predicate from SAT backpropagation requires a partial assignment to agree with a total assignment while satisfying both a CNF formula and an XOR system. The RRF abbreviation supplies the local non-sealed recognition field interface, while the PrimitiveDistinction theorem reduces seven axioms to four structural conditions plus three definitional facts.
proof idea
This is a structure definition. Its fields are populated in the downstream construction rrf_internally_consistent by supplying the nonempty Jcost set for the foundational component, a norm_num tactic for the negation of 0=1, and the literal true for the rigorous-proofs flag.
why it matters
The structure supplies the internal-consistency witness required by internal_consistency_exists and by the complete self-reference structure SelfReferenceComplete. It realizes the module's Gödel-like closure: the framework can assert absence of contradictions even though it cannot prove full consistency from within. The declaration therefore closes one scaffolding step in the self-reference octave of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.