module module high

`IndisputableMonolith.RRF.Models.Quadratic`

The Quadratic module supplies a one-dimensional consistency model for the RRF with strain cost J(x) = x². Researchers verifying that the Recognition axioms are satisfiable cite these results as an explicit example. The module proceeds by direct definition of the cost followed by algebraic verification of equilibrium, unique minimization, and ledger closure.

claimThe quadratic strain model is defined by the cost function $J(x) = x^2$ in one dimension, together with the associated equilibrium condition, unique minimizer, and closed ledger.

background

The module imports core definitions from RRF.Core, an umbrella file that re-exports all core RRF definitions and contains only definitional content with no physical constants, no hypotheses, and no heavy mathlib. It introduces the quadratic strain as the specific instance J(x) = x². The theoretical setting is the Recognition framework in which such concrete models demonstrate that the RRF axioms are satisfiable.

proof idea

This is a definition module containing multiple theorems. It defines the quadratic strain cost as the square function, then verifies the equilibrium and uniqueness properties by direct substitution into the RRF axioms, followed by algebraic proofs of the minimizer and ledger closure.

why it matters in Recognition Science

This module is imported by the RRF.Models umbrella file, which collects concrete examples that satisfy RRF axioms and thereby prove internal consistency of the framework. It supplies the quadratic strain model with J(x) = x² as one such explicit case.

scope and limits

Does not derive physical constants or match experimental data.
Does not extend beyond one spatial dimension.
Does not incorporate the phi-ladder or forcing chain.
Does not address multi-particle or higher-order interactions.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.RRF.Models module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.RRF.Core module_import

declarations in this module (16)

def quadratic1DStrain L23
theorem quadratic1D_equilibrium L30
theorem quadratic1D_unique_equilibrium L34
theorem quadratic1D_minimizer L39
theorem quadratic1D_hasUniqueMin L45
def quadratic1DLedger L55
theorem quadratic1D_ledger_closed L59
def quadratic1DStrainLedger L62
theorem quadratic1D_zero_valid L67
def quadratic1DChannel L73
def quadratic1DOctave L78
theorem quadratic1DOctave_wellPosed L88
def shiftedQuadraticStrain L94
theorem shifted_equilibrium L100
theorem shifted_is_minimizer L103
theorem exp_preserves_argmin L112