mul
plain-language theorem explainer
The lemma establishes that the subfield of reals generated by φ remains closed under multiplication. Algebraists constructing the phi-ring or cost algebra cite it to verify that products of elements algebraic over φ stay inside the same subfield. The proof is a one-line wrapper invoking the mul_mem property of the Subfield instance on phiSubfield φ.
Claim. If $x$ and $y$ belong to the subfield of $ℝ$ generated by $φ$, then the product $xy$ also belongs to that subfield.
background
In RecogSpec.Core the definition phiSubfield φ constructs the smallest subfield of the reals containing φ by taking the closure of the singleton set {φ}. PhiClosed φ x is the predicate asserting membership in this subfield. The module builds on multiplication defined recursively in ArithmeticFromLogic, lifted through quotient constructions in IntegersFromLogic and RationalsFromLogic.
proof idea
The proof is a one-line wrapper that applies the mul_mem property of the Subfield instance for phiSubfield φ to the hypotheses hx and hy.
why it matters
This closure result is invoked by shiftedCompose_val and shiftedComposeH_val in CostAlgebra, by J_at_phi and PhiInt in PhiRing, and by canonicalPhiRingObj and PhiRingHom in RecognitionCategory. It supplies the algebraic closure needed for the J-cost function and the phi-ladder, consistent with the self-similar fixed point at T6 and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.