pith. sign in
module module high

IndisputableMonolith.RRF.Models

show as:
view Lean formalization →

The RRF.Models module establishes consistency of the Recognition Recursion Framework at universe level 0 by exhibiting explicit models. It imports a trivial model with a single state and zero cost together with a quadratic model over real vectors whose cost is the squared norm. Researchers checking axiom satisfiability or developing model-specific results would cite this module. The module is a collection of imported concrete definitions rather than a single derived theorem.

claimThere exists a model with state space $S = U$ (unit type) and cost $J = 0$ satisfying the RRF axioms, and a model with $S = {R}^n$ and $J(x) = {||x||}^2$ satisfying the RRF axioms.

background

The RRF framework requires a state space, a J-cost function, and a ledger that closes under the Recognition Composition Law. This module supplies two concrete realizations. The trivial model uses State = Unit, J identically zero, and a trivial ledger 0/0. The quadratic model uses State = R^n with J(x) = ||x||^2 to illustrate continuous optimization. These constructions are drawn directly from the imported Quadratic and Trivial submodules.

proof idea

This is a definition module with no internal proofs. It assembles the existence claim by importing the Trivial submodule, which satisfies the axioms vacuously, and the Quadratic submodule, which supplies a non-trivial continuous instance. The overall structure is therefore a direct presentation of concrete models rather than a tactic-based derivation.

why it matters in Recognition Science

The module supplies the concrete instances needed for the sibling theorem models_exist, which asserts consistency at universe 0. In the Recognition Science setting it provides test cases for properties such as the Recognition Composition Law and minimizer theorems. It thereby supports downstream verification of RRF structures before they are linked to the forcing chain or physical constants.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (1)