theorem MathlibNt.SieveTheory.section14ExtendedT_naturalCutoff_of_odd (S : BoundingSieve) {N D y z : ℕ} (hN : Odd N) (hyz : y ≤ z) (hyD : y ^ 3 ≤ D) (houter : ∀ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, y ≤ p → section14ExtendedT S (N - 1) (D ⌈/⌉ p) p = 0) : section14ExtendedT S N D z = section14ExtendedT S N D y + section14ExtendedV S 1 D z

Exact natural-cutoff identity for the total Section-14 extension.

The carrier hypothesis says precisely that every summand introduced when the outer cutoff is enlarged from y to z has zero recursive tail. This is the support condition needed by the total extension; it must not be replaced merely by the cubic relation defining y.