half
plain-language theorem explainer
The lemma shows that one half belongs to the subfield generated by any real φ. Researchers on half-rung embeddings, spin-1/2 statistics, and rung fractions cite this closure property. The proof is a term-mode wrapper that first embeds the rational 2 via of_rat then applies the subfield inversion lemma.
Claim. For any real number $φ$, one has $1/2$ in the subfield of the reals generated by $φ$.
background
PhiClosed φ x is the predicate that x lies in phiSubfield φ, the subfield generated by φ under field operations. The sibling lemma of_rat shows every rational embeds into this subfield for arbitrary φ. The sibling lemma inv states that the subfield is closed under taking inverses.
proof idea
Term-mode proof. Apply of_rat φ 2 to obtain PhiClosed φ 2, then feed the hypothesis to inv and simplify to reach PhiClosed φ (1/2).
why it matters
Supplies the half-rung target used by pleasure_symmetric, cross_cousin_count, AgreesAtHalfRung, and planetaryFormationCert. It populates the universal φ-closed targets that RS claims must hit, supporting the half-ladder embedding and spin-1/2 objects in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.