subspaceModel
SubspaceModel supplies a concrete CPM model over the unit domain with K_net and C_proj both fixed to one. Researchers validating the projection-defect inequality in the abstract CPM setting cite this instance to confirm the subspace shortcut lemmas reduce the defect-ortho relation to equality. The construction populates the Model record with constant functionals and discharges all nonnegativity and control obligations by direct numerical simplification.
claimThe subspace model is the CPM model over the singleton domain with constants $K_{net}=1$, $C_{proj}=1$, $C_{eng}=2$, $C_{disp}=1$, defect mass and ortho mass both the constant function returning 1, energy gap the constant function returning 1, and tests the constant function returning 2. The projection-defect, energy-control, and dispersion conditions hold by direct numerical verification.
background
In the CPM framework the Model structure bundles a Constants record (nonnegative reals K_net, C_proj, C_eng, C_disp) with four domain-to-real functionals (defect mass, ortho mass, energy gap, tests) and three proof obligations (projection-defect inequality, energy control, dispersion). The module CPM.Examples supplies sample instances to validate the core theorems, listing the subspace model as the case with K_net = C_proj = 1 that tests the subspace shortcut. Upstream, the lemma defect_le_ortho_of_Knet_one_Cproj_one states that if K_net = 1 and C_proj = 1 then defectMass a ≤ orthoMass a for any a; the companion lemma defect_eq_ortho_of_subspace_case recovers equality when the two mass functionals coincide.
proof idea
The definition directly constructs the Model record by setting the Constants fields to the stated numerical values and the four functionals to constant maps (defectMass, orthoMass, energyGap to 1; tests to 2). All nonnegativity proofs and the three control conditions are discharged by the norm_num tactic, which reduces the resulting numerical inequalities to true.
why it matters in Recognition Science
This definition provides the minimal test case for the subspace shortcut lemmas defect_le_ortho_of_Knet_one_Cproj_one and defect_eq_ortho_of_subspace_case inside the LawOfExistence module. The module documentation explicitly positions it as the second example that validates the subspace shortcut before the RS cone model. In the Recognition Science framework it confirms that the abstract CPM infrastructure behaves correctly in the K_net = C_proj = 1 regime prior to instantiations that invoke the canonical constants and the eight-tick octave.
scope and limits
- Does not claim physical content or connection to the forcing chain T0-T8.
- Does not generalize to arbitrary positive constants or other domains.
- Does not derive positivity of cmin or other secondary quantities.
- Does not replace the need for a full realization of the Model structure.
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. -/