Hamming layers and the initial majority deficit

Strict majority uses the library predicate Complexity.majority, so a tie is false. The two layers at weights n/2 and n/2+1 straddle its threshold.

def Complexity.BooleanAnalysis.weightLayer (n r : ℕ) : Finset (Fin n → Bool)

The Boolean vectors with exactly r true coordinates.

Equations

• Complexity.BooleanAnalysis.weightLayer n r = {x : Fin n → Bool | Complexity.popCount x = r}

noncomputable def Complexity.BooleanAnalysis.majorityDeficitBound (n : ℕ) : ℝ

A common deficit and density-limit bound for the two majority boundary layers. The logarithmic term bounds their entropy deficit; 128 bounds the mask size.

Equations

• Complexity.BooleanAnalysis.majorityDeficitBound n = 128 + Real.logb 2 (2 * (↑n + 1))