pith. machine review for the scientific record. sign in
def definition def or abbrev high

trivialModel

show as:
view Lean formalization →

The trivial model constructs a CPM Model over the unit type with all mass, gap, and test functionals identically zero and the four coercivity constants each equal to 1. Researchers validating the abstract CPM infrastructure cite it as the zero-point sanity check confirming that the core inequalities hold without further hypotheses. The definition is a direct record literal whose nonnegativity and interface obligations are discharged by norm_num.

claimDefine the trivial CPM model over the singleton type by setting the net kernel, projection, energy, and dispersion constants each to 1, with defect mass, orthogonal mass, energy gap, and test functions all identically zero.

background

The Model structure packages a Constants record (four nonnegative reals K_net, C_proj, C_eng, C_disp) together with four functions from the state type to reals: defect mass, orthogonal mass, energy gap, and tests. The upstream coercivity theorem states defect mass(a) ≤ (K_net · C_proj · C_eng) · energy gap(a); the aggregation theorem states the analogous bound with C_disp and the test functional. The module supplies concrete Model instances to exercise these theorems and the LawOfExistence infrastructure.

proof idea

The definition is a direct record construction. Nonnegativity of the four constants is discharged by norm_num. Each of the three interface conditions (projection defect, energy control, dispersion) is proved by intro followed by norm_num, reducing every inequality to 0 ≤ 0.

why it matters in Recognition Science

This definition supplies the baseline case for the CPM framework, allowing immediate verification that both the coercivity link and the aggregation theorem apply to the zero model. It anchors the example suite whose later entries introduce the RS cone and eight-tick models. In the Recognition Science setting it confirms consistency of the inequalities at the zero point before the phi-ladder or dispersion relations are engaged.

scope and limits

Lean usage

example : trivialModel.defectMass () ≤ (trivialModel.C.Knet * trivialModel.C.Cproj * trivialModel.C.Ceng) * trivialModel.energyGap () := trivialModel.defect_le_constants_mul_energyGap ()

formal statement (Lean)

  30def trivialModel : Model Unit := {

proof body

Definition body.

  31  C := {
  32    Knet := 1,
  33    Cproj := 1,
  34    Ceng := 1,
  35    Cdisp := 1,
  36    Knet_nonneg := by norm_num,
  37    Cproj_nonneg := by norm_num,
  38    Ceng_nonneg := by norm_num,
  39    Cdisp_nonneg := by norm_num
  40  },
  41  defectMass := fun _ => 0,
  42  orthoMass := fun _ => 0,
  43  energyGap := fun _ => 0,
  44  tests := fun _ => 0,
  45  projection_defect := by intro _; norm_num,
  46  energy_control := by intro _; norm_num,
  47  dispersion := by intro _; norm_num
  48}
  49
  50/-- Verify coercivity theorem applies to trivial model. -/
  51example : trivialModel.defectMass () ≤
  52    (trivialModel.C.Knet * trivialModel.C.Cproj * trivialModel.C.Ceng) *
  53    trivialModel.energyGap () :=
  54  trivialModel.defect_le_constants_mul_energyGap ()
  55
  56/-- Verify aggregation theorem applies to trivial model. -/
  57example : trivialModel.defectMass () ≤
  58    (trivialModel.C.Knet * trivialModel.C.Cproj * trivialModel.C.Cdisp) *
  59    trivialModel.tests () :=
  60  trivialModel.defect_le_constants_mul_tests ()
  61
  62/-! ## Example 2: Subspace Model -/
  63
  64/-- Subspace model: K_net = C_proj = 1, functionals satisfy equality.
  65This tests the subspace shortcut lemmas. -/

depends on (11)

Lean names referenced from this declaration's body.