IndisputableMonolith.RRF.Models

   1import IndisputableMonolith.RRF.Models.Quadratic
   2import IndisputableMonolith.RRF.Models.Trivial
   3
   4/-!
   5# RRF Models
   6
   7Umbrella file for RRF consistency models.
   8
   9These are concrete examples that satisfy RRF axioms, proving internal consistency.
  10
  11## Contents
  12
  13- `Trivial`: The simplest model (Unit, J=0)
  14- `Quadratic`: A continuous model (ℝ, J=x²)
  15-/
  16
  17
  18namespace IndisputableMonolith
  19namespace RRF
  20
  21/-- At least one model exists (consistency at universe 0). -/
  22theorem models_exist : Nonempty (Core.Octave.{0, 0, 0}) := Models.trivialModel_consistent
  23
  24end RRF
  25end IndisputableMonolith
  26