alpha_t_pos
plain-language theorem explainer
The theorem proves that the ILG mixing parameter alpha_t is strictly positive. Cosmologists modeling dark matter as topological frustration in the Recognition Science framework cite it when certifying the phantom sector geometry. The tactic proof unfolds the definition and applies the inequality phi inverse less than one together with linear arithmetic.
Claim. Let $alpha_t = (1 - phi^{-1})/2$. Then $alpha_t > 0$.
background
The Cosmology.DarkMatterTopology module treats dark matter as diffuse phase-saturation in the Z^3 carrier that fails to condense into baryons, producing nonzero Betti-1 homology. The ILG mixing parameter alpha_t is defined as (1 - phi^{-1})/2 and encodes this geometry at galactic scales. The result depends on the upstream definition of alpha_t together with the positivity and greater-than-one properties of phi.
proof idea
The proof unfolds alpha_t to obtain (1 - phi^{-1})/2 > 0. It establishes phi^{-1} < 1 by rewriting with inv_lt_one_iff_of_pos applied to phi_pos and closing with phi_gt_one. Linear arithmetic then finishes the inequality.
why it matters
This theorem supplies the positivity component of darkMatterTopologyCert, which bundles it with the half-bound and gravity-only coupling to certify the dark matter topology. It anchors the spatial projection of the phantom sector and supports the claim of no discrete phi-ladder rung for dark matter particles. The result sits inside the eight-tick octave and phi-ladder structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.