SamuelSchlesinger · Oct 31, 2026 · Oct 31, 2026
diff --git a/Complexity/Foundations/Analysis/RowCompression/FalseOverflow.lean b/Complexity/Foundations/Analysis/RowCompression/FalseOverflow.lean
@@ -46,7 +46,7 @@ after overflow, and the integrated compression theorem remain separate obligatio
 ## References
 
 * [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
-  Section 8.4, equation labelled `buf-false-charge`
+  Section 8.4, equation (8.12) on p. 48 (source label `buf-false-charge`)
   (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
 -/
 

diff --git a/Complexity/Foundations/Analysis/RowCompression/NoiseDecay.lean b/Complexity/Foundations/Analysis/RowCompression/NoiseDecay.lean
@@ -22,7 +22,7 @@ finite geometric-series bound. In particular, the absolute stability factor `C =
 paid for by `q = 1/64`, with total factor at most `7/9`.
 
 Composing this numerical bound with the actual first-overflow moment theorem removes the
-finite weighted-sum obligation in [OpenAI2026LogSpace, Section 8.4, `buf-noise-sum`]. Noise
+finite weighted-sum obligation in [OpenAI2026LogSpace, Section 8.4, (8.18)]. Noise
 with individual `p`-th moment budgets `(ε * q ^ d_i) ^ p` has actual overflow-tail budget
 `(ε * C * q / (1 - C * q)) ^ p`. All quantities may share an environment.
 
@@ -39,7 +39,8 @@ it does not assert that the absolute constant 28 also proves that relative stabi
 ## References
 
 * [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
-  Section 8.4, equation labelled `buf-noise-sum` and the following choice of noise decay
+  Section 8.4, equation (8.18) on p. 49 (source label `buf-noise-sum`) and the following
+  choice of noise decay
   (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
 -/
 

diff --git a/Complexity/Foundations/Analysis/RowCompression/OverflowBudget.lean b/Complexity/Foundations/Analysis/RowCompression/OverflowBudget.lean
@@ -18,7 +18,7 @@ moment budgets into a budget for the actual first-overflow tail. All arrays and
 depend on the same environment. No conditional rarity factor is applied to noise.
 
 This supplies the finite Minkowski step of [OpenAI2026LogSpace, Section 8.4], leading to
-`buf-noise-sum`. The individual prefix-noise estimates, propagation-weight bounds and the
+(8.18). The individual prefix-noise estimates, propagation-weight bounds and the
 uniform bound on their weighted budget sum remain separate obligations.
 
 ## Main results
@@ -29,7 +29,8 @@ uniform bound on their weighted budget sum remain separate obligations.
 ## References
 
 * [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
-  Section 8.4, proof paragraph leading to equation labelled `buf-noise-sum`
+  Section 8.4, proof paragraph leading to equation (8.18) on p. 49 (source label
+  `buf-noise-sum`)
   (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
 -/
 

diff --git a/Complexity/Foundations/Analysis/RowCompression/OverflowNoise.lean b/Complexity/Foundations/Analysis/RowCompression/OverflowNoise.lean
@@ -21,7 +21,7 @@ tail is bounded by the full weighted noise sum, pointwise in the environment. Th
 integrated moment comparison permits arbitrary dependence between noise and overflow.
 
 This is the pointwise aggregation step in [OpenAI2026LogSpace, Section 8.4], the paragraph
-leading to equation `buf-noise-sum`. The event is `IsFirstOverflow` of the actual compression
+leading to equation (8.18). The event is `IsFirstOverflow` of the actual compression
 run. No conditional rarity discount is claimed for noise. Prefix-noise budgets, Minkowski,
 propagation weights and convergence of their final series remain separate.
 
@@ -34,7 +34,8 @@ propagation weights and convergence of their final series remain separate.
 ## References
 
 * [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
-  Section 8.4, proof paragraph leading to equation labelled `buf-noise-sum`
+  Section 8.4, proof paragraph leading to equation (8.18) on p. 49 (source label
+  `buf-noise-sum`)
   (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
 -/
 

diff --git a/Complexity/Foundations/Probability/HeavyCount.lean b/Complexity/Foundations/Probability/HeavyCount.lean
@@ -49,7 +49,7 @@ integrated compression bound are separate steps.
 ## References
 
 * [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
-  Section 8.4, Lemma 8.4, equation labelled `buf-rarity`
+  Section 8.4, Lemma 8.4, equation (8.13) on p. 48 (source label `buf-rarity`)
   (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
 -/
 

diff --git a/Complexity/Foundations/Probability/PolynomialAtomFalseOverflow.lean b/Complexity/Foundations/Probability/PolynomialAtomFalseOverflow.lean
@@ -28,7 +28,7 @@ The resulting normalized bound uses the final state of the real compression recu
 the raw prefix at `j + 1`. The environment may jointly determine the increments, initial
 states, true rows, retained endpoints, and first overflow. No independence is assumed.
 
-This is the bounded-output integration of `buf-false-charge` in the proof of
+This is the bounded-output integration of (8.12) in the proof of
 [OpenAI2026LogSpace, Section 8.4, Proposition 8.5], on the fourth-moment route of issue #1721.
 It does not supply prefix mean/noise budgets, sum their geometric costs, prove post-overflow
 relative stability, or assert the complete integrated compression estimate.
@@ -43,7 +43,8 @@ relative stability, or assert the complete integrated compression estimate.
 ## References
 
 * [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
-  Section 8.4, equations labelled `buf-false-charge` and `buf-false-sum`
+  Section 8.4, equations (8.12) on p. 48 and (8.16) on p. 49 (source labels
+  `buf-false-charge` and `buf-false-sum`)
   (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
 -/