div
plain-language theorem explainer
The lemma shows that the subfield generated by φ remains closed under division. Recognition Science model builders cite it when ratios of phi-algebraic quantities must stay inside the same algebraic closure for consistent observables. The proof is a direct term application of the div_mem property on the Subfield instance for phiSubfield.
Claim. If $x$ and $y$ lie in the subfield of the reals generated by $φ$, then $x/y$ lies in the same subfield.
background
In RecogSpec.Core the predicate PhiClosed φ x is defined as membership of x in phiSubfield φ, where phiSubfield φ is the smallest subfield of ℝ containing the singleton {φ}. This construction supplies the algebraic closure needed for quantities built from φ under field operations. The module imports Mathlib for Subfield and ObservablePayloads for downstream payload handling. The two upstream results are exactly the definitions of PhiClosed and phiSubfield.
proof idea
Term-mode proof consisting of the single expression (phiSubfield φ).div_mem hx hy, which invokes the division closure axiom of the Subfield structure.
why it matters
The result is referenced by 22 downstream declarations, among them discrete_to_continuum_continuity, DimensionedQuantity, toComplex_div, lsb_unsuppressed_limit, curvature_equals_d2h, solution_exists, and G_ratio_continuous_snd. It supplies the algebraic interface required for the phi-ladder and Recognition Composition Law. The declaration fills a basic closure step inside the RecogSpec layer that feeds both classical-bridge and gravity derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.