half
plain-language theorem explainer
The lemma shows that one-half lies in the subfield of the reals generated by any real phi under field operations. Researchers deriving half-rung scalings on the phi-ladder cite it for orbit agreements, style gaps, and kinship counts. The term proof first embeds the integer 2 via the rational map lemma then applies subfield inverse closure.
Claim. For any real number $phi$, the number $1/2$ belongs to the subfield of $mathbb{R}$ generated by $phi$.
background
PhiClosed phi x holds precisely when x lies in the subfield generated by phi. The of_rat lemma places every rational into this subfield by the algebra map. The inv lemma records that the subfield is closed under multiplicative inverses: if x is in the subfield then so is x inverse. The module collects universal phi-closed targets that Recognition Science statements are forced to satisfy.
proof idea
Term proof. Apply of_rat to obtain PhiClosed phi 2, then feed the result to inv and let simpa reduce the inverse expression to the target 1/2.
why it matters
Supplies the phi-closed status of the half-rung target used by AgreesAtHalfRung in planetary formation, pleasure_symmetric in aesthetics, and cross_cousin_count in kinship cohomology. It anchors the half-ladder embedding that appears in rung-fraction mass formulas and the eight-tick octave of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.