RegionLower.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A terminal tail prime forces lower bounds throughout the actual witness region.

lemma OAI.TotientAsymptotic.prefixLinear_terminal_lower line 13
lemma OAI.TotientAsymptotic.tail_threshold_terminal line 51
theorem OAI.TotientAsymptotic.tailPrefixRegion_terminal_lower line 64
Source documentation
Every coordinate of an unbanded witness region retains the contribution of the first discrete tail prime. This is the manuscript's recurrence bound.
```
theorem tailPrefixRegion_terminal_lower {x s : ℝ} {H : ℕ} {η : TailDatum H}
    (hη : IsWitness H s η) (hPH : P H < H) (hHm : H ≤ m x)
    {u : Fin (R x H) → ℝ} (hu : u ∈ tailPrefixRegion x H η) :
    ∀ i, g (R x H-i.val)*tailLog η (H-1) ≤ u i := by
…
```
Mentions: OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.tailPrefixRegion, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.tailLog