diff --git a/Complexity/Foundations/Analysis/RowCompression/FalseOverflow.lean b/Complexity/Foundations/Analysis/RowCompression/FalseOverflow.lean index 35d292f0d..3cbf1e5ec 100644 --- 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 index 4f3d85a27..62cb0907e 100644 --- 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 index 3f6a341b7..134561909 100644 --- 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 index ab58bd8b0..74b214ca9 100644 --- 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 index 168478352..8d7d2413e 100644 --- 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 index f9b4ba858..adf4d1fd5 100644 --- 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). -/