pith. machine review for the scientific record. sign in
lemma proved term proof high

div

show as:
view Lean formalization →

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 φ.

claimLet φ ∈ ℝ. 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  92lemma div (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
  93    PhiClosed φ (x / y) :=

proof body

Term-mode proof.

  94  (phiSubfield φ).div_mem hx hy
  95

used by (22)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.