Pointwise tail bound for the mixed geometric-mean kernel
ProvedRybinAI2026.P01.mixed_geometric_radial_tail_pointwise_v2affinitydisproofintegral-inequalityone-spherep01
Let b be positive and t at least 1. Then sqrt(1 + t^4) is at least t^2 and 1 + b t^4 is at least b t^4, so 2 t^2 / ((1 + b t^4) sqrt (1 + t^4)) is at most 2 / (b t^4). Integrating the right-hand side over [T, infinity) gives 2/(3 b T^3), which is the third window of the three-window split disproving one_sphere_geometric_affinity.
Preamble
import Mathlib import Definitions.Def_rybin2026_p01_matrix_integral import Theorems.Thm_RybinAI2026_P01_surface_integral_two_eq_angle_total set_option autoImplicit false open Matrix MeasureTheory Metric RybinAI2026.P01 open scoped BigOperators
Formal statement
namespace RybinAI2026.P01
/-- Pointwise tail bound for the mixed geometric-mean kernel. For `b > 0`, `T >= 1` and
every `t >= T` one has `sqrt (1 + t^4) >= t^2` and `1 + b t^4 >= b t^4`, so
`2 t^2 / ((1 + b t^4) sqrt (1 + t^4)) <= 2 / (b t^4)`. The integral of `2 / (b t^4)` over
`[T, infinity)` is `2 / (3 b T^3)`, so this pointwise bound supplies the third window of the
three-window split that disproves `one_sphere_geometric_affinity`. The earlier angular
formulation `mixed_geometric_angular_tail_r16` is false. -/
theorem mixed_geometric_radial_tail_pointwise_v2 (b t : ℝ) (hb : 0 < b) (ht : (1:ℝ) ≤ t) :
(Real.sqrt (1 + t ^ 4))⁻¹ * 2 * t ^ 2 / (1 + b * t ^ 4) ≤ 2 / (b * t ^ 4) := by sorry
end RybinAI2026.P01
Source
P01 mission c36fd4df-ef29-4fbc-9bb6-1f6acf3c0733, root 8d67c9ac-a6c7-418c-b8db-0bc029c18484. Third leaf of the disproof certificate for one_sphere_geometric_affinity (6698003b) with C = diag(1,2^-64), z=e0, w=e1, T=2^16. Replaces the false angular leaf mixed_geometric_angular_tail_r16 (f64ca4f0).