Density limits from many single-bit neighbors

At rate 16/n, a mask hits any set of at least n/2 coordinates with probability at least 8/9. Its expected size is 16, so the probability that it has more than 128 coordinates is at most 1/8. A selected single-bit neighbor then gives fiber density at least 2^(-128).

Applying this to the two middle Hamming layers initializes Korten's top-down adversary for majority. This is an extension of his parity initialization in ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.

theorem Complexity.BooleanAnalysis.bernoulliAverage_popCount_internal {n : ℕ} (p : ℝ) : (bernoulliAverage p fun (P : Fin n → Bool) => ↑(popCount P)) = ↑n * p

theorem Complexity.BooleanAnalysis.bernoulliAverage_hits_internal {n : ℕ} (p : ℝ) (s : Fin n → Bool) : (bernoulliAverage p fun (P : Fin n → Bool) => if ∃ (i : Fin n), s i = true ∧ P i = true then 1 else 0) = 1 - (1 - p) ^ popCount s

theorem Complexity.BooleanAnalysis.coordinateDensity_of_neighbor_internal {n : ℕ} (X : Finset (Fin n → Bool)) (P x : Fin n → Bool) (i : Fin n) (hi : P i = true) (hx : (Function.update x i !x i) ∈ X) (hsmall : popCount P ≤ 128) : 2 ^ (-128) ≤ coordinateDensity X P x

theorem Complexity.BooleanAnalysis.isDensityLimit_of_many_neighbors_internal {n : ℕ} (hn : 16 ≤ n) (X : Finset (Fin n → Bool)) (x s : Fin n → Bool) (hs : n ≤ 2 * popCount s) (hneighbor : ∀ (i : Fin n), s i = true → (Function.update x i !x i) ∈ X) : IsDensityLimit X (16 / ↑n) 128 x

theorem Complexity.BooleanAnalysis.majority_layers_limits_internal {n : ℕ} (hn : 16 ≤ n) : (∀ x ∈ weightLayer n (n / 2), IsDensityLimit (weightLayer n (n / 2 + 1)) (16 / ↑n) (majorityDeficitBound n) x) ∧ ∀ y ∈ weightLayer n (n / 2 + 1), IsDensityLimit (weightLayer n (n / 2)) (16 / ↑n) (majorityDeficitBound n) y