# Math audit (working notes): Hironaka, "Resolution of Singularities in Positive Characteristics", preprint dated March 23, 2017, 92 pp.

Date 2026-10-23. AI-generated working notes (model claude-fable-5-1, Claude Code agent); not human-reviewed; no formal verification. Source: /Users/tdupuy/repos/dumps/refs/hironaka-resolution-of-singularities-in-char-p.pdf, read via `pdftotext -layout` (all 92 pages). Page numbers are the manuscript's printed page numbers. Computations: verify.sage (output verify-output.txt), search_constant_ridge.py / search_constant_ridge2.py (outputs *.out). The companion report.md is the self-contained write-up; these are the line-level notes behind it.

Conventions used below. E = (J, b) an ideal exponent; S(E) the set of permissible LSBs (Def. 2.5, p.6); ℘(E) = ⊕_d ℘(E,d) the characteristic algebra (Thm 4.1, p.17); Ê the maximum base-hike (§6.1, p.29); Ě the core-edge focusing (§6.2, p.30); Inv_ξ(E) = (n, n−r, q_1,…,q_r) (Eq. (34), p.24); Diff^{(m)} = differential operators of order ≤ m (§3.1.1, p.7: "differential operators of orders ≤ m"); ∂^{(β)} Hasse derivatives (Eq. (8), p.9); ℘̃, ℘^{nega} the extension (Def. 5.1, p.25).

---

## 0. Architecture / dependency graph

```
§2–3  preliminaries (ideal exponents, S(E), Diff theorem 3.1, AR theorem 3.10, NE theorem 3.15)   [cited to [22],[23],[24]]
  │
§4    ℘(E) finitely generated, Diff-closed, integrally closed (Thm 4.1/4.4, p.17–18)  [cited to [23]]
  │   edge data / Inv (Eq. 26–28, 34; pp.20–24); cot(E) (Def 4.14/4.18, pp.22–23); edge decomposition (Thm 4.19, p.24)
  │
§5    negative part ℘^{nega}(E,−a) := Σ_d Diff^{(dm+a)} ℘^{posi}(E,dm)   (Def 5.1, Eq. (36), p.25)        <-- R2: trivial (= O)
  │
§6    Ê (Thm 6.1, p.29); Ě via (43)/(44) (p.30)                                                                <-- R1: (44) vacuous, (43) unproven
  │   Thm 6.3 (criterion for ℘^{nega}, p.30–31); L(Ě) LL-heads (Def 6.12, p.33); Thm 6.14 (p.34)
  │
§7    Thm 7.1/7.2 (Inv non-increase, p.35); Lemmas 7.3–7.6 (p.35–36); Thm 7.8 Eq.(59) transformation rule for ℘^{nega} (p.37)  <-- R3: false
  │   §7.4 translations (Lemma 7.14, Cor 7.15 p.40)  <-- Cor 7.15 misstated; §7.5 cleaning (p.40–42)
  │
§8    unit-monomial / standard expressions (Prop 8.1, Thm 8.6–8.8, pp.42–46)  <-- proofs of 8.6/8.7 incomplete
  │
§9    LLUED: Thm 9.2 "master key" (p.47) — vacuous given R2; H♭ operators (§9.5–9.7, pp.50–53); LL-chain (83),(84) (pp.54–55);
  │   tail y(e) (Def 9.20, p.56); Thm 9.18, Cor 9.19 (p.55–56)
  │
§10   Lemma 10.1, Thm 10.3–10.6 (pp.59–61): Sing(Ě) ⊂ tail hypersurface Y    <-- proofs are non sequiturs; statement undetermined
  │
§11–13 GLUED: operators Λ, τ, θ, σ (pp.63–67), diagram (104), T(Ě), Cot(Ě) (Def 13.2, p.67)
  │
§14   local vs global: Thm 14.1–14.2, Cor 14.3 (pp.68–69); Thm 14.4 (p.69) and Lemma 14.5 (p.70) proofs break off; Thm 14.6/Cor 14.7 (p.70); Thm 14.8 (ℓ̄) p.71
  │
§15   AR-schemes (Def 15.1, p.74); CotAR-scheme Y(E) (Def 15.5, p.76); chain Y(0)⇝Y(1)⇝… (Def 15.7–15.8, pp.77–78);
  │   Thm 15.9 (p.79), Thm 15.10 (p.79–80): terminal plat ∇ smooth                                                <-- R4: Step 2 false
  │
§16   Thm 16.4 (Theorem ∆: reduction to Ê, p.82–83) + Lemma 16.5 (Γ-monomial, p.83)
      Thm 16.6 (Main Thm I, p.84): (1) permissibility, (2) strict lex drop of Inv-string off ∇', (3) equality on ∇', (4) D=∇ ⇒ ℘^{posi} empty   <-- R5: (2),(4) false
        via Lemmas 16.7–16.11 ("domino fall", pp.85–86)                                                              <-- rests on R3
      Thm 16.13 (Main Thm II, p.87): "apply 16.6 repeatedly, finitely many times" — termination rests on 16.6(2)
      Thm 16.14 (Main Thm III, p.87) = 16.4 + 16.13
```

Load-bearing steps for the final theorem: (A) Thm 16.6(2) [termination], (B) Lemma 16.8 "domino fall" [needs the transformation rule Eq.(59)/Rem. 7.7 for ℘^{nega}], (C) Thm 15.10 [smooth terminal plat as center], (D) Thm 10.3/10.4 [Sing(Ě) ⊂ tail hypersurface, i.e. permissibility of the AR-reduced centers], (E) well-definedness of Ě (§6.2) and of the Inv-string.

---

## 1. §2–3: preliminaries

- p.7, §3.1.1: Diff^{(m)} = operators of order ≤ m, identified with Hom(D^{(m)}, O). This is the standard convention and it is the one used in Thm 4.1(2) and Thm 4.5 (p.18): Diff^{(μ)}℘(E,a) ⊂ ℘(E,a−μ) with μ ≥ 0 includes μ = 0 (O-module structure) and Thm 4.5 is exactly Diff^{(a−b)} ⊇ Diff^{(0)}. Noted because it drives R2 below.
- p.12, Lemma 3.14: the proof is a textual fragment ("We have the natural epimorphism φ : O_V → O_Y. Let J = (φ^{-1}(I), I(Y,V))^b O_V and then The proof is reduced to … Then has the required property"). The statement (natural AR-extension (J,b) of (I,b) with AR-equivalence) is plausible via Lemma 15.3's construction G = (J + I(X)^b, b). Classify: sketched/garbled, repairable (use Lemma 15.3).
- pp.12–16, Thm 3.15 (Numerical Exponent theorem) with Rem. 3.16–3.25 and Prop. 3.26: type (I) sequence (blow up D(j) = T(j) ∩ H(j) in Z[t]) makes ord_{H(r)} F_i(r) = ord(E_i) + r(ord(E_i)−1) (Eq. 18); type (II) blows up the hypersurface H(r,k) (an isomorphism) and lowers the order by exactly 1 per step (Eq. 19) while permissible; the stopping number s_i(r) satisfies N ≤ s_i(r) ≤ N+1 with N = ord(E_i)(r+1) − r; S(E_1) ⊂ S(E_2) gives s_1(r) ≤ s_2(r); dividing by r and letting r → ∞ gives ord(E_1) ≤ ord(E_2). I checked each step; the argument is complete modulo typographical noise (e.g. Rem. 3.22 "b_j" for "b_i", Def. 3.24 indices). Classify: proved (re-proof of a published result of [23]).
- p.10, Thm 3.10 (AR theorem): J♯ = Σ_{j<b} (Diff^{(j)}J)^{b!/(b−j)}, F = (J♯ O_W, b!). This is the coefficient-ideal construction (cf. Hauser's BAMS 2003/2010 "coefficient ideal"); cited to [22],[24]. Used in V1 below.

## 2. §4: ℘(E), edge data, Inv

- p.17: two definitions (geometric: ℘(E,a) = union of ideals I with S(I,a) ⊃ S(J,b); algebraic: integral closure in Bl(Z)* of O[Diff^{(j)}J in degree b−j]). Their equivalence is cited to [23] (Lemmas 2.1–2.2 and claim (♭) p.918 there), explicitly "under the assumption that K is perfect". Not re-proved here; I take it as given for the audit.
- IMPORTANT for later: because ℘(E) is integrally closed *as a graded algebra* (Thm 4.1(3)), ℘(E,1) can contain linear elements that are not derivatives of J. Example (V1): E = (x²+y⁵, 2) in char 2. All permissible LSBs for E (over Z and over Z[t]) have centers in the strict transforms of {x = 0} (verified for the finite tree in verify.sage; over Z[t] the same computation applies with t a spectator), so S(y⁵,2) ⊃ S(E), i.e. y⁵ ∈ ℘(E,2) (geometric definition), hence x² = f − y⁵ ∈ ℘(E,2), hence xT is integral over ℘(E) and x ∈ ℘(E,1). So the edge algebra at 0 is (x̄) and Inv_0(E) = (2, 1, 1) — not (2,1,2) as the tangent cone x̄² would suggest. Consequence: Inv is NOT computable from the tangent cone alone; in particular "ridge" computations (V4) are only a proxy for Inv. All Inv claims in these notes are argued S-theoretically.
- p.22–23, Def. 4.14/4.18 (cot): as printed, cot(E,ℓ)_ξ = p^ℓ-th root of (ρ^ℓ(Bl(Z,1)) ∩ ℘(E,p^ℓ) + max(O_ξ)Bl(Z,p^ℓ)). Since Bl(Z,p^ℓ) = O as a module, max(O_ξ)Bl(Z,p^ℓ) = max(O_ξ), and the formula would make cot(E)_ξ = max(O_ξ). Clearly intended: max(O_ξ)·bl_ξ(Z,p^ℓ) = max^{p^ℓ+1} (as in Eq. (21), p.18). With that reading cot(E)_ξ = {y : ȳ^{p^ℓ} ∈ edge algebra in degree p^ℓ for ℓ ≫ 0}. Classify: ill-typed as printed, repairable.
- p.24, Thm 4.19 (edge decomposition) cited to [22]–[25]; Rem. 4.20 constructs R(E). Not checked.

## 3. §5: the negative part ℘^{nega} — R2 (first-class)

Def. 5.1 (p.25): ℘̃(E,−a) = Σ_{d: dm ≥ |a|} D(m,a,d), D(m,a,d) = Diff^{(dm+a)}_Z ℘^{posi}(E,dm), with m a common multiple of the generator degrees and (Rem. 5.5, Eq. (37), p.26) an element g ∈ ℘(E,m)_ξ with ord_ξ g = m assumed at every ξ ∈ Sing(E)_cl ("From now on throughout this section we will be assuming the existence of the element g in Eq.(37)").

**Claim R2.** Under these hypotheses ℘^{nega}(E,−a)_ξ = O_ξ for every a > 0 and every ξ ∈ Sing(E)_cl; likewise ℘̃(E,0)_ξ = O_ξ.

Proof 1 (from the definition). For a > 0 and d = 1: D(m,a,1) = Diff^{(m+a)}℘^{posi}(E,m) ⊇ Diff^{(m)}(g) (order ≤ m+a includes order ≤ m). Since ord_ξ g = m exactly, in the completion K̄[[x]] some monomial x^β with |β| = m has nonzero coefficient c, and ∂^{(β)}g ≡ c mod max(O_ξ) is a unit. Hence 1 ∈ D(m,a,1)_ξ.

Proof 2 (independent of the "≤ m vs = m" reading of Diff^{(m)}; uses only the manuscript's Thm 6.3 and Thm 4.5). Thm 6.3 (p.30): f ∈ ℘^{nega}(E,−a)_ξ iff g^{p^ℓ} f ∈ ℘(E, qp^ℓ − a) for all ℓ ≫ 1 (q = deg g). Take f = 1: g^{p^ℓ} ∈ ℘(E, qp^ℓ) ⊂ ℘(E, qp^ℓ − a) by Thm 4.5 (p.18: ℘(E,a) ⊂ ℘(E,b) for a > b). Hence 1 ∈ ℘^{nega}(E,−a). (Thm 4.5 is geometrically correct: S(I,a) ⊂ S(I,b) for a > b since transforms satisfy I'_b = I(D)^{a−b} I'_a.) Even if one only trusted the "if" direction's mechanics: for f = h = 1, d = 0 the proof of Thm 6.3 applies ∂^{(p^ℓ α)} with ∂^{(α)}g = u a unit to g^{p^ℓ} ∈ ℘(E, qp^ℓ − a) and lands in D(m',a,d') with d'm' = qp^ℓ − a, producing u^{p^ℓ} ∈ ℘^{nega}(E,−a). ∎

Consequences (each checked against the text):
- Lemma 5.3/Thm 5.11 (coherence) true but trivial.
- Lemma 5.6 (p.27, monotonicity in d): the displayed proof uses Diff^{(N)}(g^{d'−d}·X) ⊃ Diff^{(N−md)}(g^{d'−d})·Diff^{(md+a)}(X); the Leibniz rule gives the opposite inclusion ⊂. Conclusion is true anyway (trivially, by R2).
- Lemma 5.9(4) (p.28) is garbled ("The sum of the two ideals of (1) is contained in the ideal of ℘nega(E,−b) contains the ideal of ℘posi(E,−a)").
- Thm 6.5 (p.32): ℘^{nega}(Ê,−a) ⊂ Ker(σ) — consistent (Ker σ = O_V since g·1 ∈ ℘(Ê,q−a) ∩ ℘(Ê,q)).
- Thm 6.7, Thm 7.11(1),(2), Thm 7.12: true, trivially.
- **Thm 9.2 "Master key" (p.47)**: "there is h ∈ ℘^{nega}(Ě)_ξ with ord_ξ h ≥ ord_ξ ε and (g − h)^{1/p} ∈ O_ξ" — vacuous: take h = ε (or ε minus any p-th power). Thm 9.3 likewise, given the ord_D condition (take h = ε after the Lemma 7.3 adjustment y ∈ I(D); then ord_D ε ≥ q).
- The homogeneity-degree bookkeeping of §9.7 (−δ(A,I,0) = 2q − |α+pβ+qγ_0| etc., p.51) assigns degrees to elements of a module that is O in every negative degree; it is bookkeeping about *which* copy of O the element is placed in, not a constraint on the element.
- **Thm 7.8, Eq. (59) (p.37)**: ℘^{nega}(E',−a)_{ξ'} = Π I(D_i,Z_i)^a ℘^{nega}(E,−a) O_{Z'} at ξ' ∈ π^{-1}(ξ) ∩ Sing(E') with Inv_{ξ'}(E') = Inv_ξ(E). FALSE. Counterexample (V1): E = (x²+y⁵,2), char 2, D = origin, ξ' = origin of the chart y (E' = (x'²+y³,2)), a = 1. E is max-hiked with Inv_0 = (2,1,1) (see §2 above) and E' is max-hiked at ξ' with the same Inv. LHS = O_{ξ'} by R2 applied to E' at ξ'. RHS = I(D)O_{ξ'} = (y)_{ξ'} ≠ O_{ξ'}. The computation in Rem. 7.9, Eq. (60) (p.37) fails at the step "= z^{−a}(g')^{p^ℓ}℘^{nega}(E',−a)_{ξ'} (degree down by division)", which uses ℘^{posi}(E', mp^ℓ−a) = (g')^{p^ℓ}·℘^{nega}(E',−a); Thm 6.3 only gives ⊇ for the right-hand side's image, not equality (and in fact ℘^{posi}(E', mp^ℓ−a) ⊋ (g')^{p^ℓ}O).
- Rem. 7.7 ("the transform of ℘^{nega}(E,−a) is adding a-times exceptional divisor") is therefore not a property of elements of ℘^{nega}: the element 1 ∈ ℘^{nega}(E,−a) would have to transform to z^a, but 1 ∈ ℘^{nega}(E',−a) as well. In the LL-chain identity g(i) = g(i+1)^p + h(i) (Eq. (83)–(84), p.54–55) the pull-back forces h(i) ↦ z^{−q(i)}π*h(i) (both other terms transform with weight −q(i)); this is the transformation rule actually imposed on h(i), and it is a different one from Rem. 7.7's z^{+a}π*h. Rem. 9.25 (p.58) instructs to "go back to the original homogeneity summands and honor their inherited rule of transformations", but an identity in O cannot be pulled back with different rules for different summands.
- **Lemma 16.8(1) (p.85)**: "g'(e−1) = g'(e)^p + h'(e−1) does not vanish at ξ' because h'(e−1) vanishes there by the rule of transformation of ℘^{nega}". With h'(e−1) = z^{−p}π*h(e−1) (forced by the chain identity), vanishing on the exceptional divisor requires ord_D h(e−1) > p, whereas Thm 9.3/Lemma 16.7 only provide ord_D h ≥ q(i) = p. The "domino fall" is unsupported. (In the examples below it does fail: see R5.)

## 4. §6: Ê and Ě — R1 and R6

- Thm 6.1 (p.29), second sentence: "for every d > 0 and every ξ ∈ Sing(Ê)_cl we have d = ord_ξ ℘(Ê,d) provided ℘(Ê,d) ≠ (0)". FALSE for d not a multiple of the hike. Counterexample (V2): Narasimhan's f = x² + yz³ + zw³ + y⁷w, char 2, Ê = (f,2), ξ = 0. ℘(Ê,1) ∋ ∂f ≠ 0 but every element of ℘(Ê,1)_0 has order ≥ 2: an element of order 1 would define a smooth hypersurface containing Sing(Ê) near 0 (S(h,1) ⊃ S(Ê) implies Sing(Ê) ⊂ {h=0}), and Sing(Ê) = C = (t³²,t⁷,t¹⁹,t¹⁵) has embedding dimension 4 at 0 (semigroup ⟨32,7,19,15⟩ has all four as minimal generators; I(C) has no order-1 generator — verify.sage V2). So ord_0 ℘(Ê,1) ≥ 2 > 1. The proof ("its differentiations produce nontrivial edge generators") only yields elements of order ≥ d − μ > ... in degree d − μ when the Hasse derivative of the initial form is nonzero; for a p-th-power initial form all lower-order derivatives of the initial form vanish. The first sentence (r(ξ) > 0) is fine. Eq. (37) is only guaranteed for m a multiple of the hike degree; the manuscript does choose m as a common multiple (Def. 5.1), so downstream use is unaffected.
- **R1, §6.2 (p.30).** Two definitions of Ě are offered. (43): ℘(Ě) ⊃ ℘(Ê) maximal with Sing(Ě)_cl = {ξ : Inv_ξ(Ê) = Inv_max}. (44): S(Ě) = ∩_{i≤r} S(℘(Ê,q_i), q_i) ∩ S(Ê).
  (44) is vacuous: for every i, ℘(Ê,q_i) is (geometric definition, p.17) the union of ideals I with S(I,q_i) ⊃ S(Ê); a sum of such ideals again satisfies S(I_1+I_2, q_i) = S(I_1,q_i) ∩ S(I_2,q_i) ⊃ S(Ê); so S(℘(Ê,q_i),q_i) ⊃ S(Ê) and the right side of (44) equals S(Ê). Hence (44) gives Ě ~ Ê and Sing(Ě) = Sing(Ê), contradicting (43) whenever Inv is not constant on Sing(Ê) (e.g. Narasimhan's example: Inv_0 = (4,3,2) but at η ∈ C∖0 the derivative f_z = yz² + w³ has order 1 (∂_y f_z = z² ≠ 0), so Inv_η = (4, ≤2, …) < Inv_0; the Inv-max stratum is {0}, not C).
  (43): the family {E : ℘(E) ⊃ ℘(Ê), Sing(E) = Σ} is directed under the ∩ operation of §4.3.1 (p.24), so a maximal ℘ is the union of a directed family of finitely generated algebras; its finite generation (needed for everything in §§6–16) is not addressed. No existence proof is given. Classify: ill-posed definition; the intended object (an ideal exponent with ℘ ⊃ ℘(Ê) and singular locus the Inv-max stratum) can be obtained e.g. as Ê ∩ (I(Σ),1) when Σ is smooth, but then Thm 6.14(1) etc. need re-checking; for singular Σ I do not know a canonical choice with finitely generated ℘.
- Thm 6.14 (p.34), "Proof. Follows immediately from Eq.(52), Eq.(54) and Eq.(55)": item (1) (a single system of edge generators valid at every point of V ∩ Sing(Ě)) needs core-focusing plus a coherence argument; not given. Plausible.

## 5. §7: transformations, translations, cleaning

- Thm 7.1 (p.35): Inv never increases at ξ' ∈ π^{-1}(ξ) ∩ Sing(E'). This is the one classical-type statement in the chapter (Hironaka 1970 / Giraud: non-decrease of the ridge). The manuscript's proof (Lemma 7.6, p.36) is one sentence: "ord_{ξ'}(g_i') = ord_ξ(g_i) … hence the g_i' are enough to generate the edge data … Thus the Inv equality". Sketch of a genuine argument for the "n−r" component: the initial forms in(g_i') ≡ ȳ_i'^{q_i} mod (z̄) with ȳ_1',…,ȳ_r',z̄ independent (Lemma 7.5), so the edge ideal at ξ' contains an ideal of height r, hence has ≥ r generators; for the q-components one needs a degree argument. Not written in the manuscript. V4 (verify.sage): 375 near points of random order-2/order-4 hypersurfaces in char 2, ridge data never increased lexicographically (ridge, not ℘-Inv: a proxy). Classify: plausibly true, proof sketched.
- Lemma 7.3 (p.35): correct (g ∈ I^q ⇒ ε ≡ y^q mod I, a q-th power in R/I, in max(R̄)^{q+1}, hence ȳ ∈ max(R̄)² since order is a valuation on a regular local ring).
- Lemma 7.4/7.5: fine.
- Lemma 7.10 (p.37–38): invokes "the inclusion of Eq.(62) for all ℓ ≫ 1" where (62) is displayed later inside Thm 7.11's proof — forward reference; the argument (Cartier extension ∆(ℓ), Krull intersection, faithful flatness) is the same device as Thm 6.3 and is fine modulo the assertion ∆(g^ℓ x^β) = x^β (should be ∆(ρ^ℓ(g) x^β) = x^β with ρ^ℓ(g) = g^{p^ℓ}).
- Cor. 7.15 (p.40): "for every monomial x^α we have ∂_j((x − ρ^N(a_N))^α) = ∂_j(x^α)" is false as stated (char 2: ∂_x(x − c)³ = (x − c)² ≠ x²). The true statement is that the Hasse-derivative *operators* with respect to x and with respect to x − a coincide. Harmless misstatement.
- Thm 7.17 (p.40): "W(ξ) = 0 ⇒ W(η) = 0 nearby" — proof is one line about translations; the statement (vanishing of a coherent module at a point propagates to a neighborhood) is false for coherent modules in general (W(ξ)=0 means fibre zero ⇒ W_ξ = 0 by Nakayama ⇒ W = 0 near ξ; OK, fine for finitely generated modules). Fine.
- §7.5 cleaning (pp.40–42): formal g-cleaning ε♯(∞) = Σ_{j<q} y^j σ(0,j) in K̄[[y,ω]] using Ô = ⊕_{j<q} y^j K̄[[g,ω]]; approximation ε♯(N). Cor. 7.20's proof is one garbled sentence. The construction is standard (division by g = y^q + ε as a Weierstrass-type expansion requires ord ε > q so that g is regular in y of order q — fine).

## 6. §8: standard expressions

- Prop. 8.1 (p.42–44): for h ∈ K̄[[x]] a presentation h = Σ_{a_i < ℓ} A_a x^a with units A_a ∈ ρ^ℓ(K̄[[x]])?? As printed "unit in ρ^ℓ(K[[x]])" — but the proof produces units in K̄[[x]] (B_a + B_b x^{b−a}), not p^ℓ-th powers. Rem. 8.2 then iterates. Unclear.
- Thm 8.6 (p.44–45): the proof writes h = Σ_c h(c)^{p^ℓ} x^c, expands each h(c) by Prop. 8.1, and then claims the lexicographically maximal θ has ∂^{(θ)}h = h(c,k)^{p^ℓ} "clearly an element of O_ξ". But ∂^{(θ)} also hits terms u(θ')x^{θ'} with θ' ∈ θ + Z^n_{≥0}, θ' ≠ θ, contributing u(θ')C(θ',θ)x^{θ'−θ}; these need not vanish (Lucas: C(θ+p^ℓk, θ) ≡ C(k,0)·… is 1 for k ≥ 0). So the "lexicographical induction" does not isolate coefficients. Thm 8.7 (uniqueness) has the same gap. Classify: sketched, gap; probably repairable by a more careful order (e.g. divisibility order instead of lex), but I did not do it. Since the downstream use (H♭ operators) is vacuous by R2, this does not affect the verdict.

## 7. §9: LLUED

- Lemma 9.6 (p.50) three cases; Rem. 9.9–9.11 (p.51): Case (III) item (5)–(7): "(h♭)^k(ε(0)) ∈ ℘(Ě, q − k b)" and H♭ = (h♭)^{k̄} — read as operator iteration (h♭∘h♭∘…), not as a power; as a power it would not eliminate the top monomial (example: g = x² + y³z + z⁴, char 2, q = 2: top monomial y³z, h♭(ε) = ∂_y∂_z(ε)·∂_y^{(2)}(ε) = y³z, b = 2, k̄ = 2; (h♭)² as a power is y⁶z² and ε − y⁶z² keeps y³z; as iteration h♭(h♭(ε)) = y³z and ε(1) = z⁴ = (z²)², as intended).
- Def. 9.12/Eq.(79)–(80) (p.51–52): the claim that iterating H♭ terminates with ε(m+1) ∈ ρ(O) ∩ ℘^{nega} (Eq. 80) is the real content of §9; the mechanism (each H♭(ε(j)) is unit·(top monomial) + lexicographically smaller tail) is plausible but the tails' effect on the "rest portion" is asserted ("Thus Eq.(79) is justified", p.52), not proved. Termination by Lemma 9.14/Prop. 9.15 (lex well-ordering of finite sequences in Z^N ∪ {∞}): Prop. 9.15 as stated is fine (well-ordering of lex on tuples with ∞-padding for *bounded length* N; the manuscript's "finite sequences" of varying length are padded, fine).
- Given R2, the only non-vacuous content of an LL-chain (Eq. (83)–(84)) is: g(i) = g(i+1)^p + h(i) with g(i+1) ∈ O (so h(i) ≡ g(i) mod ρ(O)), ord_ξ h(i) > q(i), and y(i+1) ≡ y(i) mod max². Any choice h(i) = ε(i) − φ^p with ord φ > q(i)/p works. The tail y(e) is therefore a p^e-th root of g − H with H ≡ ε mod ρ^e(O) arbitrary within those constraints: the "coordinate-free" issue of §11 is real, since different φ give different tails.
- Thm 9.18 (p.55): (1) y(e) − y ∈ max² ✓ (each step changes y(i) by a p-th root of a higher-order term); (2) y(e) mod max² ∈ v(Ě) nonzero ✓. Cor. 9.19 ✓ (edge generators of p-power degree have cotangent parameters; Thm 6.11 p.33).
- Thm 9.22/9.29 (p.56, 58): "Proof. Infer to Def.(6.15)". Finite generation of the tails module t(Ě;V,ℓ) as ρ^ℓ(O)-module: plausible given finitely many heads and a fixed ℓ.

## 8. §10: enclosure of Sing(Ě) by tails — R6 (undetermined statement, invalid proofs)

- Lemma 10.1 (p.59): given the LL-chain at ξ, for each η ∈ Sing(Ě) ∩ V there is a *modified* chain at η (y(i,η) = y(i) − u(i,η) with u(i,η) ∈ ρ^N(O(V)) ∩ max(O_ξ)) with the same head and same h(i), whose tail vanishes at η. This just translates the tail so that it vanishes at η; the modification depends on η.
- Thm 10.4 (p.60): "the LL-chain extends uniquely to every point of V ∩ Sing(Ě)_cl and its scheme-tail Y contains V ∩ Sing(Ě). Proof. Lemma 10.1 applies to every η." Non sequitur: Lemma 10.1 gives, for each η, a different hypersurface {y(e) − u(e,η) = 0} through η; it does not show that the single hypersurface Y = {y(e) = 0} contains η. Thm 10.3 ("Sing(Ě) ∩ V ⊂ Y for every triplet") inherits the gap. Thm 10.5 similar.
- Thm 10.6 (p.61): for smooth D ⊂ Sing(Ě), the tail vanishes along D. Proof replaces y(j) by y(j) − c(j) with c(j) ∈ I(D) ∩ max² (Lemma 7.3) and ε(j) by ε(j) + c(j)^{q(j)}, "then both g(j) and h(j) are unchanged … Hence its tail g(e) = y(e) is unchanged." But by Eq. (84)(7)–(8) the tail *is* y(e) (g(e) = y(e) + ε(e), ord ε(e) > 1); replacing y(e) by y(e) − c(e) changes it unless c(e) = 0. The proof is incoherent. A correct argument for smooth D exists along different lines: if ord_D h(e−1) ≥ p then g(e)^p = g(e−1) − h(e−1) ∈ I(D)^p so g(e) ∈ I(D); but ord_D h(e−1) ≥ p is exactly what is not established in general (it depends on the choice of h(e−1); it holds for the choice h = ε when y ∈ I(D)).
- Is the *statement* of Thm 10.3/10.4 true (is the Inv-max stratum always contained in a smooth hypersurface, namely the tail)? I looked for a counterexample of the simplest shape — a hypersurface f = x² + ε(y,z,w) in char 2 whose order-2 locus is a monomial curve C = (t^A,t^a,t^b,t^c) of embedding dimension 4 and whose tangent cone is a square of a linear form at every point of C (so that the ridge-type data is constant along C; this is necessary but, by §2 above, not sufficient for Inv to be constant). Result (search_constant_ridge.py, search_constant_ridge2.py; exhaustive over A,a,b,c < 24, monomials of degree ≤ 10; both found none), with proof:

  **Lemma (no monomial-curve example).** Let p = 2, f = x² + ε(y,z,w), C : t ↦ (t^A, t^a, t^b, t^c) with gcd(A,a,b,c) = 1. If f, ∂_y ε, ∂_z ε, ∂_w ε and the mixed Hasse derivatives ∂_y∂_z ε, ∂_y∂_w ε, ∂_z∂_w ε all vanish on C, then C ⊂ {x = m(y,z,w)} for a monomial m, a smooth hypersurface.
  Proof. Write ε = Σ monomials (coefficients in F_2 suffice for the parity argument; over a general perfect field group monomials by t-weight and parity class). For the monomial y^i z^j w^k put D = ia + jb + kc and parity class (i,j,k) mod 2. Vanishing of ε − x² on C, of the three first derivatives and of the three mixed second derivatives on C is a system of 7 F_2-linear conditions per weight D on the eight class-counts N(D,·) mod 2 (Σ_all N = [D = 2A]; Σ_{i odd} N = 0; Σ_{j odd} = 0; Σ_{k odd} = 0; Σ_{i,j odd} = 0; Σ_{i,k odd} = 0; Σ_{j,k odd} = 0). Solving: for D ≠ 2A all eight counts have a common parity s(D); for D = 2A the seven nonzero classes have parity s and class 000 has parity 1 + s. Class (1,0,0) with D ≡ 0: a ≡ D(m) ≡ 0 mod 2 whenever that class is odd at some weight; if every class is even at every weight except at D = 2A with s = 0, then exactly one monomial, in class 000, has weight 2A: ε = m² + (pairs cancelling on C), so C ⊂ {x = m}. Otherwise some class with i odd is odd at some weight, forcing a even; similarly b, c even; gcd = 1 forces A odd. Now compute the second Hasse derivative in t of ε(C(t)) = t^{2A}: D_t^{(2)}(ε∘C) = Σ_j ∂_j ε·D_t^{(2)}y_j + Σ_{i<j} ∂_i∂_j ε·y_i'y_j' + Σ_j ∂_j^{(2)}ε·(y_j')² = 0 on C (first and mixed derivatives vanish; y_j' = a_j t^{a_j − 1} = 0 since a_j even), while D_t^{(2)} t^{2A} = C(2A,2) t^{2A−2} = A(2A−1)t^{2A−2} ≡ t^{2A−2} ≠ 0 (A odd). Contradiction. ∎
  More generally (non-monomial C with parameter t), the same computation gives the necessary "tangency" condition x'(t)² = Σ_j ∂_j^{(2)}ε(C(t))·y_j'(t)², i.e. the tangent of C lies in the hyperplane ker ℓ_η for the varying linear form ℓ_η = x + Σ_j (∂_j^{(2)}ε(η))^{1/2} y_j whose square is the tangent cone. Whether such C exist with embedding dimension ≥ 3, and with Inv (not just ridge) constant, I did not determine. If ℓ_η is constant along C then g − ℓ^q ∈ I(C)^{(q+1)} and g ∈ I(C)^{(q)} force ℓ ∈ I(C), so C ⊂ {ℓ = 0}: a counterexample needs ℓ_η to vary.
  Status: Thm 10.3/10.4 UNDETERMINED (proof invalid; no counterexample found; monomial-curve counterexamples excluded).

## 9. §§11–14: GLUED

- Def. 11.3, Eq. (94)–(97) (p.63–64): Λ_{e−i}X = X + Diff*_{Z/Z(p^i)}(X)·Diff_Z(X) (diff-products), τ_{e−i}(Y) = Y ∩ ρ^i(ρ^{e−i}(cot(Ě)) + I(Sing)^{(p^{e−i}+1)}Bl(Z)); L_{e−i}(j+1) = τΛL_{e−i}(j); L_{e−i}(∞) = ∪_j. Rem. 11.6: stabilization by Noetherianity (the sequence is increasing in j) ✓.
- Def. 12.3 θ (p.65): θ_{e−i}: L_{e−i}(∞) → ‖L_{e−i}(∞)‖_{p^{e−i}} "contraction" (forget degrees, sum into O, place in degree p^{e−i}). Rem. 12.4 "θ(θ^{-1}) acts as the identity because we are taking ideal-sum only". Def. 12.5 (p.66): L_{e−i}(0) = θ_{e−i+1}^{-1}(θ_{e−i+1}L_{e−i+1}(∞) ∩ ρ(O)) — the step-down. Since ℘^{nega} = O in each negative degree (R2), the sets Λ(X) ⊂ ℘̃ are unconstrained in negative degrees and the diagram (104) lives in ⊕_{d≤0} O ⊕ ℘^{posi}; the only real content is the ∩ρ(O) and the τ-intersections.
- Thm 14.1 (p.68) items (1)–(4): proofs are one paragraph of assertions. Thm 14.2 (p.69): "ρ^i(g(i)) ∈ θ_{e−i}(L_{e−i}(∞))" — asserts the local chain members are among the global ones; proof: "H♭ operators are all Diff-products contained in the corresponding members of the GLUED diagram". Plausible for the Λ-part; the τ-part (intersection with cot + I(Sing)^{(p^{e−i}+1)}) requires h(i) ∈ I(Sing)^{(…)}, i.e. the h(i) vanish to high order along Sing(Ě) — not shown (ord_ξ h(i) > q(i) at the one point ξ is shown; along Sing is Thm 9.3-type, which again depends on the choice).
- **Thm 14.4 (p.69)**: proof is the fragment "Infer to Lem.(5.9) of §5. It is important to note that the" — ends mid-sentence.
- **Lemma 14.5 (p.70)**: proof is the fragment "… Now assume this inclusion for e − i > 0 and we want to prove ρ^e(cot(Ě)) ⊂ L_{e−i−1}(0)." — ends.
- Thm 14.6 (p.70), second line "S(T(Ě),1) ⊂ I(Sing(Ě))Bl(Z)" is type-mismatched (a set of LSBs ⊂ a module). The proof's content: "every LSB permissible for Ě is permissible for (L(Ě),q)" (true since L(Ě) ⊂ ℘(Ě,q)) and "always so for ℘^{nega}(Ě) by the rule of transformation of the negative degree parts" (R2/R3: vacuous/false). Cor. 14.7 ("Sing(Ě') ⊂ transform of Sing(Ě)") is either trivial (total transform) or false (strict transform; e.g. E=(x²+y⁵,2), Sing(E') ≠ ∅ while the strict transform of the point is empty).
- Thm 14.8 (p.71): existence of a single ℓ̄ — fine (finitely many operators; quasi-compactness).

## 10. §15: AR-schemes — R4

- Def. 15.1 (p.74): AR-scheme = finite family of triplets (V_j, F_j, Y_{ji}), Y_{ji} smooth closed in V_j of common dimension m, F_j ⇝ F_j(Y_{ji}); Sing(Y) := ∩ Sing(F_j(Y_{ji})) (item (5) prints ∪ but Thm 15.9 and Eq. (124) use ∩). Lemma 15.2 (gluing of ideal exponents with equal S on overlaps) ✓ via ℘. Lemma 15.3 (G = (J + I(X)^b, b) has AR-equivalence to F on X) ✓.
- Def. 15.5/Eq. (117) (p.76): Y(E): V_j, hypersurfaces Y_{ji} = {h_{ji} = 0} for CotLL generators h of Cot(Ě), F_j = Ě|V_j. Thm 15.6 (p.77): S(E(1)) = S(F_j) ∩ S(Cot(Ě),1) glues. ✓ given Lemma 15.2.
- Def. 15.7–15.8 (pp.77–78): E(s) → Ê(s) → Ě(s) → Cot(Ě(s)) → Y(s) → E(s+1) with S(E(s+1)) = S(Ě(s)) ∩ S(Cot(Ě(s)),1). Eq. (124): dim Y(s) = n − rank v(Ě(s)).
- Thm 15.9 (p.79): "n > dim Y(0) > dim Y(1) > …" and "Sing(Ě) = Sing(Y(0)) ⊋ Sing(Y(1)) ⊋ … ⊋ Sing(Y(t)) ⊋ Sing(Y(t+1)) = Sing(Y(t+2)) = …" and "Y(t+1) is smooth, i.e. F(t+1)_j is the zero ideal". The first chain is contradicted by V1 (dim Y(0) = dim Y(1) = 1); "zero ideal" conflicts with Thm 15.10(3) "Sing(Y(t+1)) is a smooth closed non-empty subset". Sing(Ě) = Sing(Y(0)) requires Sing(Ě) ⊂ ∩Y_{ji} (Thm 10.3; see §8).
- **Thm 15.10 Step 2 (p.80), R4.** Claim: if Sing(Y(s+1)) = Sing(Y(s)) then, for a system f = (f_1,…,f_m) ⊂ Cot(Ě(s)) inducing a basis of v(E(s))_ξ, "the ideal J(s) of Ě(s) has generators contained in (f)^{b(s)}ρ^ℓ(O)", hence E(s+1) = Ê(s+1) = Ě(s+1), Y(s+1) = Y(s), and Sing(Ě(s+1)) = {f = 0} is smooth. FALSE. Counterexample (V1): E = (x²+y⁵,2), char 2, n = 2. Ê = Ě = E (Sing = {0}, Inv constant trivially). Cot(Ě) = (x) (the only cotangent direction; tails of LL-chains headed by x² are x). Y(0) = {(A², E, Y = {x=0})}, F(Y) = ((f, (∂f)²)|_{x=0}, 2) = (y⁵, 2) on A¹ (verify.sage: J♯|_{x=0} = (y⁵)); Sing(Y(0)) = {0}. S(E(1)) = S(E) ∩ S(x,1) = S(E) (every center in the tree lies on the strict transform of {x=0}: verify.sage V1), so E(1) ~ E, Ě(1) ~ E, Cot(Ě(1)) = (x), Y(1) = Y(0), Sing(Y(1)) = Sing(Y(0)) = {0}: stabilization at s = 0. Step 2 would give J(0) = (x²+y⁵) ⊂ (x)²ρ^ℓ(O) — false (y⁵ ∉ (x)) — and Sing(Ě(1)) = {x = 0} — false (it is {0}). What is true in this example: the terminal plat ∇ = Sing(Y(0)) = {0} happens to be smooth. Whether ∇ is always smooth is UNDETERMINED (the proof is wrong; I have no counterexample; in Hauser's kangaroo example f0 = x²+y⁷+yz⁴ the order-2 locus is the cusp {x=0, z²=y³}, but Inv is not constant along it — at η ≠ 0 the local ℘ contains the two linear elements x and u = y³+z² since near η all infinitely near points lie on x = 0 and on u = 0 — so the Inv-max stratum is {0} and ∇ = {0}).
- Thm 15.10 Step 1: "if Sing(Y(s)) ≠ Sing(Y(s+1)) then H(s+1) nontrivial ⇒ dim Y(s+1) < dim Y(s)": the dimension of Y is n − rank v(Ě(s+1)); that the cotangent rank strictly increases is asserted, not proved.

## 11. §16 — R5 (first-class)

- Thm 16.4 (Theorem ∆, p.82–83): reduction of ERS for E = (J,b) to ERS for maximum base-hiked exponents with NC data, by successively resolving (J,d), (J',d−1), … and ending in the Γ-monomial case. This is the standard "maximal-order reduction"; the bookkeeping "K(1) = (K(0)', d(1)) ∩ E(1)" is loose (the ∩ of ideal exponents of different b's is (J_1^{b_2}+J_2^{b_1}, b_1b_2), p.24) but the strategy is standard and I regard it as repairable. Lemma 16.5 (Γ-monomial case, p.83): the invariant (n−s, A, |T|) is described with s = "shortest length of subsystems with non-empty intersection" (as written s = 1 whenever some Γ_i ≠ ∅; intended: subsystems C with a(C) ≥ b); the combinatorial game is standard (Hironaka's polyhedra game in the monomial case is elementary). Classify: sketched, standard.
- **Thm 16.6 (Main Theorem I, p.84).** D ⊂ ∇ smooth closed irreducible, π the blowup, ∇' the strict transform, D' = ∇' ∩ π^{-1}(D).
  (1) permissibility for every member of Y(i): follows from D ⊂ ∇ ⊂ Sing(Y(i)) ⊂ Sing(F) for all members; fine.
  (2) at ξ' ∈ π^{-1}(D)_cl ∖ D', (Inv_{ξ'}(Y'(0)),…) <_lex (Inv_ξ(Y(0)),…) — FALSE. (4) for D = ∇ (so ∇' = ∅), ℘^{posi}(F'(i;α)) empty at every ζ' ∈ π^{-1}(∇) for every F(i;α) ∈ Y(i) — FALSE.
  Counterexample (V1): E = (x²+y⁵,2), char 2. ∇ = {0} (§10). D = ∇, ∇' = ∅, so every ξ' ∈ π^{-1}(0) qualifies for (2) and (4). Take ξ' = origin of the chart y: E' = (x'²+y³, 2), ord_{ξ'} = 2, so Sing(E') ∋ ξ' and ℘^{posi}(E') is not "empty" at ξ' — (4) fails for F(0;·) = Ě itself (and for the AR member F(Y) = (y⁵,2) ↦ (y³,2), which is singular at the origin of Y'). For (2): Inv_{ξ'}(E') = (2,1,1) = Inv_0(E) (both edge algebras are (x̄): again all infinitely near points lie on x' = 0), and the AR members (y⁵,2) and (y³,2) on A¹ have identical edge data (edge-trivial: ℘(·,1) = (y³) resp. (y²), no order-1 element, Inv = (1,1); hiked versions (y⁵,5),(y³,3) both have Inv = (1,0,1)). Padding with (0) as instructed does not help: the strings are identical term by term. Hence no strict drop. The same happens at the next blowup (E'' = (x''²+y,2) is resolved only because ord dropped below 2 — a drop of the residual order ord ε: 5 → 3 → 1, a quantity that is not a component of Inv).
  (3) equality on ∇' — vacuous here.
- Lemma 16.7 (p.85): modifies the chain so that ord_D g(i) ≥ p^{e−i}: "by Th.(7.1) and Th.(7.2) of §13 we can modify the parameters y(i) so that ord_D(y(i)) ≥ p^{e−i} without changing any g(i)" — the modification y ↦ y − c changes g unless ε is changed too (as in Thm 10.6); and "ord_D(h(i)) ≥ ord_D(ε(i)) ≥ p^{e−i}" is asserted "by our choice of h(i) ∈ ℘̃(g(i))" — see §3: ord_D of a diff-product can be < ord_D ε in general; for the specific H♭ products it holds when each factor is a derivative of a monomial supported in I(D)-variables. Sketched.
- Lemma 16.8(1) (domino fall): see §3 — rests on the false transformation rule for ℘^{nega}. Direct check in V1: g(0) = x²+y⁵ = g(1)² + h(0) with g(1) = x, h(0) = y⁵ (the manuscript's H♭ gives exactly this: ε = y⁵ = y·(y²)², case (I), H♭ = ∂_y(ε)·∂_y^{(4)}(ε) = y⁴·y = y⁵). Blow up 0; at ξ' = origin of chart y, g'(1) = x' vanishes (ξ' ∈ Y'), so Lemma 16.8(1)'s hypothesis "g'(e) does not vanish at ξ'" fails and the lemma says nothing — but Cor. 16.9 (p.85) applies it to "ξ' ∈ π^{-1}(∇) ∖ ∇'" claiming "g(0)' does not vanish at ξ' because ξ' is not in the strict transform ∇' of ∇" — this identifies ∇ with the tail hypersurface {g(e) = 0} (Eq. (129): "∇ = {g(e) = 0}"), which is false whenever ∇ ≠ Y (here ∇ = {0}, Y = {x=0}). So Cor. 16.9 is false in V1: ξ' ∈ π^{-1}(∇) ∖ ∇' = π^{-1}(0), and g'(0) = x'²+y³ vanishes at ξ'.
- Lemma 16.10 (p.85–86): "Inv upper semi-continuous … equality by the theorems and lemmas of §13" — assertion.
- Lemma 16.11 (p.86): "the transform is an LL-chain headed by g'(0); the only important point is h'(i) ∈ ℘^{nega}(F̌'(i))" — vacuous by R2; the substantive point (that the transformed tail still generates the cotangent space / has maximal-contact behaviour at the new point) is not addressed. Hauser's kangaroo example (V3) shows what can go wrong one level down: at a3 the strict transform of the tail {x=0} still contains Sing(f3,2) but the coefficient ideal with respect to it has residual order 2 while the correct hypersurface {x + yz³(1+y) = 0} (the manuscript's own H♭ recipe at a3 produces exactly this tail: square part of ε = (y²z³+yz³)²) gives residual order 3 > 2 at a2.
- Proof of Thm 16.6 (p.86): "we can reduce the problem to the following case: the ideal exponents of Y(m−1) are all resolved by a finite sequence of permissible blowups whose centers are nowhere dense in the respective strict transforms of ∇ … This means that the blowup with center ∇ is permissible and the strict transform of ∇ turns to be empty. This means that Sing(F̌(m−1)) turns out to be empty." The induction hypothesis (resolution of the AR-reduced F_j(Y_{ji}) on the (n−1)-dimensional Y_{ji}) is invoked implicitly here; the inference "∇' = ∅ ⇒ Sing(F̌') = ∅" is Cor. 16.9, false (V1).
- Thm 16.13 (p.87): "By applying Th.(16.6) repeatedly but finitely many times" — finiteness rests on 16.6(2). With (2) false, no termination argument remains. The natural repair — append to the Inv-string the order of the AR-reduced exponent F(Y) (= residual order / shade) — is exactly the invariant that can increase (Moh's bound shade' ≤ shade + p^{e−1}; Hauser's kangaroo example V3: 2 → 3). So the gap is not local.
- §16.4 (pp.87–89), Θ(Ě,q(k)), (σΘ): definitions only; no statements proved; not used in §16.2–16.3.

## 12. Items checked and found correct or acceptable (so that the negative list is not read as "everything is wrong")

- Thm 3.15 and Prop. 3.26 (NE theorem): complete modulo typos.
- Thm 4.5: correct (and its proof idea with the auxiliary variable t is fine).
- Lemma 7.3, 7.4, 7.5: correct.
- Thm 7.1 (Inv non-increase): plausibly correct, classical (ridge non-decrease); proof sketched. V4 proxy test: 0 violations in 375 near points.
- Thm 6.3 (criterion for ℘^{nega}): proof correct (Cartier trick + Krull intersection + faithful flatness); the theorem is true — and it is what shows 1 ∈ ℘^{nega}.
- Thm 7.11(2) (integral closedness of ℘̃): proof fine (and trivial).
- Thm 9.18, Cor. 9.19: correct.
- Prop. 9.15 (lex well-ordering): correct.
- Thm 14.8 (single ℓ̄): correct.
- Lemmas 15.2, 15.3: correct.
- Thm 16.4 / Lemma 16.5: standard reductions, sketched, repairable.

## 13. Summary table of classifications

| # | Item (locator) | Status |
|---|---|---|
| R1 | §6.2 Eq.(44) p.30 | FALSE as a definition of the Inv-max focusing (equals S(Ê)); (43) existence/finite generation unproved |
| R2 | Def. 5.1 p.25 with Eq.(37) | ℘^{nega}(E,−a)_ξ = O_ξ for all a>0 (proved two ways) ⇒ Thm 9.2, 9.3, 7.11, 7.12, 14.6 (℘^{nega} part), Lemma 16.11 vacuous |
| R3 | Thm 7.8 Eq.(59) p.37; Rem. 7.7, 7.9 | FALSE (V1); invalid step in (60) |
| R4 | Thm 15.10 Step 2 p.80; Thm 15.9 dimension chain p.79 | FALSE (V1) |
| R5 | Thm 16.6(2),(4) p.84; Cor. 16.9 p.85 | FALSE (V1); Lemma 16.8 unsupported; Thm 16.13 termination unproved |
| R6 | Thm 10.3/10.4 p.60, Thm 10.6 p.61 | proofs invalid (non sequitur / incoherent); statement UNDETERMINED; monomial-curve counterexamples excluded by the Lemma in §8 |
| R7 | Thm 6.1 second sentence p.29 | FALSE for d not a multiple of the hike (Narasimhan, V2) |
| R8 | Thm 14.4 p.69, Lemma 14.5 p.70 | proofs break off mid-sentence |
| R9 | Thm 8.6/8.7 pp.44–45 | proofs incomplete (derivatives mix terms) |
| R10 | Cor. 7.15 p.40 | misstated (true for operators, false for values) |
| R11 | Lemma 5.6 p.27 | proof uses Leibniz inclusion backwards (conclusion true, trivially) |
| R12 | Lemma 3.14 p.12, Lemma 5.9(4) p.28, Def. 4.14 p.22, Thm 14.6 line 2 p.70 | garbled / type-mismatched |
| OK | Thm 3.15, 4.5, 6.3, 7.1 (modulo proof), 7.3–7.5, 9.15, 9.18, 14.8, 15.2, 15.3, 16.4 (strategy) | correct / plausible |
