diff --git a/zero_distillable_entanglement_v2.txt b/zero_distillable_entanglement_v2.txt
index ffd5fa9..f56faa0 100644
--- a/zero_distillable_entanglement_v2.txt
+++ b/zero_distillable_entanglement_v2.txt
@@ -255,7 +255,7 @@ nonzero. This is the range criterion of Horodecki~[cite].
 A density operator (omega) on (C^a ⊗ C^b) belongs to
 (C if there exist positive integers (r,s), a vector
 (chiinC^r ⊗ C^s), and linear maps
-(L:calL:Mat rtoMat a), (M:calM:Mat stoMat b) such
+(L:L:Mat rtoMat a), (M:M:Mat stoMat b) such
 that
 
 omega=(L ⊗ M)(*),
@@ -328,11 +328,11 @@ and (lambda=sum_{r,s}norm{B_sA_r}_F^2). Since (Zne0),
 which is allowed.
 
 
-# A four-effect coherence inequality
+# A four-effect coherence ineuality
 
 
 The first step of the operational obstruction is a purely algebraic
-inequality about any state in (C and four arbitrary positive
+ineuality about any state in (C and four arbitrary positive
 local matrices. It compares the "coherence" between two equal-bit
 branches with the weights of branches in which the bits disagree. No
 pointwise normalization is assumed: later the matrices will be densities
@@ -359,7 +359,7 @@ le(sum_knorm{a_k}^2)^{1/2}(sum_knorm{b_k}^2)^{1/2}
 =√(tr H,tr J)).
 
 
-[Four-effect inequality]
+[Four-effect ineuality]
 
 Let (omegainC act on (C^p ⊗ C^q). For arbitrary
 (X_0,X_1succeq0) in (Mat p) and (Y_0,Y_1succeq0) in (Mat q),
@@ -404,7 +404,7 @@ This congruence is achievable inside the representation without changing
 (L by (L and (chi) by
 ((S^{-1} ⊗  I_s)chi). The output (omega) is unchanged, the
 pullbacks become (A_i'), the map is still CP, and
-(L'calL'circ T_r=(L T_r)circAd_{overlineoverline S}S) is
+(L'L'circ T_r=(L T_r)circAd_{overlineoverline S}S) is
 CP. Suppress the primes.
 
 Two block estimates.: 
@@ -459,7 +459,7 @@ Off-diagonal: (Z(v,w)) is bounded by (eq:reversed-block-bound) and
 (Z(w,v)) by (eq:direct-block-bound), and both right sides become
 (sqrt{p_{10}p_{01}}). Finally
 (sqrt{D_{00}}omegasqrt{D_{11}}
-=Z(v,v)+Z(v,w)+Z(w,v)+Z(w,w)), so the triangle inequality gives
+=Z(v,v)+Z(v,w)+Z(w,v)+Z(w,w)), so the triangle ineuality gives
 (eq:coherence).
 
 
@@ -486,7 +486,7 @@ Let (R) be the input state on (C^a ⊗ C^b).
 In fixed product bases, Eve's canonical purification is
 
 |Psi_R>=sum_h sqrt R,|h>_{AB}|h>_E,
- Econg A ⊗  B.
+ E~= A ⊗  B.
 
 Suppose the protocol is finite (only finitely many steps, all classical
 records finite) and produces bits (i,jin{0,1}) almost surely on
@@ -633,7 +633,7 @@ through to the actual input.
 
 Proof. 
 Set (a=dim A), (b=dim B), and attach untouched references
-(A_0cong A) and (B_0cong B). Run the protocol on the product of the
+(A_0~= A) and (B_0~= B). Run the protocol on the product of the
 normalized local probes
 
 |Phi_a>_{AA_0} ⊗ |Phi_b>_{BB_0},
@@ -669,8 +669,8 @@ A step sent by Alice makes the new record measurable with respect to
 (sigma(U)veeF_m; Bob's symmetric. A public-source step
 has the sampling kernel as its regular conditional law. Induction shows
 (Uperp VmidF_m for every (m), and passing to
-(F_∞=calF_∞=sigma(T)) in (L^1) gives
-(E[u(U)v(V)bbE[u(U)v(V)mid T]=E[u(U)bbE[u(U)mid T]E[v(V)bbE[v(V)mid T]).
+(F_∞=F_∞=sigma(T)) in (L^1) gives
+(E[u(U)v(V)E[u(U)v(V)mid T]=E[u(U)E[u(U)mid T]E[v(V)E[v(V)mid T]).
 
 Using regular conditional probability kernels on the standard Borel
 tape and transcript spaces~cite[Thm.~6.3--6.4]{Kallenberg2002} and
@@ -688,10 +688,10 @@ outcome. Countable extension in finite dimension
 cite[Thm.~6.14]{Kallenberg2002} constructs the complete-history positive
 matrix-valued reference measure. Let (W) denote the resulting reference
 measure on the history space; when a terminal quantum readout is used,
-its instrument refines this to (widehatwidehat WW), agreeing on the preterminal
+its instrument refines this to (WWhat), agreeing on the preterminal
 history.
 
-Push (widehatwidehat WW) forward to the defaulted-bit pair plus transcript.
+Push (WWhat) forward to the defaulted-bit pair plus transcript.
 Call the transport measures (W_{ij}). The probe transcript law
 (mu(S)=sum_{i,j}tr W_{ij}(S)) is a probability measure. Squeeze and
 Radon--Nikodym give matrix-entry densities (W_{ij}(t)) with
@@ -730,7 +730,7 @@ terminal instrument by clause~protocol:terminal.
 
 Let (N) be the event that some prescribed bit is missing before the
 default rule. On the actual input (R), clause~protocol:completion
-gives (tr[Kwidehatwidehat W(N)K^*]=0W(N)K^*]=0), so (Kwidehatwidehat W(N)K^*=0W(N)K^*=0), so
+gives (tr[KWhat(N)K^*]=0W(N)K^*]=0), so (KWhat(N)K^*=0W(N)K^*=0), so
 default bit tags correspond to zero filtered measure on the actual
 input. Therefore
 [
@@ -749,7 +749,7 @@ null set if necessary. Transposition preserves positivity, giving
 Let (R) and (|Psi_R>) be as in Lemma~lem:transcript, and
 let (|psi>in A ⊗  B ⊗ widetilde E) be any
 purification. There is a channel
-(R:calR:T( E)toT(E) mapping
+(R:R:T( E)toT(E) mapping
 (|psi>) to (|Psi_R>). If Alice and Bob run the same
 admitted protocol and Eve retains her purification and full transcript,
 (R ⊗ id_T) recovers the canonical output of
@@ -783,10 +783,10 @@ bound from the canonical to the general case.
 # Separation from an ideal secret bit
 
 
-The coherence inequality applies at each transcript. Take
+The coherence ineuality applies at each transcript. Take
 (S = the trace-norm distance from the actual transcript joint
 state to the ideal secret-bit transcript joint state. Two forces compete:
-correctness forces little mass in unequal-bit branches, and secrecy
+correctness forces little mass in uneual-bit branches, and secrecy
 forces the equal-bit branches to have matching Eve densities of at least
 half mass each. A Cauchy--Schwarz calculation turns these into incompatible
 requirements. Below (eta < 1/5) they cannot both hold.
@@ -845,7 +845,7 @@ For (eq:fidelity-lower), put (Z=sqrt H-sqrt J). Then
 (sgn(Z)) is a Hermitian contraction, so trace-norm
 duality and cyclicity give
 (norm{H-J}_1getr[sgn(Z)(H-J)]=tr[|Z|(sqrt H+sqrt J)]ge tr Z^2),
-where the last inequality uses
+where the last ineuality uses
 (<sqrt H+sqrt J>ge|<sqrt H-sqrt J>|
 =|z|) in an eigenvector of (Z). Finally
 (tr Z^2=tr H+tr J-2tr(sqrt Hsqrt J)) and
@@ -861,7 +861,7 @@ bit registers (K_A,K_B), and let its output (tau_{K_AK_BE'})
 retain in (E') an initial purification held by Eve and the complete
 public transcript. For every normalized (sigma_{E'}),
 
-norm{tau_{K_AK_BE'}-tfrac12sum_{i=0}^1
+norm{tau_{K_AK_BE'}-1/2sum_{i=0}^1
 |i,i>< i,i| ⊗ sigma_{E'}}_1gefrac15.
 
 Thus the traditional trace distance is at least (1/10), and
@@ -902,7 +902,7 @@ f(tau_{00}(t),tau_{11}(t))
 Apply Lemma~lem:coherence a.e. and scalar Cauchy--Schwarz after
 integration:
 
-mathfrak f:=frakf:=int f(tau_{00}(t),tau_{11}(t)),dmu(t)
+f:=f:=int f(tau_{00}(t),tau_{11}(t)),dmu(t)
 lesqrt{P_{00}P_{01}}+sqrt{P_{10}P_{11}}+2sqrt{P_{01}P_{10}}.
 
 No pointwise POVM normalization was used.
@@ -911,8 +911,8 @@ Let (eta) be the unhalved trace-norm distance to the ideal bit after
 the common transcript readout, and define
 (e=P_{01}+P_{10}),
 (q=intnorm{tau_{00}-tau_{11}}_1dmu),
-(a_i=intnorm{tau_{ii}-tfrac12sigma(t)}_1dmu).
-The unequal-bit blocks of the ideal state are zero. Additivity of trace
+(a_i=intnorm{tau_{ii}-1/2sigma(t)}_1dmu).
+The uneual-bit blocks of the ideal state are zero. Additivity of trace
 norm across bit blocks, then triangle within equal-bit blocks, gives
 
 eta=e+a_0+a_1, qle a_0+a_1=eta-e.
@@ -926,13 +926,13 @@ eleeta/2.
 
 
 Integration of (eq:fidelity-lower) gives
-(mathfrak ffrakfge(P_{00}+P_{11}-q)/2=(1-e-q)/2ge(1-eta)/2). On the
+(fge(P_{00}+P_{11}-q)/2=(1-e-q)/2ge(1-eta)/2). On the
 other side, Cauchy--Schwarz on the first two terms and AM-GM on the
 last give
 (sqrt{P_{00}P_{01}}+sqrt{P_{10}P_{11}}le√(e(1-e))) and
 (2sqrt{P_{01}P_{10}}le e), so
 
-(1-eta)/(2)lemathfrak ffrakfle√(e(1-e))+e, elefraceta2.
+(1-eta)/(2)lefrakfle√(e(1-e))+e, elefraceta2.
 
 If (eta<1/5), then (e<1/10), and on (0le ele1/10) the function
 (√(e(1-e))+e) is increasing with value (2/5) at (e=1/10).
@@ -966,8 +966,8 @@ retain an arbitrary initial purification and the full transcript.
       gap applies, possibly on different output spaces. Suppose their
       bit registers are kept fixed and their Eve registers embedded in
       a common (F) with embeddings (R_k If
-      (widehattau_ktotau) in trace norm, then
-      (norm{tau-tfrac12sum_i|i,i>< i,i| ⊗ sigma_F}_1
+      (tauhat_ktotau) in trace norm, then
+      (norm{tau-1/2sum_i|i,i>< i,i| ⊗ sigma_F}_1
       ge 1/5) for every normalized (sigma_F).
 
 
@@ -991,11 +991,11 @@ contradicting Theorem~thm:zero-key applied to the completed protocol
 with the local replacement appended.
 
 (3) Recovery channel (R_k transfers ideal bits:
-(R_k:calR_k:sigma|->sigma_{R_k} Contraction and the
+(R_k:R_k:sigma|->sigma_{R_k} Contraction and the
 per-protocol gap give
-(norm{widehattau_k-gamma_sigma}_1genorm{tau_k-gamma_{R_k(}}_1ge1/5).
+(norm{tauhat_k-gamma_sigma}_1genorm{tau_k-gamma_{R_k(}}_1ge1/5).
 Then
-(norm{tau-gamma_sigma}_1ge 1/5-norm{widehattau_k-tau}_1to 1/5).
+(norm{tau-gamma_sigma}_1ge 1/5-norm{tauhat_k-tau}_1to 1/5).
 No convergence on auxiliary probes and no factorization of (tau) is
 used.
 
@@ -1277,14 +1277,14 @@ relations (u_{ij}u_{kell}=u_{iell}u_{kj}).
 For (P_{a,b}=(u_{ij}:ige a or jge b)), (P_{a,b}) is prime
 and the chain
 (0=P_{4,4}subset P_{3,4}subset P_{2,4}subset P_{1,4}
-subset P_{1,3}subset P_{1,2}subset P_{1,1}subsetmathfrak mfrakm)
-is strict, so (htmathfrak mfrakmge7).
+subset P_{1,3}subset P_{1,2}subset P_{1,1}subsetfrakm)
+is strict, so (htfrakmge7).
 Let (ell_1,...,ell_6) be the six forms and
-(mathfrak a=(fraka=(ell_1,...,ell_6)). If the only common zero on
+(a=(a=(ell_1,...,ell_6)). If the only common zero on
 rank-one matrices were zero, the Nullstellensatz would give
-(√(mathfrak a)=fraka)=mathfrak mfrakm), making (mathfrak mfrakm) minimal over
+(√(a)=a)=m), making (m) minimal over
 a six-generator ideal. Krull's height theorem would give
-(htmathfrak mfrakmle6), contradiction. So some nonzero
+(htfrakmle6), contradiction. So some nonzero
 rank-one (xy^{T}) annihilates all six forms.
 
 
@@ -1420,7 +1420,7 @@ reduced.
 ## Quadratic evaluations via Galois
 
 Let (K be a splitting field of (f),
-(G=Gal(K/bbK/Q)). The evaluation matrix
+(G=Gal(K/K/Q)). The evaluation matrix
 (E_{j,alpha}=(t^{(j)})^alpha) for
 (1le jle20), (|alpha|le2) has column rank ten over
 (K Under the (S_{20}) action, (sigmain G) permutes
@@ -1585,7 +1585,7 @@ Take unit vectors (u_qinR^K for (qinQ, with
 (c_{qr}=u_q^{T}u_r). For each (q), ({P_i:iinI_q}) is
 a finite projective measurement on (C^D); zero projections allowed.
 Take the (I_q disjoint, (I=⊔_qcalI=⊔_qI_q,
-(n=|I|calI|). Suppose:
+(n=|I|I|). Suppose:
  (P_iP_j=P_jP_i) whenever (c_{qr}ne0);
  there is a real (kappa<Q/K) such that every
       (J⊆I with (tr(P_iP_j)>0) for all distinct
@@ -1670,7 +1670,7 @@ term zero, so for one (z_i=x_iy_i), (supp z) has no pair with
 Compressing to the diagonal subspace gives (B=sum_ell z^{(ell)}(z^{(ell)})^*).
 Complex Cauchy--Schwarz on supports:
 
-mathbf1^*Bbf1^*Bmathbf1=bf1=sum_ell|sum_i z_i^{(ell)}|^2
+mathbf1^*Bbf1^*Bmathbf1=1=sum_ell|sum_i z_i^{(ell)}|^2
 lekappasum_ellnorm{z^{(ell)}}^2=kappatr B
 <frac QKtr B=(DQ^2)/(K),
 
@@ -1745,7 +1745,7 @@ orthogonal eight-set into a forbidden positive-overlap choice.
 Set (p=257), (k=4p=1028), ([k]={1,...,k}). Define
 
 U={A⊆[k]:|A|=2p, 1in A},
-b=|U|=calU|=binom{1027}{513}=frac12binom{4p}{2p},
+b=|U|=U|=binom{1027}{513}=frac12binom{4p}{2p},
 
 and (s_A=k^{-1/2}(2mathbf1_bf1_{{hin A}}-1)_{h=1}^kinR^k
 Each (s_A) is a unit vector; by counting agreeing entries,
@@ -1762,8 +1762,8 @@ elementary multilinear methods.
 
 [Restricted intersections]
 
-If (F⊆calF⊆U has no two distinct sets with
-orthogonal associated vectors, then (|F|calF|le a_0=delta b).
+If (F⊆F⊆U has no two distinct sets with
+orthogonal associated vectors, then (|F|F|le a_0=delta b).
 
 
 Proof. 
@@ -1773,22 +1773,22 @@ give (1le|Acap B|le2p-1); orthogonality is excluded, so
 (|Acap A|=2pequiv0pmod p). Over (F_p) define
 (f_A(x)=prod_{hin A}(1-x_h^{p-1})=1-(sum_{hin A}x_h)^{p-1})
 in the identity (a^{p-1}=1) for (ainF_p^times). On indicators:
-(f_A(mathbf1_B)=bf1_B)=delta_{AB}).
+(f_A(mathbf1_B)=1_B)=delta_{AB}).
 Replace every positive power (x_h^{d}to x_h) for (d>1); evaluations
 on Boolean vectors are unchanged and degrees drop to (le p-1).
 Independence follows by evaluating any linear relation at each
 (mathbf1_Bbf1_B). The multilinear polynomials of degree (le p-1) have
 basis ({x^alpha:|alpha|le p-1}), size (a_0). So
-(|F|calF|le a_0).
+(|F|F|le a_0).
 
 
 [Fiber amplification]
 
 For (t=1,2,3), to ((A_1,...,A_t)inU^t associate the
 unit tensor (s_{A_1} ⊗ ... ⊗  s_{A_t}). If
-(R⊆calR⊆U^t contains no collection of (2^t)
+(R⊆R⊆U^t contains no collection of (2^t)
 distinct tuples whose associated tensors are pairwise orthogonal, then
-(|R|calR|le tdelta b^t).
+(|R|R|le tdelta b^t).
 
 
 Proof. 
@@ -1799,11 +1799,11 @@ Let (G be those (A) for which (R_A contains
 (2^{t-1}) pairwise orthogonal tuples. Two (A,BinG with
 (s_Aperp s_B) and disjoint fibers would produce (2^t) forbidden
 tuples; so (G has no orthogonal pair, forcing
-(|G|calG|le a_0=delta b). Fibers in (G have
+(|G|G|le a_0=delta b). Fibers in (G have
 (le b^{t-1}) elements; other fibers have (le(t-1)delta b^{t-1}).
 Summing gives
 [
-|R|calR|le(delta b)b^{t-1}+b(t-1)delta b^{t-1}=tdelta b^t.
+|R|R|le(delta b)b^{t-1}+b(t-1)delta b^{t-1}=tdelta b^t.
 ]
 
 
@@ -1816,9 +1816,9 @@ Q=, Q=b^3, K=k^3=1028^3=1{,}086{,}373{,}952,
 of size eight with pairwise orthogonal (u_q)'s. Lemma~%
 lem:fiber-amplification at (t=3) gives
 
-|R|calR|lekappa:=3delta Q=3a_0b^2
+|R|R|lekappa:=3delta Q=3a_0b^2
 
-for any (R⊆calR⊆Q with no orthogonal eight-set.
+for any (R⊆R⊆Q with no orthogonal eight-set.
 
 The analytic bound: central binomial
 (b=frac12binom{4p}{2p}ge 16^p/(2(4p+1))), and
@@ -1886,7 +1886,7 @@ non-membership questions get trivial measurements.
 
 
 S={S⊆Q:|S|=8calQ:|S|=8},
-L=|S|=calS|=binom Q8,
+L=|S|=S|=binom Q8,
 H=⊗_calH=⊗_{SinS}, D=4^L.
 
 For each (qinQ and outcome string
@@ -1919,7 +1919,7 @@ overlap factors over the tensor factors. If the questions represented
 by a positive-overlap label set contained an orthogonal eight-set (S),
 the six selected projections would violate Lemma~%
 lem:parity-obstruction on factor (S). So
-(|J|lekappa). The strict inequality is (eq:combinatorial-strict-bound).
+(|J|lekappa). The strict ineuality is (eq:combinatorial-strict-bound).
 
 
 [Combinatorial construction]
@@ -2045,7 +2045,7 @@ respectively, each nonzero.
 
 
 The combinatorial construction of Section~sec:combinatorial is
-proved by finite formulas and analytic inequalities. Two small
+proved by finite formulas and analytic ineualities. Two small
 programs verify its exact integer components. Neither is a premise of
 the proof.
 
@@ -2054,7 +2054,7 @@ verification/combinatorics_exact_checks.py uses only the
 Python standard library. It checks:
 (1) primality of (257) by trial division by the primes up to
      (√(257)), namely (2,3,5,7,11,13);
-(2) the intermediate binomial and power inequalities used to derive
+(2) the intermediate binomial and power ineualities used to derive
      (delta<2^{-65});
 (3) (3a_0K<b) and (3a_0b^2ge3).
 Its recorded output combinatorics_exact_checks.json stores