research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S6 — Easton-function closure under pointwise binary max (build pending)

[rjwalters]

Summary

Session 6 structural closure result for proofs/Proofs/CantorDiagonalizationOQ01OQ01OQ02OQ01.lean. Adds one theorem (isEastonFunction_max): the Easton-function class is closed under pointwise binary maximum. The 2 axioms (easton_permitted_realizable, easton_consistency, both True-codomain placeholders) and 0 sorries are unchanged.

The new theorem

theorem isEastonFunction_max
    {F G : Cardinal.{0} → Cardinal.{0}}
    (hF : IsEastonFunction F) (hG : IsEastonFunction G) :
    IsEastonFunction (fun κ => max (F κ) (G κ)) where
  succ_le κ hreg hℵ₀ :=
    (hF.succ_le κ hreg hℵ₀).trans (le_max_left _ _)
  monotone κ ν hκ hν hℵ₀ hκν :=
    max_le_max
      (hF.monotone κ ν hκ hν hℵ₀ hκν)
      (hG.monotone κ ν hκ hν hℵ₀ hκν)
  konig_pointwise κ hreg hℵ₀ := by
    rcases le_total (F κ) (G κ) with h | h
    · simpa [max_eq_right h] using hG.konig_pointwise κ hreg hℵ₀
    · simpa [max_eq_left h] using hF.konig_pointwise κ hreg hℵ₀

Each of the three Easton constraints is preserved by binary max via standard LinearOrder lemmas already in Mathlib:

field	proof primitive
succ_le	le_max_left + transitivity
monotone	max_le_max
konig_pointwise	le_total case split + max_eq_left/max_eq_right

Why this is real progress (and the limits thereof)

Real progress: This is qualitatively distinct from S5 (PR #16936 — lt_apply corollary + non-examples):

• S5's lt_apply is a corollary of the succ_le field — restates an existing constraint.
• S5's id_not_isEastonFunction and const_aleph0_not_isEastonFunction constrain the class from below.
• S6's isEastonFunction_max is a closure property — gives a new witness-construction primitive. The pointwise max of two distinct Easton functions is generally not equal to either, so this builds genuinely new examples.

What this isn't: Not Phase-3b work — the two True-codomain axioms remain placeholders. Not yet the set-indexed sup generalization (Phase-3c) — that requires Cardinal.iSup and is the natural follow-up.

Mathlib API used (no new symbols)

All five lemmas are general LinearOrder API on Cardinal.{0}:

• le_max_left : a ≤ max a b
• max_le_max : a₁ ≤ b₁ → a₂ ≤ b₂ → max a₁ a₂ ≤ max b₁ b₂
• le_total : a ≤ b ∨ b ≤ a
• max_eq_left : b ≤ a → max a b = a
• max_eq_right : a ≤ b → max a b = b

No cardinal-arithmetic-specific drift risk. The proof tactics (.trans, where syntax, rcases ... with h | h, simpa [...] using ...) are already exercised elsewhere in the same file.

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 PR #16936 (S5) and the birthday-OQ-03 series (#16777, #16837, #16873, all build-pending drafts), this PR is opened as draft.

The 18 added lines use only tactics already exercised in the same file. Risk of build failure is low; review-by-inspection should suffice.

Conflict with PR #16936 (S5)

S5 adds IsEastonFunction.lt_apply, id_not_isEastonFunction, const_aleph0_not_isEastonFunction between isEastonFunction_nonempty and Part III. S6 adds isEastonFunction_max in the same region. The two will text-conflict on whichever lands second; mathematical content does not conflict. Either order is fine — the rebaser can place all four new theorems in any order between isEastonFunction_nonempty and the Part III header.

Files Modified

• proofs/Proofs/CantorDiagonalizationOQ01OQ01OQ02OQ01.lean (+42, −0 lines: 1 theorem with docstring + 1 #check + 4-line header doc update; 257→299 total)
• src/data/proofs/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01/meta.json (lineCount 257→299, theoremCount 7→8 in both meta and leanFile; assumptions text + section endLines updated)
• src/data/research/problems/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01.json (Session 6 entries in builtItems/insights/progressSummary; iteration 4→6)
• research/problems/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01/knowledge.md (Session 6 narrative)

Test plan

• Re-run ./proofs/scripts/docker-build.sh Proofs.CantorDiagonalizationOQ01OQ01OQ02OQ01 from a worktree with warm Mathlib cache (or after S5 research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S5 — Easton non-examples + lt_apply corollary #16936 merges)
• Confirm isEastonFunction_max type-checks
• Confirm new #check @isEastonFunction_max directive resolves
• Re-verify axiomCount = 2 with grep -c "^axiom " proofs/Proofs/CantorDiagonalizationOQ01OQ01OQ02OQ01.lean (no new axioms introduced)

Related

• Sessions 1–5 in research/problems/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01/knowledge.md
• S5 PR research(cantor-diagonalization-oq-01-oq-01-oq-02-oq-01): S5 — Easton non-examples + lt_apply corollary #16936 (open, build-pending draft): adds lt_apply + 2 non-examples — non-overlapping mathematical content with S6
• 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)
• Sibling: CantorDiagonalizationOQ01OQ01OQ02OQ03.lean (Easton spectrum on aleph indexing)
• Parent: CantorDiagonalizationOQ01OQ01OQ02.lean (König's exclusion theorems)

🤖 Generated by researcher-8