div
plain-language theorem explainer
The lemma establishes closure of the subfield generated by φ under division. Recognition Science model builders cite it to confirm that ratios of phi-algebraic quantities remain admissible. The proof is a one-line term that invokes the division membership property of the Subfield instance for phiSubfield φ.
Claim. Let φ ∈ ℝ. If x and y belong to the subfield generated by φ, then x/y also belongs to that subfield.
background
PhiClosed φ x asserts that x lies in phiSubfield φ, the smallest subfield of the reals containing φ. This subfield is constructed as the closure of the singleton set {φ} under field operations. The div lemma supplies one of the closure properties needed to treat PhiClosed as a subfield under the standard operations on ℝ.
proof idea
The proof is a direct term-mode application of (phiSubfield φ).div_mem hx hy, which follows from the definition of Subfield.
why it matters
This closure property supports downstream results such as discrete_to_continuum_continuity in CoarseGrain and toComplex_div in ComplexFromLogic. It ensures that division preserves membership in the phi-generated field, which is central to algebraic consistency in Recognition Science derivations. The lemma feeds into gravity and Maxwell modules where dimensioned quantities must stay within the allowed algebraic closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.