claimroutineinferred_dep

Pointwise point-star slice inequality

Claim·§6.3 A second score forces positive rare mass·inside propRare point exceptions have positive mass

Statement (paper)

At a common level, for each point

p

, with

b_p

the conditional bad-edge probability,

\nu=\nu_{H(p)}

\zeta=k^{-2}

and

\tau(\nu)=\norm{\nu_A}_2^2+\norm{\nu_{B_1}}_2^2-1

, one has

d_P(p)+\tau(\nu)\ge\frac\lambda4\,2\rho_p(1-\rho_p)-C(b_p+\zeta)

for an absolute constant

C

, where

d_P(p)

is the common-level score at the ordinary point star of

p

with full bit probability

\rho_p

In plain English

At a common level, for each point

p

, the point-star score

d_P(p)

plus

\tau(\nu)=\norm{\nu_A}_2^2+\norm{\nu_{B_1}}_2^2-1

(with

\nu=\nu_{H(p)}

) is at least

\frac\lambda4\,2\rho_p(1-\rho_p)

up to an error

C(b_p+\zeta)

, where

b_p

is the conditional bad-edge probability,

\zeta=k^{-2}

\rho_p

is the full bit probability of the ordinary point star of

p

, and

C

is absolute.

Why it's here

This gives a pointwise lower bound on the point-star score plus the slice term

\tau(\nu)

in terms of the bit variance

2\rho_p(1-\rho_p)

, with errors only from bad edges and

\zeta

. Under the smallness assumptions from the contradiction setup, averaging it should let the later claim bound the common point-star variation

C_P

o(S)

, which is what forces positive rare mass in the proposition.

Classified routine:

A pointwise inequality inside the proof of the rare-mass proposition. It comes from a direct local calculation relating the point-star score and slice term to the bit variance

2\rho_p(1-\rho_p)

, with errors from bad edges, using the paper's earlier definitions; it is bookkeeping rather than a new idea.

Uses

claimFailure forces small exceptions and small T

Used by

claimPoint-star common variation is negligible

Sources

PaperOpen

Section: §6.3 A second score forces positive rare mass
Page: —
Label: —
Line: sections/05-common-levels.tex:450

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Pointwise point-star slice inequality" rests on claim-com-rare-positive-1