← Mathematical handbook

Continuity and the limiting corner of the source parameter path

theorem Papers.Rockel2026XiFootrule.twoParameter_parameters_continuous : Continuous Verification.diagonalHoleAlpha ∧ Continuous Verification.diagonalHoleBeta

The explicit parameter path is continuous, including the regime switch at mu=2.

theorem Papers.Rockel2026XiFootrule.twoParameter_parameters_limit : Filter.Tendsto (fun (μ : ℝ) => (Verification.diagonalHoleAlpha μ, Verification.diagonalHoleBeta μ)) Filter.atTop (nhds (1 / 2, 1 / 2))

The path tends to the corner (1/2,1/2) as the real parameter tends to infinity.