diff --git a/abundance_terminal_threefolds_charp_v2.txt b/abundance_terminal_threefolds_charp_v2.txt
index 86820fb..d52e4bb 100644
--- a/abundance_terminal_threefolds_charp_v2.txt
+++ b/abundance_terminal_threefolds_charp_v2.txt
@@ -173,7 +173,7 @@ Over C, Miyaoka proved this case of threefold abundance by studying effective pl
 
 Nonvanishing and abundance in neighboring cases are due to Xu--Zhang [cite], Witaszek [cite], Zhang [cite], Xu [cite], and Posva [cite]. The remaining gap addressed here is a possible effective canonical divisor of numerical dimension one whose nef dimension is maximal. Theorem~thm:main rules out that possibility.
 
-The proof is in the tradition of the positive-characteristic foliation method of Xu--Zhang [cite]. It uses Langer's Bogomolov inequality [cite], surface abundance [cite], and Katz's Cartier descent [cite].
+The proof is in the tradition of the positive-characteristic foliation method of Xu--Zhang [cite]. It uses Langer's Bogomolov ineuality [cite], surface abundance [cite], and Katz's Cartier descent [cite].
 
 ## The proof map
 
@@ -186,7 +186,7 @@ D=sum_alpha m_alpha D_alpha
 ]
 with connected simple-normal-crossing support, primitive multiplicities, D nef and numerically trivial on each component, O_D(D) torsion, and a local relation omega_V^{ ⊗  p^b}~=O_V(B_*) supported on D. See Proposition~prop:prepared-cycle.
  Slopes. Prove that the tangent bundle T_V is strongly semistable for the slope c_1(-)HD/rk(-). Deduce c_2(V)Dge0 and uniform bounds on polar parts of sections of semistable bundles. See Proposition~prop:strong-semistability, Proposition~prop:polar-bounds, and Corollary~cor:no-scalar-poles.
- Jets. Study finite jets of line bundles along D. A three-row spectral sequence relates scalar, middle, and canonical jets. Prove the scalar last width is asymptotically p/(p+1) and consequently c_2(V)D=0. Prove a canonical formal root widehatomega_V~=widehatO_V(B_0). See Proposition~prop:scalar-widths and Proposition~prop:canonical-formal-root.
+ Jets. Study finite jets of line bundles along D. A three-row spectral sequence relates scalar, middle, and canonical jets. Prove the scalar last width is asymptotically p/(p+1) and consequently c_2(V)D=0. Prove a canonical formal root omegahat_V~=Ohat_V(B_0). See Proposition~prop:scalar-widths and Proposition~prop:canonical-formal-root.
  Laurent cohomology. Turn the jet estimates into a criterion: for a bundle satisfying an Euler-characteristic identity, bounded polar parts, and concentration of leading jets, every Laurent v Cech one-cocycle has a primitive. Apply this to one-forms, exact forms, and closed forms. See Theorem~thm:laurent-vanishing and Corollary~cor:form-vanishing.
  Cartier descent. Use the vanishing of Laurent cocycles to give every line bundle on the formal punctured neighborhood an integrable connection whose forms are Cartier-fixed. Cartier descent then shows that every line bundle is a pth power. Hence Pic(|D|,cR) is p-divisible. See Proposition~prop:picard-divisibility.
  Degree contradiction. Orders of Laurent units and intersection with H give a nonzero homomorphism
@@ -232,15 +232,15 @@ A variety is an integral separated scheme of finite type over a field. A threefo
 For a nef divisor L, the nef dimension n(L) is the dimension of its nef reduction. In particular, n(L)=dim X means that no L-trivial curve passes through a very general point. This is a different invariant from the numerical dimension nu(L).
 
 ## Completion and Laurent sheaves
-Let V be a smooth variety and D an effective Cartier divisor. We write widehatO_V for the completion along D, regarded as a sheaf on the Zariski space |D|. Set
+Let V be a smooth variety and D an effective Cartier divisor. We write Ohat_V for the completion along D, regarded as a sheaf on the Zariski space |D|. Set
 [
-R=widehatO_V(*D).
+R=Ohat_V(*D).
 ]
 Thus a section of cR is a formal function on a formal neighborhood of D that is allowed a finite pole along D. A line bundle on (|D|,cR) is a locally free rank-one cR-module in the Zariski topology. Its Picard group is denoted Pic(|D|,cR).
 
-For a vector bundle E, we write widehatwidehat EE for its completion and
+For a vector bundle E, we write EEhat for its completion and
 [
-E_{R}=widehatwidehat EE ⊗ _{widehatO_V}R.
+E_{R}=EEhat ⊗ _{Ohat_V}R.
 ]
 A Laurent v Cech cocycle is a v Cech cocycle with values in E_{R} on a finite affine cover adapted to D and E. A primitive is a cochain whose coboundary is the given cocycle.
 
@@ -471,9 +471,9 @@ Let Y be a normal projective threefold over an algebraically closed field of cha
 
 
 Proof. 
-Replace Z by Zcap|L|. For zin Z, put R=O_{Y,z}. Normality gives depth at least two, so H^1_{mathfrak m}frakm(R)=0. Every nonmaximal localization of R is a normal local ring of dimension at most two, hence Cohen--Macaulay. This implies H^2_{mathfrak m}frakm(R) has finite length. Present R=A/I with A regular local of dimension n. The height of I is n-3, and Auslander--Buchsbaum gives projective dimension n-3 at nonmaximal primes. Hence Ext_A^{n-2}(R,A) is supported only at the closed point and has finite length. Local duality identifies H^2_{mathfrak m}frakm(R) with its Matlis dual, up to completion.
+Replace Z by Zcap|L|. For zin Z, put R=O_{Y,z}. Normality gives depth at least two, so H^1_{m}m(R)=0. Every nonmaximal localization of R is a normal local ring of dimension at most two, hence Cohen--Macaulay. This implies H^2_{m}m(R) has finite length. Present R=A/I with A regular local of dimension n. The height of I is n-3, and Auslander--Buchsbaum gives projective dimension n-3 at nonmaximal primes. Hence Ext_A^{n-2}(R,A) is supported only at the closed point and has finite length. Local duality identifies H^2_{m}m(R) with its Matlis dual, up to completion.
 
-Let t_z be a local equation of L. Choose j so large that t_z^{j-1} kills H^2_{mathfrak m}frakm(R) for every zin Z. Then the restriction diagram
+Let t_z be a local equation of L. Choose j so large that t_z^{j-1} kills H^2_{m}m(R) for every zin Z. Then the restriction diagram
 [
 [column sep=small]
 0 arrow[r] &
@@ -821,7 +821,7 @@ mu_{min}(A' ⊗ (Q')^vee)
 ]
 contradicting (eq:slope-hom-vanishing). All iterated Frobenius pullbacks of T_V are therefore semistable.
 
-Finally, apply Langer's Bogomolov inequality cite[Theorem~3.2]{langer2004},[cite]: for a strongly semistable torsion-free sheaf with a nef tuple whose product is nonzero, Delta(E)Dge0 where Delta(E)=2rk(E)c_2(E)-(rk(E)-1)c_1(E)^2. Here the tuple is (H,D), which has H^2D>0. For T_V this gives
+Finally, apply Langer's Bogomolov ineuality cite[Theorem~3.2]{langer2004},[cite]: for a strongly semistable torsion-free sheaf with a nef tuple whose product is nonzero, Delta(E)Dge0 where Delta(E)=2rk(E)c_2(E)-(rk(E)-1)c_1(E)^2. Here the tuple is (H,D), which has H^2D>0. For T_V this gives
 [
 (6c_2(V)-2K_V^2)Dge0,
 ]
@@ -850,7 +850,7 @@ dim_kHom(G_1,G_2)lerk G_1·rk G_2.
 
 
 Proof. 
-First suppose G_1,G_2 are stable of slope zero. For a nonzero map, its image has slope at least zero as a quotient of G_1 and at most zero as a subsheaf of G_2. A positive-rank kernel makes the first inequality strict; an image of smaller rank than rk G_2 makes the second strict. Hence every nonzero map is full rank and rk G_1=rk G_2=n.
+First suppose G_1,G_2 are stable of slope zero. For a nonzero map, its image has slope at least zero as a quotient of G_1 and at most zero as a subsheaf of G_2. A positive-rank kernel makes the first ineuality strict; an image of smaller rank than rk G_2 makes the second strict. Hence every nonzero map is full rank and rk G_1=rk G_2=n.
 
 Its determinant is a global section of L=det(G_2) ⊗ det(G_1)^{-1} with deg L=0, so h^0(L)le1 by Lemma~lem:degree-zero-line-sections. If f,g were linearly independent, write det(sf+tg)=P(s,t)tau with tau a global generator and P homogeneous of degree n. Since f has full rank, Pne0; over the algebraically closed field, P vanishes at some (s:t)inPP^1(k). Then sf+tg is nonzero (by independence) but has zero determinant, a contradiction. Hence dimHomle1.
 
@@ -912,9 +912,9 @@ The argument computes finite jets and their ranks. Its two outputs are (a) a tri
 
 ## Finite pages and duality
 
-Write widehatO_V for the completion along D, regarded as a sheaf on |D|, and set
+Write Ohat_V for the completion along D, regarded as a sheaf on |D|, and set
 [
-R=widehatO_V(*D).
+R=Ohat_V(*D).
 ]
 Choose a finite cover by the restrictions to |D| of affine open subsets of V, refined so that D is principal and the bundles under consideration are free on each member. All intersections of these affine opens are affine, since V is separated. For a vector bundle E, let C_i^bullet(E) be the resulting v{C}ech complex with coefficients in the completion of E(iD). These complexes give an increasing filtration, indexed by iinZ, on the Laurent v{C}ech complex.
 
@@ -1047,7 +1047,7 @@ d_{e+1}ge p d_e,
 
 (d_e)/(M_e)↗ a_*in(0,1].
 
-A trivialization on M_eD would give, by Lemma~lem:scalar-jets, a nonzero section of O(M_eD)/cO, contrary to Corollary~cor:no-scalar-poles. Triviality at width one follows from the definition of r. Taking pth powers of local trivializing sections multiplies the gluing precision by p and gives d_{e+1}ge pd_e. Division by M_{e+1}=pM_e proves monotonicity and the positive limit. If r=1, the inequality 1le d_0<M_0=1 is a contradiction; hence r>1.
+A trivialization on M_eD would give, by Lemma~lem:scalar-jets, a nonzero section of O(M_eD)/cO, contrary to Corollary~cor:no-scalar-poles. Triviality at width one follows from the definition of r. Taking pth powers of local trivializing sections multiplies the gluing precision by p and gives d_{e+1}ge pd_e. Division by M_{e+1}=pM_e proves monotonicity and the positive limit. If r=1, the ineuality 1le d_0<M_0=1 is a contradiction; hence r>1.
 
 We will repeatedly use the following consequence of nilpotence. If a line bundle L on a finite thickening T of D is trivial on D, then its class has p-power order. Indeed its transition functions can be chosen in 1+J, where J is the nilpotent ideal of D in T. For p^N at least a nilpotence exponent, (1+x)^{p^N}=1 for xin J, so L^{ ⊗  p^N} is trivial. Multiplication by an integer prime to p is injective on such classes by B'ezout and surjective on their cyclic subgroups. It follows that
 
@@ -1086,7 +1086,7 @@ Between pages s_e and s_{e+1}=d_e+1 these are the only drops: there is no top ro
 [The canonical formal root]
 Every coefficient of B_* in (eq:canonical-p-power) is divisible by p^b. Writing B_*=p^bB_0 with B_0 integral, there is an isomorphism on the completion along D,
 
-widehatomega_V~=widehatO_V(B_0).
+omegahat_V~=Ohat_V(B_0).
 
 
 
@@ -1108,7 +1108,7 @@ nonzero for all sufficiently large s, uniformly in l. Indeed, at a component det
 ]
 while the new lower bound is P(l-s)+c_*, smaller for large s.
 
-Lemma~lem:scalar-jets shows that all these powered coefficients have one integral pole ratio t. The preceding inequality and the upper bound give a constant C, independent of s,l, such that
+Lemma~lem:scalar-jets shows that all these powered coefficients have one integral pole ratio t. The preceding ineuality and the upper bound give a constant C, independent of s,l, such that
 
 |t-Pl|le C,
 
@@ -1132,24 +1132,24 @@ T=(h_0-l+s)D-B_0.
 ]
 By (eq:canonical-ratio-bound), |h_0-l| is bounded independently of the sequence. Thus T contains nD for integers nto∞. Also M_Jmid t implies M_{J-b}mid h_0 once Jge b. The line bundle O(h_0D) is therefore trivial on d_{J-b}D, and d_{J-b}to∞ by (eq:width-bounds). Removing this twist shows that L=omega_V(-B_0) is trivial on arbitrarily large finite thickenings nD.
 
-Finally, choose the trivializations compatibly. Apply the stabilized-image argument in the proof of Lemma~lem:page-calculus to the spaces H^0(nD,L|_{nD}), additionally imposing restriction to D_{red}. The latter line bundle is trivial and its section space is one dimensional because D_{red} is connected, reduced, and projective. The image from every sufficiently large thickening contains a unit, hence is that full one-dimensional space. The surjective maps between stabilized images therefore lift a chosen nonzero section on D_{red} compatibly to all thickenings. Each lift is a unit (as may be checked after reduction), and their inverse limit trivializes widehatwidehat L.L. This gives (eq:canonical-formal-root).
+Finally, choose the trivializations compatibly. Apply the stabilized-image argument in the proof of Lemma~lem:page-calculus to the spaces H^0(nD,L|_{nD}), additionally imposing restriction to D_{red}. The latter line bundle is trivial and its section space is one dimensional because D_{red} is connected, reduced, and projective. The image from every sufficiently large thickening contains a unit, hence is that full one-dimensional space. The surjective maps between stabilized images therefore lift a chosen nonzero section on D_{red} compatibly to all thickenings. Each lift is a unit (as may be checked after reduction), and their inverse limit trivializes Lhat.L. This gives (eq:canonical-formal-root).
 
 
 ## The two endpoint residues and the limiting width
 
 Write B_0=sum_alpha b_{0,alpha}D_alpha, and define
 
-h=-Biglfloor(min_alphafrac{b_{0,alpha}}{m_alpha}Bigr),
+h=-Big⌊(min_alphafrac{b_{0,alpha}}{m_alpha}),
 
 q=1-h.
 
-The formal isomorphism of Proposition~prop:canonical-formal-root identifies the finite canonical jet lattices with scalar lattices having upper and lower bounds lD+B_0 and (l-s)D+B_0. All these finite quotients are algebraic sheaves supported on finite thickenings of D: the localized widehatO_V-linear isomorphism respects every nested divisor lattice, and each width-s quotient is killed by cI_D^s. Since widehatO_V/cI_D^swidehatO_V=O_{sD}, the induced map is O_{sD}-linear and compatible with the leading-layer projections.
+The formal isomorphism of Proposition~prop:canonical-formal-root identifies the finite canonical jet lattices with scalar lattices having upper and lower bounds lD+B_0 and (l-s)D+B_0. All these finite quotients are algebraic sheaves supported on finite thickenings of D: the localized Ohat_V-linear isomorphism respects every nested divisor lattice, and each width-s quotient is killed by cI_D^s. Since Ohat_V/cI_D^sOhat_V=O_{sD}, the induced map is O_{sD}-linear and compatible with the leading-layer projections.
 
 The exact canonical counterpart of the scalar rule is: for all sufficiently large s, a canonical jet at weight l with nonzero leading image has uniform integral scalar pole ratio
 
 t=l-h.
 
-To prove this, enlarge the two bounds to uniform multiples of D as in the preceding proof. A component detecting the leading image has ratio within a fixed distance of l, so for large s the enlarged quotient still detects it. Lemma~lem:scalar-jets gives a uniform integral ratio t. Set beta_0=min_alpha b_{0,alpha}/m_alpha. Fitting under every upper bound but not under the preceding layer is exactly the pair of inequalities
+To prove this, enlarge the two bounds to uniform multiples of D as in the preceding proof. A component detecting the leading image has ratio within a fixed distance of l, so for large s the enlarged quotient still detects it. Lemma~lem:scalar-jets gives a uniform integral ratio t. Set beta_0=min_alpha b_{0,alpha}/m_alpha. Fitting under every upper bound but not under the preceding layer is exactly the pair of ineualities
 [
 l-1+beta_0<tle l+beta_0.
 ]
@@ -1318,7 +1318,7 @@ This polar part has unbounded actual order. At some component of D an original c
 
 ## A vanishing criterion
 
-We use widehatwidehat EE for the completion of a bundle E along D, and E_{R}=widehatwidehat EE ⊗ _{widehatcO}R. The finite-cover, bounded-pole interpretation is the one used above.
+We use EEhat for the completion of a bundle E along D, and E_{R}=EEhat ⊗ _{cOhat}R. The finite-cover, bounded-pole interpretation is the one used above.
 
 
 For the prepared data and periods fixed above, let E be a vector bundle on V satisfying:
@@ -1355,7 +1355,7 @@ for a fixed C, with multiplicities at each length independent of j among integer
 No drop occurs before length d_e: translation by a unit of O(M_eD)|_{d_eD} identifies leading images with those at the unshifted stable position v. Choose local formal unit lifts t_lambda of this trivializing section of O(M_eD)|_{d_eD}, and write on overlaps
 [
 (t_lambda)/(t_mu)=1+b_{lambdamu},
- b_{lambdamu}incI_D^{d_e}widehatO_V,
+ b_{lambdamu}incI_D^{d_e}Ohat_V,
  cI_D=O_V(-D).
 ]
 Fix a constant C, and pick d_e<kle M_e+C. For large e, k<2d_e by (eq:laurent-width-input). Normalize local representatives sigma_lambda of a width-k jet at v+jM_e by putting alpha_lambda=sigma_lambda/t_lambda^j. These are local sections of E(vD)hat and satisfy
@@ -1365,13 +1365,13 @@ pmod{cI_D^kE(vD)hat}.
 
 Indeed (1+b_{lambdamu})^j=1+jb_{lambdamu} to this precision, for positive or negative j alike, because k<2d_e. In particular, the cochain alpha glues to width d_e.
 
-We next match alpha to a single global completed section beta in that untwisted lattice through width k-d_e. Every completed section and every formal lattice map restricts to the actual algebraic finite jets of (eq:jet-quotient): on each affine intersection this is the identity widehatwidehat A/(f^s)=A/(f^s).A/(f^s)=A/(f^s). These restrictions commute with the v Cech maps and with projection to leading layers. Start with beta_{<0}=0. After matching the first n depths, the sum beta_{<n} of the completed global sections already chosen satisfies
+We next match alpha to a single global completed section beta in that untwisted lattice through width k-d_e. Every completed section and every formal lattice map restricts to the actual algebraic finite jets of (eq:jet-quotient): on each affine intersection this is the identity Ahat/(f^s)=A/(f^s).A/(f^s)=A/(f^s). These restrictions commute with the v Cech maps and with projection to leading layers. Start with beta_{<0}=0. After matching the first n depths, the sum beta_{<n} of the completed global sections already chosen satisfies
 [
 alpha-beta_{<n}in C_{v-n}^0(E),
 
 ∂(alpha-beta_{<n})in C_{v-d_e}^1(E).
 ]
-The second inclusion persists because each subtracted section is global. Thus, for n<k-d_e, the residual is a finite jet at upper weight v-n of width at least d_e-n. The inequalities
+The second inclusion persists because each subtracted section is global. Thus, for n<k-d_e, the residual is a finite jet at upper weight v-n of width at least d_e-n. The ineualities
 
 d_e-nge 2d_e-M_e-O(1)>u_e,
  k-d_e<M_e/2-O(1)
@@ -1407,7 +1407,7 @@ Each interval has length less than M_e for large e. For any fixed residue modulo
 [
 H_e(i)ge#{tin T_e:tequiv ipmod{M_e}}.
 ]
-Summing over a period gives equality of the two sides by the Euler identity of Lemma~lem:page-calculus and property (i). The inequality is therefore equality at every residue. Equation~(eq:middle-distribution) now says H_{e+1} is exactly the distribution of T_e modulo pM_e. For each fixed integer i, the bands (eq:drop-bands) and d_eto∞ imply
+Summing over a period gives equality of the two sides by the Euler identity of Lemma~lem:page-calculus and property (i). The ineuality is therefore equality at every residue. Equation~(eq:middle-distribution) now says H_{e+1} is exactly the distribution of T_e modulo pM_e. For each fixed integer i, the bands (eq:drop-bands) and d_eto∞ imply
 
 g^1_{u_e}(i;E)=0 for all sufficiently large e.
 
@@ -1445,7 +1445,7 @@ so U_s^{x,1} stops increasing once x+s>B_l(x). Each increase from a source cut z
 Write F for absolute Frobenius and Ω=Ω_V^1. Let B^1,Z^1subset F_*Ω be the sheaves of exact and closed algebraic one-forms, with the Frobenius module structure.
 
 
-On a smooth affine chart with 'etale coordinates x_1,x_2,x_3 and a local equation f for D, put R=widehatwidehat A[1/f].A[1/f]. The monomials x^I=x_1^{I_1}x_2^{I_2}x_3^{I_3} with 0le I_j<p form a basis of R over R^p. Ordinary differentials and the Cartier isomorphism extend to this ring. The algebraic bundles B^1,Z^1 and their defining exact sequences extend to the corresponding Laurent exact and closed forms, with their Frobenius module structure. In particular,
+On a smooth affine chart with 'etale coordinates x_1,x_2,x_3 and a local equation f for D, put R=Ahat[1/f].A[1/f]. The monomials x^I=x_1^{I_1}x_2^{I_2}x_3^{I_3} with 0le I_j<p form a basis of R over R^p. Ordinary differentials and the Cartier isomorphism extend to this ring. The algebraic bundles B^1,Z^1 and their defining exact sequences extend to the corresponding Laurent exact and closed forms, with their Frobenius module structure. In particular,
 
 0→O_V→ F_*O_V
 → B^1→0,
@@ -1464,7 +1464,7 @@ The algebraic calculation is the p-basis form of Cartier's theorem cite[Theorem~
 
 For an 'etale algebra, the relative Frobenius square is a base change square: one checks this because the relative Frobenius is 'etale and induces isomorphisms on geometric fibers. The polynomial-coordinate monomial basis over pth powers therefore gives the asserted basis for A over A^p. The field k is perfect.
 
-Complete the p-power subring along f^p and use this finite basis. The f-adic and f^p-adic topologies on A coincide, and Frobenius identifies the completion of A^p with (widehatwidehat A)^p.A)^p. The basis thus persists after completion and after inverting f; in the latter step, 1/f=f^{p-1}/f^p.
+Complete the p-power subring along f^p and use this finite basis. The f-adic and f^p-adic topologies on A coincide, and Frobenius identifies the completion of A^p with (Ahat)^p.A)^p. The basis thus persists after completion and after inverting f; in the latter step, 1/f=f^{p-1}/f^p.
 
 Every k-derivation kills pth powers. Since each element has a unique finite expansion in the displayed basis with coefficients in R^p, its differential is determined by ordinary differentiation of those monomials. Conversely the coordinate derivations are defined by that rule. Hence Ω^1_{R/k} is free on dx_j.
 
@@ -1517,9 +1517,9 @@ Theorem~thm:laurent-vanishing now applies to Ω and B^1, including finite-dimens
 
 We work on the Zariski topological space |D|, with
 [
-widehatcO=widehatO_V,
+cOhat=Ohat_V,
 
-R=widehatO_V(*D).
+R=Ohat_V(*D).
 ]
 Here and throughout, a line bundle means a locally free module of rank one for the indicated sheaf of rings. Write Ω_{R}^j for the actual Laurent differential forms, and B^1subset Z^1subsetΩ_{R}^1 for the additive sheaves of exact and closed one-forms. Lemma~lem:laurent-cartier-algebra identifies these with the Laurent extensions of the algebraic Frobenius modules. In particular there is an exact sequence of additive sheaves
 
@@ -1713,17 +1713,17 @@ For the smooth affine chart and rings A,B,R above, B is a regular Noetherian rin
 Proof. 
 The Noetherian completion theorem gives that B is Noetherian and flat over A, and B/(f^n)=A/(f^n) cite[Lemmas~10.97.1--10.97.5]{stacks}. The element f belongs to the Jacobson radical of B: an element congruent to 1 modulo f has an inverse by the convergent geometric series, and more generally an element invertible modulo f is invertible in B cite[Lemma~10.96.6]{stacks}.
 
-Every maximal ideal mathfrak nfraknsubset B corresponds to a maximal ideal mathfrak mfrakmsubset A containing f, with mathfrak n=frakn=mathfrak mB.frakmB. For each s, completion modulo mathfrak m^sfrakm^s does nothing, since f^s already vanishes there. Hence
+Every maximal ideal nsubset B corresponds to a maximal ideal msubset A containing f, with n=n=mB.mB. For each s, completion modulo m^sfrakm^s does nothing, since f^s already vanishes there. Hence
 [
-B/mathfrak n^sfrakn^s~= A/mathfrak m^s,frakm^s,
+B/n^sfrakn^s~= A/m^s,m^s,
 
-widehatwidehat{B_B_{mathfrak n}frakn}~=widehatwidehat{A_A_{mathfrak m}frakm}.
+hathat{B_B_{n}n}~=hathat{A_A_{m}m}.
 ]
-The latter ring is regular, as A_{mathfrak m}frakm is a smooth local ring. A Noetherian local ring is regular if and only if its maximal-ideal completion is regular cite[Lemma~15.44.4]{stacks}, so every B_{mathfrak n}frakn is regular, and localization gives regularity at every prime of B.
+The latter ring is regular, as A_{m}m is a smooth local ring. A Noetherian local ring is regular if and only if its maximal-ideal completion is regular cite[Lemma~15.44.4]{stacks}, so every B_{n}n is regular, and localization gives regularity at every prime of B.
 
 A regular Noetherian ring is locally factorial cite[Lemma~15.123.2]{stacks}. Its finitely many irreducible components are disjoint, since each local ring is a domain. On each component choose a rational section of the given line on Spec R and take its Weil divisor. The closure of this finite Weil divisor on Spec B is Cartier by local factoriality. Doing this on all components gives the required extension. This is the Cartier--Weil correspondence on a regular scheme cite[II, S6]{hartshorne1977}; global unique factorization of B is not required.
 
-Let zin Ucap|D|. The extended line is free on a basic open Spec B_g containing the prime corresponding to z. Choose g_0in A whose image modulo f equals that of g. Then g_0(z)ne0. On the formal basic neighborhood coming from Spec A_{g_0}, its ring is B'=widehatwidehat{A_A_{g_0}}, and the image of g is invertible: modulo f it equals the invertible element g_0. The line is therefore free there and after inverting f. Finally, Frobenius is an abstract ring isomorphism from B onto B^p and from R onto R^p, because these rings are reduced. It identifies the corresponding formal basic neighborhoods. Thus the same proof applies to the power subrings.
+Let zin Ucap|D|. The extended line is free on a basic open Spec B_g containing the prime corresponding to z. Choose g_0in A whose image modulo f equals that of g. Then g_0(z)ne0. On the formal basic neighborhood coming from Spec A_{g_0}, its ring is B'=hathat{A_A_{g_0}}, and the image of g is invertible: modulo f it equals the invertible element g_0. The line is therefore free there and after inverting f. Finally, Frobenius is an abstract ring isomorphism from B onto B^p and from R onto R^p, because these rings are reduced. It identifies the corresponding formal basic neighborhoods. Thus the same proof applies to the power subrings.
 
 
 [Divisibility of the Laurent Picard group]
@@ -1828,7 +1828,7 @@ H^0(X,O_X(mK_X)) ⊗ _{k_0}k
 ~=
 H^0(X_k,O_{X_k}(mK_{X_k})).
 ]
-Their dimensions are equal, proving the required inequality over k_0. In particular kappa(X,K_X)ge1.
+Their dimensions are equal, proving the required ineuality over k_0. In particular kappa(X,K_X)ge1.
 
 Nefness and nu(K_X)=1 give kappa(X,K_X)=1. The positive-Kodaira-dimension abundance theorem cite[Theorem~1.6]{xu2024} also gives semiampleness over the original field. This completes the proof of Theorem~thm:main.