sub
plain-language theorem explainer
Closure of the PhiClosed predicate under subtraction holds when both arguments lie in the subfield generated by φ. Algebraic work in Recognition Science, including convexity arguments and rung calculations, cites the result for field operations inside that subfield. The proof is a one-line term that applies the sub_mem property of the generated Subfield instance.
Claim. If $x$ and $y$ lie in the subfield generated by $φ$, then $x-y$ lies in the same subfield.
background
PhiClosed φ x is the predicate that $x$ belongs to phiSubfield φ, which is defined as the Subfield.closure of the singleton set {φ}. The subfield is therefore the smallest subfield of ℝ containing φ and closed under addition, multiplication, and inverses. The lemma sits inside the PhiClosed namespace of RecogSpec.Core and supplies one of the basic closure properties for this algebraic structure.
proof idea
One-line term proof that applies (phiSubfield φ).sub_mem directly to the hypotheses hx and hy.
why it matters
The result supplies subtraction closure required by forty downstream declarations, among them actionJ_convex_on_interp for the J-action convexity statement and nobleGasZFull for the periodic table. It completes the algebraic infrastructure for the φ-generated subfield that appears in the forcing chain and in manipulations of the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.