research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S7 PREP — Lever A residual: delete parent vacuous True-codomain axioms (axiom-reduction 6→4, doc-only)

[rjwalters]

Summary

Doc-only PREP scoping the "Lever A residual" refactor explicitly flagged in PR #19112's "Followup Work Available" section. Targets axiom reduction (role doc top priority): bring slug axiom count from 6 → 4 by deleting the parent file's two vacuous True-codomain axioms easton_permitted_realizable and easton_consistency.

Conflict-free with active OPEN PR #19112 (S6 ACT Phase-3b Lever A, MERGEABLE, Docker 3061 jobs clean). This PREP touches zero files PR #19112 modifies — only adds one new session doc.

Progress

• Adds: research/problems/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01/sessions/2026-05-14-s7-prep-lever-a-residual.md (408 LOC).
• Does not touch: proofs/Proofs/**, proofs/Proofs.lean, parent file's meta.json or annotations.json, slug research JSON, state.md, knowledge.md, sibling-slug files, or candidate-pool.

Findings

Role-doc priority alignment (§1.3 of doc)

/.lean/roles/researcher.md §"Axiom Elimination Priority":

"Reducing axiom counts is more valuable than adding new theorems. … Target: On any RICH problem, aim to eliminate at least 1 axiom per session."

This slug is RICH (knowledge score 43). The proposed refactor eliminates 2 axioms by recognizing the parent's True-codomain axioms have no mathematical content beyond what Phase3b's _strong siblings carry.

Parent-file line-range plan (§2 of doc)

Line range	Content	Refactor action
193–215	Part III header docstring	Retain with rewrite: redirect to Phase3b.
217–238	2 axiom declarations + docstrings	Delete.
240–253	Part IV header + 9 retained #check directives	Retain.
254–255	2 #check for deleted axioms	Delete.

Net parent file delta: 257 → ~234 LOC. Axiom count: 2 → 0 in parent file. Slug-level (parent + Phase3b): 6 → 4.

External-caller audit (§3 of doc)

Pre-claim rg "easton_permitted_realizable|easton_consistency" proofs/Proofs/ src/data/ finds 0 functional Lean callers outside the parent file:

• Sibling OQ-02-OQ-03 has its own easton_consistency theorem in a disjoint namespace with a different signature — no collision.
• All src/data/**.json matches are narrative documentation strings, not Lean tactic calls.

Deletion is fully safe.

Conflict-free cross-file path table (§5 of doc)

Path	PR #19112	This PREP	Overlap?
proofs/Proofs.lean	+1 import	—	No.
proofs/Proofs/CantorDiagonalizationOQ01OQ01OQ02OQ01Phase3b.lean (new)	+173 LOC	—	No.
proofs/Proofs/CantorDiagonalizationOQ01OQ01OQ02OQ01.lean (parent)	unchanged	—	No.
research/problems/.../state.md	+64/-33	—	No.
research/problems/.../knowledge.md	+55/-1	—	No.
src/data/research/problems/.../json	+14/-15	—	No.
sessions/2026-05-14-s7-prep-lever-a-residual.md	—	new file	No (filename unique).

Both PRs can land in any order without conflict.

S7 ACT plan (§6 of doc)

Post-#19112-merge, ~30 minutes of work:

1. Parent Lean file: −23 LOC (delete 2 axioms + 2 #check + rewrite Part III docstring).
2. Parent meta.json: lineCount 257 → 234, axiomCount 2 → 0, add additionalFiles field (matching laws-of-large-numbers-oq-04 precedent for companion files), assumptions rewrite.
3. Slug research JSON: knownResults + progressSummary rewrites referencing Phase3b _strong siblings.
4. state.md: S7 session log entry + iteration bump (6 → 7) + axiomatized-table refresh.

Sequencing recommendation (§7)

• Option A (recommended): wait for PR research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S6 ACT — Phase-3b Lever A: ConsistencyOf predicates + strong-Easton axioms (build verified) #19112 merge, S7 ACT off main.
• Option B: mechanic-PR overlay — not recommended because the parent file's transitive imports (OQ01, OQ01OQ01, OQ01OQ01OQ02) make Docker build expensive (~3061+ jobs).
• Option C: refactor axioms as trivial-bodied theorems instead of deleting — not recommended; §3 audit confirms 0 callers, so cosmetic preservation adds dead code.

Status

Outcome: progress (PREP) — S7 Lever A residual is fully scoped at ~−23 LOC parent file delta + meta.json / JSON / state.md updates. Slug axiom count moves 6 → 4 after S7 ACT.

Phase update: state.md unchanged (PR #19112 handles that; this PREP is conflict-free).

Next: S7 ACT, post-#19112-merge, following §6 plan.

Race awareness

gh pr list -R rjwalters/lean-genius --search "cantor-diagonalization-oq-01-oq-01-oq-02-oq-01 in:title" --state open returned 4 OPEN PRs:

• research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S6 ACT — Phase-3b Lever A: ConsistencyOf predicates + strong-Easton axioms (build verified) #19112 (S6 ACT Phase-3b Lever A, MERGEABLE) — this PREP's dependency.
• research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S5 — Easton non-examples + lt_apply corollary #16936, research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S6 — Easton-function closure under pointwise binary max (build pending) #17137, research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S7 — not_permitted_aleph_zero (Part V, build pending) #17169 (CONFLICTING since 2026-05-08) — stale 6 days, superseded by Phase-3a-fix iteration. Maintainer cleanup deferred.

This PREP deliberately touches none of the files modified by any open PR. §5 of the doc has the conflict-free certification.

Pattern

Doc-only axiom-reduction PREP, dispatching a prior PR's explicit "Followup Work Available" item. Distinct from STATE-SYNC (no narrative resync; this adds line-range plan + caller audit) and from cross-PR coordination audit (single open PR, no line-shift mapping needed).

🤖 Generated by researcher-8