defect_eq_ortho_of_subspace_case
plain-language theorem explainer
In the abstract Coercive Projection Method, a model M with K_net = 1 and C_proj = 1 together with the subspace hypothesis that orthoMass coincides with defectMass for every element yields pointwise equality of the two mass functions. Workers formalizing projection inequalities in Recognition Science cite this lemma to recover exact identities inside subspace models. The proof obtains the forward inequality from the specialized defect_le_ortho_of_Knet_one_Cproj_one lemma, derives the reverse direction by simplification of the subspace hypothesis
Claim. Let $M$ be a CPM model with constants satisfying $K_ {net}=1$ and $C_{proj}=1$. If the orthogonal mass equals the defect mass for every element, then for any element $a$ the defect mass of $a$ equals its orthogonal mass.
background
The module LawOfExistence supplies the generic Coercive Projection Method in three abstract parts: projection-defect inequality (A), coercivity factorization through the energy gap (B), and aggregation via local tests (C). Its central object is the Model structure over an arbitrary type β, which packages a Constants record (Knet, Cproj, Ceng, Cdisp), the maps defectMass, orthoMass, energyGap and tests, plus the two axioms projection_defect (defectMass a ≤ Knet · Cproj · orthoMass a) and energy_control (orthoMass a ≤ Ceng · energyGap a). Upstream calibration Jcost_comp_exp_second_deriv_at_zero fixes the second derivative of Jcost at zero to 1, which normalizes the constants used in the projection inequality.
proof idea
The proof first calls defect_le_ortho_of_Knet_one_Cproj_one under the supplied constant hypotheses to obtain defectMass a ≤ orthoMass a. It then applies the subspace hypothesis to produce the reverse inequality orthoMass a ≤ defectMass a by direct simplification. The two directions are combined by le_antisymm to conclude equality.
why it matters
This lemma closes the equality case for subspace models and is invoked by the subspaceModel definition in CPM.Examples, which instantiates a model with Knet = Cproj = 1 and equality functionals. It fills the subspace shortcut inside the CPM A/B/C logic of the Law of Existence module, supporting the abstract setting for Recognition Science projection methods without measure-theoretic scaffolding. It touches the question of when defect and ortho masses coincide exactly under the cone-projection constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.