Unconditional closure of the actual dyadic Vaughan Type-I input

theorem AnalyticNumberTheory.LargeSieve.apNormalizedVaughanTypeIMean_le_actual_dyadic_shells (N Q u v : ℕ) : apNormalizedVaughanTypeIMean N Q u v ≤ ∑ k ∈ Finset.range (u.log2 + 1), apNormalizedVaughanTypeIFirstShellMean (vaughanTypeIFirstDyadicShell u k) N Q + ∑ k ∈ Finset.range ((u * v).log2 + 1), apNormalizedVaughanTypeIMiddleProductShellMean (vaughanTypeIMiddleProductDyadicShell u v k) N Q

Exact unconditional decomposition of the AP-normalized Vaughan Type-I mean into the actual first and product-dyadic middle shells.

theorem AnalyticNumberTheory.LargeSieve.card_primitiveCharacter_le_totient (q : ℕ) : 0 < q → Fintype.card (PrimitiveCharacter q) ≤ q.totient

Primitive characters form a subtype of all Dirichlet characters, so their cardinality is bounded by Euler's totient without any additional hypothesis.

theorem AnalyticNumberTheory.LargeSieve.vaughanDirectAPNormalizedTypeIInput_actual_dyadic (N Q u v : ℕ) (hN : 0 < N) (hQ : 0 < Q) (hu : u ≤ Q ^ 2) (huv : u * v ≤ Q ^ 2) : VaughanDirectAPNormalizedTypeIInput N Q u v (↑(u.log2 + 1 + ((u * v).log2 + 1))) (vaughanTypeIActualDyadicLogPay N Q u v)

Unconditional direct AP-normalized Type-I input. The physical shell bounds are assembled against the proved exact first/middle long-variable shell decomposition, so no decomposition hypothesis is exposed or carried.