Category — blocked on network
The last open obligation in the formal-proof corpus: the two neural-convergence theorems. The two Lean files currently prove only ℕ preconditions.
Blocker
Needs Mathlib, whose .olean cache CDN is 403-blocked in the Claude-on-the-web sandbox (lakecache.blob.core.windows.net, mathlib4.lean-cache.cloud, release.lean-lang.org) — confirmed by direct probe.
Ready to go
Self-contained handover committed: docs/proofs/HANDOVER-neural-convergence.md (theorem statements, Mathlib API names, the separate lean4-mathlib project + cached-CI design, the ESN operator-norm ‖W‖ < 1 reframing, hard constraints — no escape hatches).
Action (needs-owner)
Either widen the network allowlist (the 3 hosts above) and re-run on Opus, or run locally per the handover.
- PageRank: damped Google operator
G(x)=α·P·x+(1-α)·v is an ℓ¹ contraction (modulus α) ⇒ Banach fixed point + convergent iterates.
- ESN:
x ↦ W·x + u is a contraction when ‖W‖ < 1 ⇒ unique bounded trajectory + exponential forgetting.
Category — blocked on network
The last open obligation in the formal-proof corpus: the two neural-convergence theorems. The two Lean files currently prove only ℕ preconditions.
Blocker
Needs Mathlib, whose
.oleancache CDN is 403-blocked in the Claude-on-the-web sandbox (lakecache.blob.core.windows.net,mathlib4.lean-cache.cloud,release.lean-lang.org) — confirmed by direct probe.Ready to go
Self-contained handover committed:
docs/proofs/HANDOVER-neural-convergence.md(theorem statements, Mathlib API names, the separatelean4-mathlibproject + cached-CI design, the ESN operator-norm‖W‖ < 1reframing, hard constraints — no escape hatches).Action (needs-owner)
Either widen the network allowlist (the 3 hosts above) and re-run on Opus, or run locally per the handover.
G(x)=α·P·x+(1-α)·vis an ℓ¹ contraction (modulus α) ⇒ Banach fixed point + convergent iterates.x ↦ W·x + uis a contraction when‖W‖ < 1⇒ unique bounded trajectory + exponential forgetting.