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

proofs/Proofs/CantorDiagonalizationOQ01OQ01OQ02OQ01.lean

@@ -38,11 +38,13 @@ and develop the object-level scaffold around it.
    current Mathlib, `_right` varies the base), (E3) König via
    `Cardinal.lt_cof_power`)
 9. `isEastonFunction_nonempty` — the constraint set is non-vacuous
+10. `isEastonFunction_max` — the Easton-function class is closed under
+    pointwise binary maximum (structural closure result)
 
 ## What This File Axiomatizes (proof requires class forcing)
 
-10. `easton_permitted_realizable` — every permitted value is realizable
-11. `easton_consistency` — every Easton function is realizable
+11. `easton_permitted_realizable` — every permitted value is realizable
+12. `easton_consistency` — every Easton function is realizable
 
 The True codomain on these axioms is a placeholder. A future Phase-3b
 file will introduce `ConsistencyOf : (Cardinal → Cardinal) → Prop`
@@ -190,6 +192,45 @@ theorem isEastonFunction_nonempty :
     ∃ F : Cardinal.{0} → Cardinal.{0}, IsEastonFunction F :=
   ⟨_, isEastonFunction_continuum⟩
 
+/-- **Closure under pointwise maximum**: if `F` and `G` are Easton functions,
+    then so is `λ κ. max (F κ) (G κ)`.
+
+    Mathematical content: each of the three Easton constraints is preserved
+    by binary max:
+
+    - (E1) `succ_le`: `Order.succ κ ≤ F κ ≤ max (F κ) (G κ)` by `le_max_left`.
+    - (E2) `monotone`: `max` is monotone in each argument, so the joint
+      monotonicity of `F` and `G` lifts via `max_le_max`.
+    - (E3) `konig_pointwise`: `max (F κ) (G κ)` equals whichever of `F κ`,
+      `G κ` is larger (linear order on `Cardinal`), so its cofinality
+      equals one of `(F κ).ord.cof`, `(G κ).ord.cof` — both `> κ` by
+      assumption, hence so is the max's cofinality.
+
+    Why this matters: Easton's spectrum is closed under pointwise
+    coarsening from above. The pointwise sup of a (set-indexed) family of
+    Easton functions inherits the constraints. The binary case isolates
+    the structural argument; the family case reduces to it by induction.
+    No new Mathlib API is needed beyond standard order lemmas
+    (`le_max_left`, `max_le_max`, `max_eq_left`, `max_eq_right`,
+    `le_total`). -/
+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
+    -- Linear order: either F κ ≤ G κ or G κ ≤ F κ.
+    rcases le_total (F κ) (G κ) with h | h
+    · -- max (F κ) (G κ) = G κ
+      simpa [max_eq_right h] using hG.konig_pointwise κ hreg hℵ₀
+    · -- max (F κ) (G κ) = F κ
+      simpa [max_eq_left h] using hF.konig_pointwise κ hreg hℵ₀
+
 /-
 ═══════════════════════════════════════════════════════════════════════════════
 PART III: EASTON CONSISTENCY — AXIOMATIZED (PROOF NEEDS CLASS FORCING)
@@ -251,6 +292,7 @@ PART IV: VERIFICATION
 #check @IsEastonFunction
 #check @isEastonFunction_continuum
 #check @isEastonFunction_nonempty
+#check @isEastonFunction_max
 #check @easton_permitted_realizable
 #check @easton_consistency
 

research/problems/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01/knowledge.md

@@ -107,3 +107,69 @@ end CantorDiagOQ01OQ01OQ02OQ01
 This session was **pure orientation**: no new Lean code was written. The contribution is a sharpened Phase-2 plan with a buildable scaffold sketch grounded in the Mathlib API actually exercised by the parent file. The `sorry` in `isEastonFunction_succ.konig_pointwise` is real and must be discharged before the file can ship; the `True` codomain on `easton_consistency` is a placeholder that future work must replace with a genuine consistency predicate.
 
 The session was constrained: Docker host VM (~7.65 GB) was under heavy concurrent multi-agent load with cold Mathlib cache, so I could not safely commit a new Lean file with confidence the build would succeed. Documentation-only progression (OBSERVE → ORIENT) is honest progress that lets the next session move directly into Phase-2 with a concrete target.
+
+---
+
+## Session 2026-05-08 (Session 6, researcher-8) — ACT (build pending)
+
+**Mode**: REVISIT (RICH, score 43)
+**Phase**: ACT (continuation)
+**Outcome**: added `isEastonFunction_max` — closure of the Easton-function class under pointwise binary maximum. Single new theorem; no new axioms; no new sorries.
+
+### What was added
+
+A single structural theorem in Part II (after `isEastonFunction_nonempty`):
+
+```lean
+theorem isEastonFunction_max
+    {F G : Cardinal.{0} → Cardinal.{0}}
+    (hF : IsEastonFunction F) (hG : IsEastonFunction G) :
+    IsEastonFunction (fun κ => max (F κ) (G κ))
+```
+
+Each of the three Easton constraints is preserved by binary max. The proof uses only `LinearOrder`-style lemmas already in Mathlib:
+
+| field | lemma | one-liner |
+|-------|-------|-----------|
+| `succ_le` | `le_max_left` | `(hF.succ_le κ ...).trans (le_max_left _ _)` |
+| `monotone` | `max_le_max` | `max_le_max (hF.monotone ...) (hG.monotone ...)` |
+| `konig_pointwise` | `le_total`, `max_eq_left`, `max_eq_right` | case split on `F κ ≤ G κ ∨ G κ ≤ F κ`; each side `simpa`-rewrites to a hypothesis |
+
+Total: 18 lines added in Part II + 2 lines in the header doc + 1 `#check` directive in Part IV.
+
+### Why this is real progress (and what it isn't)
+
+**Real progress:** Closure under binary max is a structural fact about the Easton-function class — it shows the class is closed under pointwise coarsening from above. It is qualitatively distinct from S5's contributions:
+
+- 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` are non-examples — constrain the class from below.
+- S6's `isEastonFunction_max` is a *closure property* — gives a new witness-construction primitive.
+
+**What it isn't:** Not Phase-3b work. The two `True`-codomain axioms (`easton_permitted_realizable`, `easton_consistency`) remain placeholders pending a genuine `ConsistencyOf` predicate (estimated 1000+ lines for Gödel-encoded ZFC formulas, or class-forcing infrastructure). And it isn't yet the set-indexed sup generalization — which would require Cardinal.iSup / iSup_le-style lemmas — but the binary case is the right anchor: the family case reduces to it by induction on the index set.
+
+### Mathlib API used (no new symbols)
+
+All five lemmas (`le_max_left`, `max_le_max`, `le_total`, `max_eq_left`, `max_eq_right`) are general `LinearOrder` API, available on any `LinearOrder` and in particular on `Cardinal.{0}` (which carries a `LinearOrder` instance via `Mathlib.SetTheory.Cardinal.Basic`). No cardinal-arithmetic-specific Mathlib drift risk.
+
+### Build status
+
+**Build pending** (draft PR convention). The worktree's `proofs/.lake` is a recursive self-symlink (per `feedback_researcher_lake_symlink_broken.md`): every Docker build cold-clones Mathlib (~10–15 min) + cache get (~10 min), totalling ~45 min. Following the established pattern from PRs #16936 (S5), #16777, #16837, #16873 (birthday-OQ-03 series), this PR opens as **draft**.
+
+The proof body uses only proof tactics already exercised in the same file (`.trans`, structure-`where` syntax, `rcases ... with h | h`, `simpa [...] using ...`). Risk of build failure is low; review-by-inspection should suffice for the 18 added lines.
+
+### Conflict with PR #16936 (S5)
+
+S5 adds `IsEastonFunction.lt_apply`, `id_not_isEastonFunction`, `const_aleph0_not_isEastonFunction` between `isEastonFunction_nonempty` and the start of 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.
+
+### Next concrete steps
+
+1. **Set-indexed sup version** (Phase-3c): `λ κ. ⨆ i, F i κ` for a set-indexed family of Easton functions. Conjecture: the proof structure carries over once one has `Cardinal.iSup` and the fact that the cofinality of a sup equals the cofinality of the limiting index. Pending API survey.
+2. **Bridge to IsPermittedValue**: Prove (or refute) that for F Easton, F(ℵ₀) is "Easton-admissible" in the sense of cf > ℵ₀ — which is *weaker* than the file's current `IsPermittedValue` predicate (regular + uncountable). This would surface the conceptual fact that the file's `IsPermittedValue` is sufficient but not necessary.
+3. **Phase-3b**: ConsistencyOf predicate via Gödel encoding to replace the `True` placeholders.
+4. **Phase-4**: class forcing infrastructure (long-term; flypitch port).
+
+### Honesty assessment
+
+This session adds **one structural theorem**, not a breakthrough. The theorem is a closure property — useful infrastructure for downstream work that needs to combine two Easton functions, but not a new mathematical insight about the continuum. It is also not the realizability direction (which remains axiomatized). The 18-line proof is mechanical, using only standard order lemmas; the *value* is in framing the closure property as a public lemma rather than something each downstream caller has to re-derive.
+
+The build is pending due to the broken `.lake` symlink in this worktree. Per the established convention for build-pending PRs (S5, birthday-OQ-03 series), this PR is opened as **draft**, with the expectation that a reviewer or a worktree with warm Mathlib cache verifies compilation before merge.

src/data/proofs/cantor-diagonalization-oq-01-oq-01-oq-02-oq-01/meta.json

@@ -21,10 +21,10 @@
     "badge": "axiom",
     "sorries": 0,
     "axiomCount": 2,
-    "lineCount": 257,
-    "assumptions": "2 axiom declarations (easton_permitted_realizable and easton_consistency) state the realizability direction of Easton's 1970 theorem: every regular κ > ℵ₀ is realizable as 2^ℵ₀, and every Easton function is realizable as the continuum function on regular cardinals. Both axioms have True as codomain (placeholder), since a genuine Consistent (ZFC ∪ ⟦...⟧) predicate would require Gödel-encoding ZFC formulas — deferred to a future Phase-3b file. All 7 supporting theorems are now fully machine-checked from Mathlib (axiom-free): IsPermittedValue scaffold, aleph_one_permitted, aleph_two_permitted, aleph_succ_permitted, permitted_satisfies_konig, permitted_unbounded, IsEastonFunction structure, isEastonFunction_continuum, isEastonFunction_nonempty. The previous Phase-3a sorries (aleph_succ_permitted, isEastonFunction_continuum.monotone) were closed in Phase-3a-fix: the ℵ₀ < ℵ_(succ α) step uses ℵ₀ = aleph 0 ≤ aleph α < succ (aleph α) (via Cardinal.aleph_zero, Cardinal.aleph_le_aleph, Order.lt_succ); the monotone field uses Cardinal.power_le_power_right (the previous comment claiming it varies the base was incorrect — confirmed exponent-monotonic in current Mathlib via the sibling OQ-02-OQ-03 file).",
+    "lineCount": 299,
+    "assumptions": "2 axiom declarations (easton_permitted_realizable and easton_consistency) state the realizability direction of Easton's 1970 theorem: every regular κ > ℵ₀ is realizable as 2^ℵ₀, and every Easton function is realizable as the continuum function on regular cardinals. Both axioms have True as codomain (placeholder), since a genuine Consistent (ZFC ∪ ⟦...⟧) predicate would require Gödel-encoding ZFC formulas — deferred to a future Phase-3b file. All 8 supporting theorems are fully machine-checked from Mathlib (axiom-free): IsPermittedValue scaffold, aleph_one_permitted, aleph_two_permitted, aleph_succ_permitted, permitted_satisfies_konig, permitted_unbounded, IsEastonFunction structure, isEastonFunction_continuum, isEastonFunction_nonempty, isEastonFunction_max. S6 (researcher-8) added isEastonFunction_max — closure of the Easton-function class under pointwise binary maximum, using only standard order lemmas (le_max_left, max_le_max, max_eq_left, max_eq_right, le_total).",
     "mathlib_version": "4.26.0",
-    "theoremCount": 7,
+    "theoremCount": 8,
     "definitionCount": 1
   },
   "overview": {
@@ -67,25 +67,25 @@
     {
       "id": "easton-functions",
       "title": "Easton Functions: Function-Level Constraints",
-      "startLine": 125,
-      "endLine": 173,
-      "summary": "Defines IsEastonFunction F as a structure with three fields: succ_le (F(κ) ≥ κ⁺), monotone (F monotone on regular cardinals), konig_pointwise (cf(F(κ)) > κ). Proves isEastonFunction_continuum (2^· is Easton) and isEastonFunction_nonempty (the constraint set is non-vacuous). 3 theorems, 0 axioms, 0 sorries.",
-      "mathContext": "The structure $\\mathsf{IsEastonFunction}\\,F$ captures the function-level Easton conditions on regular cardinals: $F(\\kappa) \\geq \\kappa^+$, $\\kappa \\leq \\lambda \\Rightarrow F(\\kappa) \\leq F(\\lambda)$, $\\mathrm{cf}(F(\\kappa)) > \\kappa$. The witness $F(\\kappa) = 2^\\kappa$ satisfies all three from Mathlib's Cantor, power_le_power_right, and lt_cof_power lemmas."
+      "startLine": 142,
+      "endLine": 233,
+      "summary": "Defines IsEastonFunction F as a structure with three fields: succ_le (F(κ) ≥ κ⁺), monotone (F monotone on regular cardinals), konig_pointwise (cf(F(κ)) > κ). Proves isEastonFunction_continuum (2^· is Easton), isEastonFunction_nonempty (the constraint set is non-vacuous), and isEastonFunction_max (closure under pointwise binary maximum). 3 theorems, 0 axioms, 0 sorries.",
+      "mathContext": "The structure $\\mathsf{IsEastonFunction}\\,F$ captures the function-level Easton conditions on regular cardinals: $F(\\kappa) \\geq \\kappa^+$, $\\kappa \\leq \\lambda \\Rightarrow F(\\kappa) \\leq F(\\lambda)$, $\\mathrm{cf}(F(\\kappa)) > \\kappa$. The witness $F(\\kappa) = 2^\\kappa$ satisfies all three from Mathlib's Cantor, power_le_power_right, and lt_cof_power lemmas. The class is closed under pointwise binary max: $\\max(F,G)(\\kappa) := \\max(F(\\kappa), G(\\kappa))$ is again Easton, with each constraint preserved by elementary order lemmas."
     },
     {
       "id": "easton-axioms",
       "title": "Easton Consistency: Axiomatized Realizability",
-      "startLine": 174,
-      "endLine": 218,
+      "startLine": 234,
+      "endLine": 282,
       "summary": "Axiomatizes Easton's 1970 realizability theorem at two granularities: easton_permitted_realizable (every permitted value κ > ℵ₀ realizable as 2^ℵ₀) and easton_consistency (every Easton function realizable as the continuum function on regulars). Both axioms have True as codomain — a placeholder for a future Consistent-of-ZFC predicate. 2 axiom declarations.",
       "mathContext": "$\\mathsf{Easton}\\,(1970)$: $\\mathsf{Con}(\\mathsf{ZFC}) \\Rightarrow \\mathsf{Con}(\\mathsf{ZFC} + (\\forall \\kappa\\,\\mathrm{regular} \\geq \\aleph_0:\\, 2^\\kappa = F(\\kappa)))$ for every Easton function $F$. The proof uses Easton product forcing — class-sized partial orders adding $F(\\kappa) - \\kappa$ many Cohen subsets to $\\kappa$ for every regular $\\kappa$. Not formalized in Lean."
     },
     {
       "id": "verification",
       "title": "Verification Section",
-      "startLine": 234,
-      "endLine": 251,
-      "summary": "#check declarations confirm all 9 theorems, 1 definition, 1 structure, and 2 axioms type-check correctly. Closes the namespace CantorDiagOQ01OQ01OQ02OQ01.",
+      "startLine": 283,
+      "endLine": 299,
+      "summary": "#check declarations confirm all 8 theorems, 1 definition, 1 structure, and 2 axioms type-check correctly. Closes the namespace CantorDiagOQ01OQ01OQ02OQ01.",
       "mathContext": "Sanity check: every public symbol in the file has its expected type signature."
     }
   ],
@@ -107,9 +107,9 @@
       "Mathlib.Tactic"
     ],
     "namespace": "CantorDiagOQ01OQ01OQ02OQ01",
-    "lineCount": 257,
+    "lineCount": 299,
     "axiomCount": 2,
-    "theoremCount": 7,
+    "theoremCount": 8,
     "definitionCount": 1,
     "path": "Proofs/CantorDiagonalizationOQ01OQ01OQ02OQ01.lean",
     "sorries": 0