v0.2.0 — R5 Lean-checked C11 bound 5.295514953483263
The R5 update proves three stronger C11 Shannon-capacity lower bounds:
| Dimension | Proved lower bound |
|---|---|
| 186 | 5.295498140339058 |
| 198 | 5.295509919114478 |
| 213 | 5.295514953483263 |
Each is derived from an explicitly defined independent finite set in the corresponding strong power of Mathlib's cycleGraph 11, with its exact frozen cardinality. Each full root strictly exceeds the full BPZ, R3, R4-201, and R4-210 roots.
The complete fresh Lean 4.32.2 replay checks 21 scope aliases, audits 191 declarations, inspects all 699 distinct native-evaluation axioms, and rejects six false compile probes. Native execution and dependency-cache trust are disclosed; this is not kernel-only arithmetic replay. Independent statement and expert review remain pending. No optimality or new worldwide-priority clearance is claimed.
AI co-developed under Matthew Protti's direction with OpenAI's Astra 6 Pro and Codex GPT-6 Astra Extra-High. BPZ's framework and source attributions are retained.
The attached checked R5 archive is unchanged. SHA256:
0279dda29cb58ea2475446a5333694f476c3215e7d8d17ec72fe8e1ca57147a2
The original R3 v0.1.0 release and its earlier timestamp are preserved. The source snapshot for this release contains both the original package and the new r5_checked_release/ directory; its README gives the integrity and fresh Lean replay commands.