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

half

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 111lemma half (φ : ℝ) : PhiClosed φ (1 / (2 : ℝ)) := by

proof body

Term-mode proof.

 112  have htwo : PhiClosed φ ((2 : ℚ) : ℝ) := of_rat φ 2
 113  simpa using inv htwo
 114
 115end PhiClosed
 116
 117/-- Universal φ-closed targets RS claims are forced to take. -/

used by (40)

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

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.