research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S5 — Easton non-examples + lt_apply corollary

[rjwalters]

Summary

Session 5 rounding-out of the Easton-function structure in proofs/Proofs/CantorDiagonalizationOQ01OQ01OQ02OQ01.lean. Adds 3 small theorems (one corollary + 2 non-examples). The 2 axioms (easton_permitted_realizable, easton_consistency, both True-codomain placeholders) and 0 sorries are unchanged.

Three new theorems:

1. IsEastonFunction.lt_apply — every Easton function is strictly increasing on regular cardinals ≥ ℵ₀. Direct corollary of succ_le and Order.lt_succ:

   theorem IsEastonFunction.lt_apply {F : Cardinal.{0} → Cardinal.{0}}
       (hF : IsEastonFunction F) {κ : Cardinal.{0}}
       (hreg : κ.IsRegular) (hℵ₀ : ℵ₀ ≤ κ) : κ < F κ :=
     lt_of_lt_of_le (Order.lt_succ κ) (hF.succ_le κ hreg hℵ₀)

2. id_not_isEastonFunction — the identity fun κ => κ is NOT an Easton function. Proof: lt_apply at ℵ₀ would require ℵ₀ < ℵ₀, contradicting lt_irrefl.

3. const_aleph0_not_isEastonFunction — the constant fun _ => ℵ₀ is NOT an Easton function. Same proof pattern.

Why this is real progress (and the limit thereof)

• Non-vacuity grounded with non-examples: previously isEastonFunction_continuum (existence) and isEastonFunction_nonempty (extracted ∃) showed the constraint set is non-empty; the new non-examples confirm it's not vacuously satisfied by every endofunction. The structure is genuinely a constraint.
• Reusable API: IsEastonFunction.lt_apply exposes the strict-increase property as a single lemma any future work can call directly rather than re-deriving from succ_le + Order.lt_succ each time.
• No axiom/sorry delta: this is a structural rounding-out, not Phase-3b work. The 2 True-codomain axioms (easton_permitted_realizable, easton_consistency) remain placeholders pending the genuine ConsistencyOf predicate (estimated 1000+ lines for Gödel-encoded ZFC formulas, or class-forcing infrastructure).

Build status: pending

The worktree's proofs/.lake is a recursive self-symlink (per feedback_researcher_lake_symlink_broken.md), forcing every Docker build to fresh-clone Mathlib (~10–15 min) + cache get (~10 min) — total ~45 min. Following the convention from birthday-OQ-03-OQ-01-OQ-02-OQ-01 PRs #16777, #16837, #16873 (all build-pending drafts), this PR is opened as draft.

The 3 added theorems use only basic structural tactics already exercised elsewhere in the same file:

• lt_of_lt_of_le (standard order combinator)
• Order.lt_succ (used at lines 105, 115, 124, 140 of this file)
• lt_irrefl _ : ¬ a < a (basic Mathlib)
• Cardinal.isRegular_aleph₀ (standard aleph₀ regularity instance)
• le_rfl (trivial)

Risk of build failure is low; review of the proof body should be straightforward by inspection.

Files Modified

• proofs/Proofs/CantorDiagonalizationOQ01OQ01OQ02OQ01.lean (+35 lines: 3 theorems + header update + 3 #check directives; 257→292 total)
• src/data/proofs/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01/meta.json (lineCount 257→292, theoremCount 7→10 in both top-level meta and leanFile; assumptions text expanded to mention the 3 new theorems)
• src/data/research/problems/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01.json (Session 5 entries in builtItems/insights/progressSummary; iteration 4→5)
• research/problems/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01/knowledge.md (Session 5 narrative)

Test plan

• Re-run ./proofs/scripts/docker-build.sh Proofs.CantorDiagonalizationOQ01OQ01OQ02OQ01 from a worktree with warm Mathlib cache
• Confirm IsEastonFunction.lt_apply, id_not_isEastonFunction, const_aleph0_not_isEastonFunction type-check
• Confirm new #check directives at end of file resolve

Related

• Sessions 1–4 in research/problems/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01/knowledge.md
• Most recent merge: PR research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): close 2 sorries (formalized → axiomatized) #16867 (S4, closed 2 sorries; status formalized→axiomatized)
• No open PRs for this slug at session start

🤖 Generated by researcher-11

[rjwalters]

Build verified locally via Docker (./proofs/scripts/docker-build.sh Proofs.CantorDiagonalizationOQ01OQ01OQ02OQ01): all 3060 jobs succeeded; #check output confirms 14 declarations (12 theorems + 2 axioms). researcher-11 2026-05-08.