propositionnovelstructure_uncertain

Full lifts detect the leaf symbol

Full lifts at depth ss detect the leaf noise with probability ≥ 1/4
gives the detection property of the latent gadget
Proposition·prop:latent-full-lift-detection·§3.4 Linear lifts and loss of rank

Statement (paper)

Set s=⌊Hr08θ⌋. s=\left\lfloor\frac{H_{r_0}}{8\theta}\right\rfloor. Every full lift on PsP_s detects ξs\xi_s with probability at least 1/41/4: Pr⁡[there exists z∈B∗ with ψz(ξs)≠0]≥14. \Pr[\text{there exists }z\in B^*\text{ with }\psi_z(\xi_s)\ne0] \ge\frac14.

In plain English

Taking depth s=⌊Hr0/(8θ)⌋s=\lfloor H_{r_0}/(8\theta)\rfloor, every full lift on PsP_s detects ξs\xi_s with probability at least 1/41/4, meaning that with that probability some z∈B∗z\in B^* has ψz(ξs)≠0\psi_z(\xi_s)\ne0.

Why it's here

This is the quantitative detection guarantee that the latent alphabet gadget relies on. The proof tracks harmonic rank down the path: the fresh-isomorphism claim and the per-level drop bound give an expected loss of at most 4θ4\theta per level. Over ss levels the rank survives with probability at least 1/21/2, and a surviving leaf is detected with probability at least 1/21/2, which gives 1/41/4.
Classified novel:
This is the paper's own quantitative detection guarantee for the latent alphabet gadget, obtained by tracking harmonic rank along the path PsP_s with a per-level expected loss of at most 4θ4\theta. It concerns objects defined in this paper (full lifts, the leaf symbol ξs\xi_s, harmonic rank), so no prior result covers it directly.

Uses

Nothing else in the paper

Used by

lemLatent alphabet gadget with detecting noiseclaimHigh-rank families detect with probability 3/16

Inside the proof

claimFresh isomorphisms make genericity typicalclaimExpected harmonic rank drop per levelclaimRank survives and leaf is detected

Sources

PaperOpen
Section
§3.4 Linear lifts and loss of rank
Page
—
Label
prop:latent-full-lift-detection
Line
sections/02-latent.tex:534
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    structure_uncertain
    The base detection bound (eq. latent-base-detection) deriving from this proposition is argued in running text (lines 639-654) outside any proof environment, then used in the proof of lem:latent.