From 6e55f5aef84ecb309bf7204e8faa087c56dc31de Mon Sep 17 00:00:00 2001 From: Procyon_ Date: Thu, 13 Aug 2026 16:31:53 +0900 Subject: [PATCH 1/5] Add combined Heath-Brown--Guth-Maynard energy derivation --- blueprint/src/python/derived.py | 39 +++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/blueprint/src/python/derived.py b/blueprint/src/python/derived.py index 818ef1b..2dfe92b 100644 --- a/blueprint/src/python/derived.py +++ b/blueprint/src/python/derived.py @@ -1119,6 +1119,44 @@ def prove_improved_heath_brown_energy_estimate(): LVZ_star_hyp = ad.compute_LV_star(hypotheses, LVER_zeta_domain, zeta=True) bounds = ze.lver_to_energy_bound(LV_star_hyp, LVZ_star_hyp, Interval(frac(1,2), 1)) +def prove_heath_brown_guth_maynard_energy_estimate(): + hypotheses = Hypothesis_Set() + + for k in range(2, 5): + hypotheses.add_hypothesis(ad.get_raise_to_power_hypothesis(k)) + + hypotheses.add_hypothesis(lv.large_value_estimate_L2) + + literature_names = ( + "Heath-Brown large value energy region 2a", + "Heath-Brown large value energy region 2b", + "Guth--Maynard large value energy region 3", + ) + for name in literature_names: + matches = [h for h in literature if h.name == name] + if len(matches) != 1: + raise ValueError( + f"Expected exactly one literature hypothesis named {name!r}, " + f"found {len(matches)}" + ) + hypotheses.add_hypothesis(matches[0]) + + hypotheses.add_hypotheses(ad.lv_to_lver(hypotheses, zeta=False)) + + tau0 = Affine( + 0, + 2, + Interval(frac(2, 3), frac(3, 4)) + ) + hs = ze.lver_to_energy_bound( + hypotheses, + tau0, + debug=False + ) + for h in hs: + print(h.data) + return hs + def prove_zero_density_energy_2(): hypotheses = Hypothesis_Set() @@ -1398,6 +1436,7 @@ def prove_zero_density_energy_13(): def prove_all_zero_density_energy_estimates(): prove_heath_brown_energy_estimate() prove_improved_heath_brown_energy_estimate() + prove_heath_brown_guth_maynard_energy_estimate() prove_zero_density_energy_2() prove_zero_density_energy_3() prove_zero_density_energy_4() From 1adc4cd7804e90668a619ccab91bdfc6f3a560c1 Mon Sep 17 00:00:00 2001 From: Procyon_ Date: Thu, 13 Aug 2026 16:49:03 +0900 Subject: [PATCH 2/5] Document improved zero-density energy bound --- blueprint/src/chapter/zero_density_energy.tex | 43 ++++++++++++++++++- 1 file changed, 41 insertions(+), 2 deletions(-) diff --git a/blueprint/src/chapter/zero_density_energy.tex b/blueprint/src/chapter/zero_density_energy.tex index df95562..1ebe648 100644 --- a/blueprint/src/chapter/zero_density_energy.tex +++ b/blueprint/src/chapter/zero_density_energy.tex @@ -404,6 +404,43 @@ \section{Known additive energy bounds} for $4\sigma - 2 \le \tau' \le 3\sigma - 1$. The treatment is analogous to before, so we omit the proof. \end{proof} +\begin{theorem}\label{imp-energy-bound1} +For $2/3 \le \sigma \le 3/4$, one has +\begin{align*} +\A^*(\sigma) &\le \frac{10 - 11\sigma}{(2 - \sigma)(1 - \sigma)}, && \frac{2}{3} \le \sigma \le \frac{5}{7},\\ +\A^*(\sigma) &\le \frac{3(25 - 27\sigma)}{8(2 - \sigma)(1 - \sigma)}, && \frac{5}{7} \le \sigma \le \frac{315}{433},\\ +\A^*(\sigma) &\le \frac{2(45 - 44\sigma)}{(2\sigma + 15)(1 - \sigma)}, && \frac{315}{433} \le \sigma \le \frac{3}{4}. +\end{align*} +\end{theorem} + +\derived +\code{prove_heath_brown_guth_maynard_energy_estimate()} + +\begin{proof}\uses{zeroe-large-cor-0, l2-mvt, hbt, hb-energy-simp, gm-3, power-energy} +Take $\tau_0=2$ in Corollary \ref{zeroe-large-cor-0}. The $\LV^*_{\zeta}$ supremum is then empty, so it remains to bound $\rho^*/\tau$ for $(\sigma,\tau,\rho,\rho^*,s)\in\Energy$ with $2\leq\tau\leq4$. The relevant large-value-energy region is obtained by intersecting the $L^2$ large-value consequence from \Cref{l2-mvt}, the Heath--Brown regions \Cref{hbt,hb-energy-simp}, the third Guth--Maynard energy relation \Cref{gm-3}, and their $k=2,3,4$ power transforms from \Cref{power-energy}. Starting from the $L^2$ estimate and Heath--Brown region 2b, adding either \Cref{hbt} or \Cref{gm-3} alone is insufficient; the claimed bounds arise when both are included in the full intersection. + +Exact polyhedral elimination of this intersection, as implemented by \code{prove_heath_brown_guth_maynard_energy_estimate()}, gives the three bounds in the statement. The first two transition profiles can be seen explicitly. They share +\[ +\tau=2(2-\sigma), \qquad \rho=6(1-\sigma), +\] +while the two $k=2$ branches of the third Guth--Maynard energy relation give respectively +\[ +\rho^*=2(10-11\sigma), \qquad \rho^*=\frac{3(25-27\sigma)}{4}. +\] +Their difference is $(7\sigma-5)/4$, so they cross exactly at $\sigma=5/7$. Consequently the corresponding values of $\rho^*/\tau$ are +\[ +\frac{10-11\sigma}{2-\sigma} +\qquad\text{and}\qquad +\frac{3(25-27\sigma)}{8(2-\sigma)}. +\] +The second and third pieces meet because +\[ +\frac{3(25-27\sigma)}{8(2-\sigma)} +=\frac{2(45-44\sigma)}{2\sigma+15} +\] +at $\sigma=315/433$. These extremal profiles explain the two transition points; the upper bounds themselves follow from the exact calculation using the full intersection described above. +\end{proof} + Using Theorem \ref{guth-maynard-lvt}, it is possible to obtain improved energy estimates near $\sigma = 3/4$, which are given by the next two theorems. \begin{theorem}\label{imp-energy-bound2} @@ -1127,9 +1164,11 @@ \section{Known additive energy bounds} \hline $\dfrac{10 - 11\sigma}{(2 - \sigma)(1 - \sigma)}$ & $\dfrac{1}{2} \leq \sigma \le \dfrac{2}{3} = 0.6666\ldots$ & Theorem \ref{hb-energy-bound}\\ \hline - $\dfrac{18 - 19\sigma}{(4 - 2\sigma)(1 - \sigma)}$ & $\dfrac{2}{3} \leq \sigma \le \dfrac{7}{10} = 0.7$ & Theorem \ref{hb-energy-bound}\\ + $\dfrac{10 - 11\sigma}{(2 - \sigma)(1 - \sigma)}$ & $\dfrac{2}{3} \leq \sigma \le \dfrac{5}{7} = 0.7142\ldots$ & Theorem \ref{imp-energy-bound1}\\ + \hline + $\dfrac{3(25 - 27\sigma)}{8(2 - \sigma)(1 - \sigma)}$ & $\dfrac{5}{7} \leq \sigma \le \dfrac{626 - \sqrt{3301}}{785} = 0.7242\ldots$ & Theorem \ref{imp-energy-bound1}\\ \hline - $\dfrac{5(18 - 19\sigma)}{2(5\sigma + 3)(1 - \sigma)}$ & $\dfrac{7}{10} \leq \sigma \le \dfrac{539 - \sqrt{42121}}{460} = 0.7255\ldots$ & Theorem \ref{imp-energy-bound2}\\ + $\dfrac{5(18 - 19\sigma)}{2(5\sigma + 3)(1 - \sigma)}$ & $\dfrac{626 - \sqrt{3301}}{785} \leq \sigma \le \dfrac{539 - \sqrt{42121}}{460} = 0.7255\ldots$ & Theorem \ref{imp-energy-bound2}\\ \hline $\dfrac{2(45 - 44\sigma)}{(2\sigma + 15)(1 - \sigma)}$ & $\dfrac{539 - \sqrt{42121}}{460} \leq \sigma \le \dfrac{165}{226} = 0.7300\ldots$ & Theorem \ref{imp-energy-bound2}\\ \hline From fea1d5a685178f1e7849f1880a84a0df6eac15de Mon Sep 17 00:00:00 2001 From: Procyon_ Date: Thu, 13 Aug 2026 17:25:36 +0900 Subject: [PATCH 3/5] Coalesce identical zero-density energy pieces --- blueprint/src/python/zero_density_energy_estimate.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/blueprint/src/python/zero_density_energy_estimate.py b/blueprint/src/python/zero_density_energy_estimate.py index a835bca..2344aee 100644 --- a/blueprint/src/python/zero_density_energy_estimate.py +++ b/blueprint/src/python/zero_density_energy_estimate.py @@ -323,7 +323,11 @@ def lver_to_energy_bound( # Take maximum bounds = [(f[0], f[1]) for f in fns] - sup = RF.max(bounds, sigma_interval) + sup = RF.max( + bounds, + sigma_interval, + track_dependencies=False + ) return [ derived_zero_density_energy_estimate( # Remember to divide by (1 - \\sigma) From e5e4938e16ea89f869ad206f0f64de211d3eb675 Mon Sep 17 00:00:00 2001 From: chaemin333-max Date: Thu, 13 Aug 2026 09:48:15 +0000 Subject: [PATCH 4/5] Align the new energy derivation with repository conventions Use literature.find_hypothesis() for the three literature energy regions, matching the surrounding derived proofs, and compact the tau0 and lver_to_energy_bound calls in the same style. Match the existing wording of the zeta supremum in the blueprint proof ("now trivial" rather than "empty"), and add a lead-in sentence before the new theorem. Update the hardcoded current-best list in zero_density_energy_plot() so that the plotted envelope agrees with the current-best table. --- blueprint/src/chapter/zero_density_energy.tex | 4 ++- blueprint/src/python/derived.py | 31 +++++-------------- blueprint/src/python/visualizations.py | 4 ++- 3 files changed, 13 insertions(+), 26 deletions(-) diff --git a/blueprint/src/chapter/zero_density_energy.tex b/blueprint/src/chapter/zero_density_energy.tex index 1ebe648..889b4db 100644 --- a/blueprint/src/chapter/zero_density_energy.tex +++ b/blueprint/src/chapter/zero_density_energy.tex @@ -404,6 +404,8 @@ \section{Known additive energy bounds} for $4\sigma - 2 \le \tau' \le 3\sigma - 1$. The treatment is analogous to before, so we omit the proof. \end{proof} +Combining the Heath--Brown relations with the third Guth--Maynard relation (Lemma \ref{gm-3}) improves Theorem \ref{hb-energy-bound} in the range $2/3 \le \sigma \le 3/4$. + \begin{theorem}\label{imp-energy-bound1} For $2/3 \le \sigma \le 3/4$, one has \begin{align*} @@ -417,7 +419,7 @@ \section{Known additive energy bounds} \code{prove_heath_brown_guth_maynard_energy_estimate()} \begin{proof}\uses{zeroe-large-cor-0, l2-mvt, hbt, hb-energy-simp, gm-3, power-energy} -Take $\tau_0=2$ in Corollary \ref{zeroe-large-cor-0}. The $\LV^*_{\zeta}$ supremum is then empty, so it remains to bound $\rho^*/\tau$ for $(\sigma,\tau,\rho,\rho^*,s)\in\Energy$ with $2\leq\tau\leq4$. The relevant large-value-energy region is obtained by intersecting the $L^2$ large-value consequence from \Cref{l2-mvt}, the Heath--Brown regions \Cref{hbt,hb-energy-simp}, the third Guth--Maynard energy relation \Cref{gm-3}, and their $k=2,3,4$ power transforms from \Cref{power-energy}. Starting from the $L^2$ estimate and Heath--Brown region 2b, adding either \Cref{hbt} or \Cref{gm-3} alone is insufficient; the claimed bounds arise when both are included in the full intersection. +Take $\tau_0=2$ in Corollary \ref{zeroe-large-cor-0}. The $\LV^*_{\zeta}$ supremum is now trivial, so it remains to bound $\rho^*/\tau$ for $(\sigma,\tau,\rho,\rho^*,s)\in\Energy$ with $2\leq\tau\leq4$. The relevant large-value-energy region is obtained by intersecting the $L^2$ large-value consequence from \Cref{l2-mvt}, the Heath--Brown regions \Cref{hbt,hb-energy-simp}, the third Guth--Maynard energy relation \Cref{gm-3}, and their $k=2,3,4$ power transforms from \Cref{power-energy}. Starting from the $L^2$ estimate and Heath--Brown region 2b, adding either \Cref{hbt} or \Cref{gm-3} alone is insufficient; the claimed bounds arise when both are included in the full intersection. Exact polyhedral elimination of this intersection, as implemented by \code{prove_heath_brown_guth_maynard_energy_estimate()}, gives the three bounds in the statement. The first two transition profiles can be seen explicitly. They share \[ diff --git a/blueprint/src/python/derived.py b/blueprint/src/python/derived.py index 2dfe92b..e0f9f63 100644 --- a/blueprint/src/python/derived.py +++ b/blueprint/src/python/derived.py @@ -1125,34 +1125,17 @@ def prove_heath_brown_guth_maynard_energy_estimate(): for k in range(2, 5): hypotheses.add_hypothesis(ad.get_raise_to_power_hypothesis(k)) + # Add classical and literature Large value estimates hypotheses.add_hypothesis(lv.large_value_estimate_L2) + hypotheses.add_hypothesis(literature.find_hypothesis(name="Heath-Brown large value energy region 2a")) + hypotheses.add_hypothesis(literature.find_hypothesis(name="Heath-Brown large value energy region 2b")) + hypotheses.add_hypothesis(literature.find_hypothesis(name="Guth--Maynard large value energy region 3")) - literature_names = ( - "Heath-Brown large value energy region 2a", - "Heath-Brown large value energy region 2b", - "Guth--Maynard large value energy region 3", - ) - for name in literature_names: - matches = [h for h in literature if h.name == name] - if len(matches) != 1: - raise ValueError( - f"Expected exactly one literature hypothesis named {name!r}, " - f"found {len(matches)}" - ) - hypotheses.add_hypothesis(matches[0]) - + # Convert all large value estimates -> large value energy region hypotheses.add_hypotheses(ad.lv_to_lver(hypotheses, zeta=False)) - tau0 = Affine( - 0, - 2, - Interval(frac(2, 3), frac(3, 4)) - ) - hs = ze.lver_to_energy_bound( - hypotheses, - tau0, - debug=False - ) + tau0 = Affine(0, 2, Interval(frac(2,3), frac(3,4))) + hs = ze.lver_to_energy_bound(hypotheses, tau0, debug=False) for h in hs: print(h.data) return hs diff --git a/blueprint/src/python/visualizations.py b/blueprint/src/python/visualizations.py index cf01791..bf2df88 100644 --- a/blueprint/src/python/visualizations.py +++ b/blueprint/src/python/visualizations.py @@ -259,7 +259,9 @@ def zero_density_energy_plot(): # List of new derived estimates so far. TODO: replace with actual derivations energy_estimates = [ (RF.parse("1000000"), Interval(frac(1,2), 1)), # default - (RF.parse("5 * (18 - 19 * x) / (2 * (5 * x + 3) * (1 - x))"), Interval(frac(7,10), 0.7255)), + (RF.parse("(10 - 11 * x) / ((2 - x) * (1 - x))"), Interval(frac(2,3), frac(5,7))), + (RF.parse("3 * (25 - 27 * x) / (8 * (2 - x) * (1 - x))"), Interval(frac(5,7), 0.7242)), + (RF.parse("5 * (18 - 19 * x) / (2 * (5 * x + 3) * (1 - x))"), Interval(0.7242, 0.7255)), (RF.parse("2 * (45 - 44 * x) / ((2 * x + 15) * (1 - x))"), Interval(0.7255, 0.73)), (RF.parse("(457 - 546 * x) / (2 * (61 - 58 * x) * (1 - x))"), Interval(0.73, 0.7373)), (RF.parse("5 * (18 - 19 * x) / (2 * (5 * x + 3) * (1 - x))"), Interval(0.7373, frac(42,55))), From d916558528ce35bd85bb09dc1170639d73312155 Mon Sep 17 00:00:00 2001 From: Min Chae Date: Thu, 13 Aug 2026 20:02:36 +0900 Subject: [PATCH 5/5] Use exact crossover in zero-density energy plot --- blueprint/src/python/visualizations.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/blueprint/src/python/visualizations.py b/blueprint/src/python/visualizations.py index bf2df88..740a292 100644 --- a/blueprint/src/python/visualizations.py +++ b/blueprint/src/python/visualizations.py @@ -257,11 +257,12 @@ def zero_density_energy_plot(): ze.add_trivial_zero_density_energy_estimates(hypotheses) # List of new derived estimates so far. TODO: replace with actual derivations + crossover = (626 - math.sqrt(3301)) / 785 energy_estimates = [ (RF.parse("1000000"), Interval(frac(1,2), 1)), # default (RF.parse("(10 - 11 * x) / ((2 - x) * (1 - x))"), Interval(frac(2,3), frac(5,7))), - (RF.parse("3 * (25 - 27 * x) / (8 * (2 - x) * (1 - x))"), Interval(frac(5,7), 0.7242)), - (RF.parse("5 * (18 - 19 * x) / (2 * (5 * x + 3) * (1 - x))"), Interval(0.7242, 0.7255)), + (RF.parse("3 * (25 - 27 * x) / (8 * (2 - x) * (1 - x))"), Interval(frac(5,7), crossover)), + (RF.parse("5 * (18 - 19 * x) / (2 * (5 * x + 3) * (1 - x))"), Interval(crossover, 0.7255)), (RF.parse("2 * (45 - 44 * x) / ((2 * x + 15) * (1 - x))"), Interval(0.7255, 0.73)), (RF.parse("(457 - 546 * x) / (2 * (61 - 58 * x) * (1 - x))"), Interval(0.73, 0.7373)), (RF.parse("5 * (18 - 19 * x) / (2 * (5 * x + 3) * (1 - x))"), Interval(0.7373, frac(42,55))),