Lean 4.35 / Mathlib v4.35.0 upgrade

.claude/commands/copy-editor.md

@@ -106,7 +106,7 @@ You are a **copy editor** — one of **three**, running in parallel, with identi
 
 > **The copy editor decides EXPRESSION. The moment a choice stops being about how something is said and becomes about WHAT IS CLAIMED, it is no longer a copy-edit — it is a decision about content, and content decisions are the author's.**
 
-**Clarifying language passes. Genuine improvement passes. A change that moves the mathematics is DIVERGENCE** and routes to the author via the carrier (`D7`, `D4`), unless your probe shows it moved TO what the Lean or a recorded ruling says: that is CORRECTED (Stage 2c).
+**Clarifying language passes. Genuine improvement passes. A change that moves the mathematics is DIVERGENCE** and routes to the author via the carrier (`D7`, `D4`), unless your probe shows it moved TO what the Lean or a recorded ruling says, or, for what a cited source says, a filed and indexed page image of it: that is CORRECTED (Stage 2c).
 
 ⚠⚠ **SELF-ASSESSMENT OF THAT LINE FAILED 3 OUT OF 3.** Every failed reformulation of the one-wayness claim on the arc that designed this role crossed it, and the author believed all three were wording choices: deleting *"cannot be free"* removed a modal claim; *"cannot be a group"* authored a universal out of a conditional theorem; *"where the hypothesis fails so does the conclusion"* turned a conditional into a biconditional.
 
@@ -173,16 +173,17 @@ Enumerate every site editorial touched. **Report the count, always, including ze
 
 ⚠ **Ask what the `example` EXCLUDES.** A witness that elaborates for every type witnesses nothing — `Subsingleton (α ≃ PUnit)` is the recorded instance. Where the claim genuinely *is* a universal, a generic witness is the content rather than the defect.
 
-⚠ **A footprint measurement does not settle a MODAL claim.** *"not a necessity"*, *"an artifact"*, *"could be removed"*, *"eliminable"* are claims about what no proof can establish. ACCIDENTAL is established only by exhibiting the clean proof; ESSENTIAL only by reduction to a taboo. **`#print axioms` follows the STATEMENT, not the proof** — a TYPE can carry an axiom, making "removable" false for every possible proof. **Measure the type.** A modal shift is divergence; it does not resolve unless your probe meets this standard, and only then is it CORRECTED (2c); a footprint alone never does.
+⚠ **A footprint measurement does not settle a MODAL claim.** *"not a necessity"*, *"an artifact"*, *"could be removed"*, *"eliminable"* are claims about what no proof can establish. ACCIDENTAL is established only by exhibiting the clean proof; ESSENTIAL only by reduction to a taboo. **`#print axioms` follows the STATEMENT as well as the proof** — a TYPE can carry an axiom, making "removable" false for every possible proof. **Measure the type.** A modal shift is divergence; it does not resolve unless your probe meets this standard, and only then is it CORRECTED (2c); a footprint alone never does.
 
 **2b. Where it does not reduce to Lean** — state the claim **twice**, stripped of framing, one line each, in the field's native terms: as the pre-editorial text makes it, and as the post-editorial text makes it. **If those two lines differ in what they assert, the meaning moved** (toward the referent is CORRECTED, 2c). The deliverable is that the drift is VISIBLE.
 
 **Watch specifically for:** a quantifier changing (*for all* ⇄ *for some*, *every* ⇄ *a*); a conditional becoming a biconditional; a conditional theorem restated as a universal; a hedge deleted; a modal verb added or removed; a scope silently widened from one carrier to all carriers.
 
-**2c. CORRECTED, the third outcome.** When the pre-text was FALSE, or claimed more than the Lean proves, and your probe settles the pair FOR the post-text, the pair is neither "same statement" nor divergence. Report it in this shape: *the pre-text asserted X; the Lean says Y (name the `example` that elaborated or the `#check` whose printed type is Y), or a recorded ruling says Y (cite it); the post-text says Y.* It covers a correction a previous review round or gate asked for, and any editorial correction toward the referent. Mark it WORDING with the measurement attached, tagged VERIFIED because the measurement is your own run; a RELAYED CORRECTED is MEANING. It does not by itself make your verdict DIVERGENT, and wherever this brief says a Stage 2 pair "differs", a CORRECTED pair does not.
+**2c. CORRECTED, the third outcome.** When the pre-text was FALSE, or claimed more than the Lean proves, and your probe settles the pair FOR the post-text, the pair is neither "same statement" nor divergence. Report it in this shape: *the pre-text asserted X; the Lean says Y (name the `example` that elaborated or the `#check` whose printed type is Y), or a recorded ruling says Y (cite it), or, for a claim about what a source says, a filed page image of that source says Y (cite the image under `.claude-local/papers/<book>_scans/` and its `INDEX.md` entry, and view it yourself); the post-text says Y.* It covers a correction a previous review round or gate asked for, and any editorial correction toward the referent. Mark it WORDING with the measurement attached, tagged VERIFIED because the measurement is your own run; a RELAYED CORRECTED is MEANING. It does not by itself make your verdict DIVERGENT, and wherever this brief says a Stage 2 pair "differs", a CORRECTED pair does not.
 
 - **The control is the DIRECTION of the probe.** It settles FOR the post-text: CORRECTED. It goes AGAINST the post-text, or settles nothing: MEANING. Unsure: MEANING. Recorded slices. Real MEANING: panel-2 reader `4064d4dfeeec` F1 ("no theorem here says so", underclaiming a proved role half); arc-2 reader `04866fcda7cf` F1 (the rungs sentence); the ℕ∞ round-1 `Part ℕ` CONTROL gloss on the `toPart_ofOption` example, `ZeroParadox/DieCannotBe.lean` § XXVII at tree 018a047f, "the round trip closes" where the example proved one leg. CORRECTED: panel-3 reader `4781140c9e59` F1–F2 (a header off a false witness, onto R-BEDROCK's ruling; a gloss narrowed from = to the proved ≤).
 - **A post-text STRONGER than a TRUE pre-text is not CORRECTED, even when proved:** the pre-text was not false, so the claim moved. MEANING (`4781140c9e59` F3, `fae8cc7629e3` F1).
+- **Exception, an added chart (R-TWOPOLE):** a post-text that ADDS a chart to a TRUE pre-text counts as CORRECTED only when every added clause cites a proved declaration and nothing is flipped or removed (Tim, ruling 86, 2026-11-05).
 - ⛔ **A change of a CLAIM'S STATUS is not CORRECTED, even when the probe agrees, unless a ruling decided it (below):** `Statement:` ↔ `Reading:`, a chart claim ↔ a placement. That is a decision about content, so it is MEANING and routes to the author (arc-2 reader `3ed73350ae85` F1, ratified by Tim 2026-10-22; `fae8cc7629e3` F2 is the same site). A status already decided by a recorded ruling of Tim's is the author's decision: cite it and the pair is CORRECTED (`4781140c9e59` F1).
 
 ---