alpha_t_lt_half
plain-language theorem explainer
The bound establishes that the ILG mixing parameter derived from the golden ratio as (1 - phi inverse)/2 lies strictly below one half. Cosmologists modeling dark matter as delocalized topological frustration in the Recognition Science framework cite it when building the topology certificate. The proof is a direct algebraic reduction that unfolds the definition and applies linear arithmetic after confirming positivity of the inverse golden ratio.
Claim. The ILG mixing parameter satisfies $alpha_t < 1/2$, where $alpha_t := (1 - phi^{-1})/2$.
background
The module treats dark matter as diffuse phase-saturation in the Z^3 carrier that failed to condense into discrete baryons during baryogenesis, yielding nonzero Betti-1 homology on the parity bundle. The ILG kernel is defined as alpha_t = (1 - phi^{-1})/2 and encodes this geometry at galactic scale. Upstream results include the cost function as the J-cost of a recognition event and the gradient of a scalar field, which together enforce gravitational-only coupling for frustration regions.
proof idea
Unfold the definition of alpha_t to (1 - phi^{-1})/2. Apply inv_pos.mpr to phi_pos to obtain phi^{-1} > 0. Conclude the strict inequality via linarith.
why it matters
This bound supplies the alpha_t_bound field in the DarkMatterTopologyCert, which assembles the positivity, bound, and gravity-only properties to certify the topology. It realizes the ilg_encodes_dm key result stated in the module documentation. In the broader framework it rests on the phi fixed point from the forcing chain and supports the hypothesis that dark matter remains delocalized rather than a discrete particle at a new phi-rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.