def
definition
def or abbrev
subspaceModel
show as:
view Lean formalization →
formal statement (Lean)
66def subspaceModel : Model Unit := {
proof body
Definition body.
67 C := {
68 Knet := 1,
69 Cproj := 1,
70 Ceng := 2,
71 Cdisp := 1,
72 Knet_nonneg := by norm_num,
73 Cproj_nonneg := by norm_num,
74 Ceng_nonneg := by norm_num,
75 Cdisp_nonneg := by norm_num
76 },
77 defectMass := fun _ => 1,
78 orthoMass := fun _ => 1,
79 energyGap := fun _ => 1,
80 tests := fun _ => 2,
81 projection_defect := by intro _; norm_num,
82 energy_control := by intro _; norm_num,
83 dispersion := by intro _; norm_num
84}
85
86/-- Verify subspace shortcut: D ≤ orthoMass when K_net = C_proj = 1. -/
87example : subspaceModel.defectMass () ≤ subspaceModel.orthoMass () :=
88 Model.defect_le_ortho_of_Knet_one_Cproj_one subspaceModel rfl rfl ()
89
90/-- Verify subspace equality when orthoMass = defectMass. -/
91example : subspaceModel.defectMass () = subspaceModel.orthoMass () :=
92 Model.defect_eq_ortho_of_subspace_case subspaceModel rfl rfl (fun _ => rfl) ()
93
94/-! ## Example 3: RS Cone Constants Model -/
95
96/-- Model using the canonical RS cone constants. -/