Task context · pinned snapshot
Context pack v2
The updated snapshot after a passing local Lean run, with the earlier failed route retained.
Included research context
The pack selects relevant material; it does not certify completeness or independent review.
Mathematical material
4 claims, 2 proof outlines, and cited source passages.
Prior work
2 attempts and 2 Lean runs, linked to exact inputs.
Recorded attempts
Failed direct route
The non-strict witness gives n ≤ p, which cannot establish n < p.
Inspect attempt →Passing strict-bound route
Apply the pinned theorem at n + 1 and derive a strict bound.
Inspect attempt →Snapshot identity
Attempts retain the exact context pack they used, so later changes do not rewrite what the contributor saw.
IDs, checksum, and source version
- Pack ID
- context-prime-strict-v2
- SHA-256
- d67c6f126d758b69be14e1afcb5ad1e4fea90e717757bb0b60ba79fd99c83d3e
- Mathlib commit
- 32d24245c7a12ded17325299fd41d412022cd3fe
- Previous pack
- context-prime-strict-v1