Upload repro/src/empirical.py with huggingface_hub

Upload repro/src/symbolic_proof.py with huggingface_hub

Add exact Theorem 3.3 hard-instance audit

Restore full repaired logbook (revert stale sync) + add Claim 3 lower-bound executed page (Thm 3.3)

Correct Claim 1 boundary framing (p=1.2 empirically converges; 4/3 is theoretical) + add Claim 5 (p<=4/3 unresolved proof-gap limitation; AdaGrad-Norm resolves it)

Rewrite Claim 2: AdaGrad adapts to both tail index p and noise level (converges across (p,sigma) grid; non-adaptive SGD diverges)

Add Claim 4: AdaGrad-Norm converges for full range p in (1,2] at rate (p-1)/(2p); converges at p=1.2 where coordinatewise AdaGrad fails

Rewrite Claim 1: AdaGrad converges under heavy-tailed noise for p in (4/3,2], adaptive to p; p=1.2 boundary control confirms the 4/3 threshold