Burgers: from a unique formal stream to a certified front

Static snapshot of Burgers.lean · source revision dated 2026-10-19T10:47:08.000Z · source SHA-256 059b449bc88c37e728db4f0a050282016ce0e9fce6d79d4d2787a0d34cb9706d. Saved results, shown as recorded. Each result is shown as its check last saved it, compared only with this saved source and not with the reader's Lean environment. Nothing was checked or run to show it. This static page does not check or update results.

import Mathlib
L1–1
import Gimle.Asgard.Examples.BurgersSquare
L2–2
import Gimle.Asgard.Examples.PolynomialHeat
L3–3
import Gimle.Asgard.Examples.BurgersFront
L4–4
import Gimle.Asgard.Streams.ColeHopf
L5–5

The viscous Burgers equation is

ut=−u ux+ν uxx.u_t = -u\,u_x + \nu\,u_{xx}.

We first treat it as a formal power series in tt and xx: exact rational coefficients, with no convergence assumed. We then certify convergence and bounds for one particular Cole–Hopf front.

Proved here. Formal uniqueness at ν=110\nu = \tfrac{1}{10} for every profile, circuit reconstruction from x2x^2, and the first coefficients. For the front from φ(0,x)=1+e−x\varphi(0,x)=1+e^{-x} at ν=12\nu=\tfrac12, the series converges on ∣t∣≤16|t|\le\tfrac16, ∣x∣≤18|x|\le\tfrac18. Its 16×1616\times16 truncation has error at most 116384\tfrac{1}{16384}; its sum is 1/(1+ex−t/2)1/(1+e^{x-t/2}) and lies in [25,35][\tfrac25,\tfrac35] on that box.

Refuted and unresolved. The front's tighter upper bound 2750\tfrac{27}{50} is refuted at a corner of the box. The decider's 10−610^{-6} truncation request on the same box remains unknown: failure to certify it is not a refutation.

Scope. The divergence discussion for the x2x^2 series is unformalized; its finite numerical evidence is not a proof. The front's convergence and closed-form identification apply only on the certified box. This notebook does not prove that the closed form solves the real PDE, or address shocks or the limit ν→0\nu\to0.

Route. Construct the formal stream, inspect its coefficients and limits, certify the front's series, identify its sum, then inspect automated bounds. More Burgers fronts applies the decider to two other cases.

Construct the unique formal stream

At ν=110\nu=\tfrac{1}{10}, equal initial profiles determine equal formal streams. The circuit reconstructs exactly the stream from x2x^2; this is formal uniqueness, with no convergence hypothesis or conclusion.3 Kernel checked 3 As recorded

Read the causal recurrence

Each new time coefficient depends only on earlier time degrees. Picard iteration constructs the stream, and induction establishes uniqueness; the library's general result allows every rational viscosity.No claim observations

Write u=∑n,kcn,k tnxku = \sum_{n,k} c_{n,k}\, t^n x^k and [tnxk][t^n x^k] for cn,kc_{n,k}. The equation says

(n+1) cn+1,k=ν (k+2)(k+1) cn,k+2−∑i+j=n ∑a+b=kci,a (b+1) cj,b+1,(n+1)\, c_{n+1,k} = \nu\,(k+2)(k+1)\, c_{n,k+2} - \sum_{i+j=n}\ \sum_{a+b=k} c_{i,a}\,(b+1)\,c_{j,b+1},

and the right-hand side involves only tt-degrees ≤n\le n: the equation is causal in tt. The library proves this once for any causal right-hand side (the formal Cauchy–Kowalevski lemma): Picard iteration along tt — integrate the right-hand side of the previous iterate from the profile, again and again — constructs a solution, and strong induction on the tt-degree shows there is no other with the same profile. Burgers is an instance because sums, spatial derivatives and Cauchy products (products of series) are causal.

Read the circuit interface

The circuit integrates the Burgers right-hand side from the boundary profile. Its relation states that its candidate is the formal solution.No claim observations
namespace Notebook.Burgers
L69–69
open Gimle.Asgard.Streams Gimle.Asgard.Streams.Burgers Gimle.Asgard.Examples.BurgersSquare
L70–70

The right-hand side −u ux+ν uxx-u\,u_x + \nu\,u_{xx} is a stream expression in the unknown: two spatial derivatives, a Cauchy product, two constants. The library compiles it, integrates it along tt from the boundary profile, and proves that the resulting circuit relates [u,profile,_][u, \text{profile}, \_] to [rhs u,u][\text{rhs}\,u, u] exactly when uu is the formal solution. The third input is unused; it is there because the heat circuit has the same shape.

In the Lean below, rhs basis ν u is the right-hand side as a function of the stream u; stream basis ν b is the formal solution from the boundary stream b; ofPoly .ogf p reads the polynomial p as a stream of ordinary coefficients (the .ogf basis; .egf stores n! k!n!\,k! times them); and an index Finsupp.single 0 n + Finsupp.single 1 k is the monomial tnxkt^n x^k, axis 00 being tt. MvPolynomial.X 1 ^ 2 is x2x^2. The library fixes ν := 1/10 for its example, which is why the restatements below typecheck with 1 / 10 written out.

Check uniqueness and reconstruction

Two formal streams satisfying the equation with the same t=0t = 0 slice are equal. The claim is for ν=110\nu = \tfrac{1}{10} and either basis; the library's theorem is for every ν\nu.3 Kernel checked 3 As recorded

Theorem uniqueness Kernel checkedAs recorded L96–101

Namespace Notebook.Burgers

Two formal Burgers solutions with the same profile are the same stream.

Statement
(basis  :  Basis)  (a  b  :  Stream  2)(\text{basis}\;:\;\text{Basis})\;(\text{a}\;\text{b}\;:\;\text{Stream}\;2)  (ha  :  derivative  basis  0  a  =  rhs  basis  (1  /  10)  a)\;(\text{ha}\;:\;\text{derivative}\;\text{basis}\;0\;\text{a}\;=\;\text{rhs}\;\text{basis}\;(1\;/\;10)\;\text{a})  (hb  :  derivative  basis  0  b  =  rhs  basis  (1  /  10)  b)\;(\text{hb}\;:\;\text{derivative}\;\text{basis}\;0\;\text{b}\;=\;\text{rhs}\;\text{basis}\;(1\;/\;10)\;\text{b})  (slice  :  ∀  m  :  Index  2,  m  0  =  0  →  a  m  =  b  m)  :  a  =  b\;(\text{slice}\;:\;\forall \;\text{m}\;:\;\text{Index}\;2,\;\text{m}\;0\;=\;0\;\to \;\text{a}\;\text{m}\;=\;\text{b}\;\text{m})\;:\;\text{a}\;=\;\text{b}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- Two formal Burgers solutions with the same profile are the same stream. -/
theorem uniqueness (basis : Basis) (a b : Stream 2)
    (ha : derivative basis 0 a = rhs basis (1 / 10) a)
    (hb : derivative basis 0 b = rhs basis (1 / 10) b)
    (slice : ∀ m : Index 2, m 0 = 0 → a m = b m) : a = b := by
  exact formal_unique basis (1 / 10) a b ha hb slice

Theorem circuit_reconstructs Kernel checkedAs recorded L103–110

Namespace Notebook.Burgers

The compiled circuit reconstructs the constructed stream from x² …

Statement
(unused  :  Stream  2)  :(\text{unused}\;:\;\text{Stream}\;2)\;:  (circuit  .ogf  (1  /  10)).Rel\;(\text{circuit}\;.\text{ogf}\;(1\;/\;10)).\text{Rel}  ![stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2)),\;!\text{[}\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2)),  ofPoly  .ogf  (MvPolynomial.X  1  ^  2),  unused]\;\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2),\;\text{unused}\text{]}  ![rhs  .ogf  (1  /  10)  (stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2))),\;!\text{[}\text{rhs}\;.\text{ogf}\;(1\;/\;10)\;(\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2))),  stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2))]\;\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2))\text{]}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 8 lines
/-- The compiled circuit reconstructs the constructed stream from `x²` … -/
theorem circuit_reconstructs (unused : Stream 2) :
    (circuit .ogf (1 / 10)).Rel
      ![stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2)),
        ofPoly .ogf (MvPolynomial.X 1 ^ 2), unused]
      ![rhs .ogf (1 / 10) (stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2))),
        stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2))] := by
  exact circuit_solution .ogf (1 / 10) _ unused

Theorem from_circuit Kernel checkedAs recorded L112–116

Namespace Notebook.Burgers

… and nothing else: whatever it reconstructs from x² is that stream.

Statement
(a  unused  v  :  Stream  2)(\text{a}\;\text{unused}\;\text{v}\;:\;\text{Stream}\;2)  (rel  :  (circuit  .ogf  (1  /  10)).Rel  ![a,  ofPoly  .ogf  (MvPolynomial.X  1  ^  2),  unused]  ![v,  a])  :\;(\text{rel}\;:\;(\text{circuit}\;.\text{ogf}\;(1\;/\;10)).\text{Rel}\;!\text{[}\text{a},\;\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2),\;\text{unused}\text{]}\;!\text{[}\text{v},\;\text{a}\text{]})\;:  a  =  stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2))\;\text{a}\;=\;\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2))

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 5 lines
/-- … and nothing else: whatever it reconstructs from `x²` is that stream. -/
theorem from_circuit (a unused v : Stream 2)
    (rel : (circuit .ogf (1 / 10)).Rel ![a, ofPoly .ogf (MvPolynomial.X 1 ^ 2), unused] ![v, a]) :
    a = stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2)) := by
  exact candidate_stream .ogf (1 / 10) _ a unused v rel

Inspect coefficients and the limits of formal reasoning

At ν=110\nu=\tfrac{1}{10}, the first coefficients from x2x^2 are exact and rule out the heat stream x2+2tx^2+2t. They do not establish convergence or divergence. For affine data, only the first-iterate coefficient is checked.6 Kernel checked 6 As recorded

Compute the first coefficients from x2x^2

Polynomial Picard iterates give the correct coefficients through their iteration's time degree. Terms at higher degrees can still change.4 Kernel checked 4 As recorded

From a polynomial profile every Picard iterate is a polynomial, and the nn-th iterate is right up to tt-degree nn. The library computes the first three as polynomial identities:

p1=x2+t(15−2x3)p2=x2+t(15−2x3)+t2(−45x+5x4)+t3(25x2−4x5)p3=(p2 up to t2)+t3(165x2−14x5)+t4(⋯ )+⋯+t7(⋯ )\begin{aligned} p_1 &= x^2 + t\Big(\tfrac15 - 2x^3\Big) \\ p_2 &= x^2 + t\Big(\tfrac15 - 2x^3\Big) + t^2\Big(-\tfrac45 x + 5x^4\Big) + t^3\Big(\tfrac25 x^2 - 4x^5\Big) \\ p_3 &= (p_2 \text{ up to } t^2) + t^3\Big(\tfrac{16}{5}x^2 - 14x^5\Big) + t^4(\cdots) + \dots + t^7(\cdots) \end{aligned}

The t3t^3 term of p2p_2, 25x2−4x5\tfrac25 x^2 - 4x^5, is an artefact of the iteration; the true slice, 165x2−14x5\tfrac{16}{5}x^2 - 14x^5, appears in p3p_3, whose own artefacts run from t4t^4 to t7t^7. That is the theorem made visible: the nn-th iterate is the stream up to degree nn, and no further.

Theorem coefficient_t Kernel checkedAs recorded L142–147

Namespace Notebook.Burgers

The coefficient of tt is 15\tfrac15: only the viscous term ν (x2)′′=15\nu\,(x^2)'' = \tfrac15 contributes, since u0u0′=2x3u_0 u_0' = 2x^3 has no constant part (the library also checks that it is 00 without viscosity).

Statement
stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2))  (Finsupp.single  0  1)  =  1  /  5\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2))\;(\text{Finsupp}.\text{single}\;0\;1)\;=\;1\;/\;5

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- The coefficient of $t$ is $\tfrac15$: only the viscous term
$\nu\,(x^2)'' = \tfrac15$ contributes, since $u_0 u_0' = 2x^3$ has no constant
part (the library also checks that it is $0$ without viscosity). -/
theorem coefficient_t :
    stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2)) (Finsupp.single 0 1) = 1 / 5 := by
  exact coeff_t

Theorem coefficient_t_x3 Kernel checkedAs recorded L149–153

Namespace Notebook.Burgers

The coefficient of tx3t x^3 is −2-2: only the nonlinearity contributes.

Statement
stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2))\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2))  (Finsupp.single  0  1  +  Finsupp.single  1  3)  =  −2\;(\text{Finsupp}.\text{single}\;0\;1\;+\;\text{Finsupp}.\text{single}\;1\;3)\;=\;-2

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 5 lines
/-- The coefficient of $t x^3$ is $-2$: only the nonlinearity contributes. -/
theorem coefficient_t_x3 :
    stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2))
      (Finsupp.single 0 1 + Finsupp.single 1 3) = -2 := by
  exact coeff_t_x3

Theorem coefficients_t2 Kernel checkedAs recorded L155–161

Namespace Notebook.Burgers

At t2t^2: the coefficients of xx and x4x^4 are −45-\tfrac45 and 55.

Statement
stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2))\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2))  (Finsupp.single  0  2  +  Finsupp.single  1  1)  =  −4  /  5  ∧\;(\text{Finsupp}.\text{single}\;0\;2\;+\;\text{Finsupp}.\text{single}\;1\;1)\;=\;-4\;/\;5\;\land   stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2))\;\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2))  (Finsupp.single  0  2  +  Finsupp.single  1  4)  =  5\;(\text{Finsupp}.\text{single}\;0\;2\;+\;\text{Finsupp}.\text{single}\;1\;4)\;=\;5

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 7 lines
/-- At $t^2$: the coefficients of $x$ and $x^4$ are $-\tfrac45$ and $5$. -/
theorem coefficients_t2 :
    stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2))
        (Finsupp.single 0 2 + Finsupp.single 1 1) = -4 / 5 ∧
      stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2))
        (Finsupp.single 0 2 + Finsupp.single 1 4) = 5 := by
  exact ⟨coeff_t2_x, coeff_t2_x4⟩

Theorem coefficients_t3 Kernel checkedAs recorded L163–170

Namespace Notebook.Burgers

At t3t^3: the coefficients of x2x^2 and x5x^5 are 165\tfrac{16}{5} and −14-14, from the third iterate, not from the second's artefact.

Statement
stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2))\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2))  (Finsupp.single  0  3  +  Finsupp.single  1  2)  =  16  /  5  ∧\;(\text{Finsupp}.\text{single}\;0\;3\;+\;\text{Finsupp}.\text{single}\;1\;2)\;=\;16\;/\;5\;\land   stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2))\;\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2))  (Finsupp.single  0  3  +  Finsupp.single  1  5)  =  −14\;(\text{Finsupp}.\text{single}\;0\;3\;+\;\text{Finsupp}.\text{single}\;1\;5)\;=\;-14

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 8 lines
/-- At $t^3$: the coefficients of $x^2$ and $x^5$ are $\tfrac{16}{5}$ and $-14$,
from the third iterate, not from the second's artefact. -/
theorem coefficients_t3 :
    stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2))
        (Finsupp.single 0 3 + Finsupp.single 1 2) = 16 / 5 ∧
      stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2))
        (Finsupp.single 0 3 + Finsupp.single 1 5) = -14 := by
  exact ⟨coeff_t3_x2, coeff_t3_x5⟩

Reject the proposed heat stream

The checked coefficient [t]=15[t]=\tfrac15 rules out the proposed value 22. This is a proved negation, not a decider refutation.1 Kernel checked 1 As recorded

The heat equation from the same profile has the polynomial solution x2+2tx^2 + 2t, so its tt-coefficient is 22. Burgers' is 15\tfrac15: the two streams differ. This comparison also uses different diffusion coefficients: x2+2tx^2+2t is the heat solution at viscosity 11, whereas this Burgers stream uses ν=110\nu=\tfrac{1}{10}. This theorem is proved on this page from coefficient_t rather than restated.

Theorem not_heat Kernel checkedAs recorded L186–196

Namespace Notebook.Burgers

The heat stream from x² is not the Burgers stream from x².

Statement
Heat.stream  .ogf  (Polynomial.X  ^  2)  ≠\text{Heat}.\text{stream}\;.\text{ogf}\;(\text{Polynomial}.\text{X}\;\text{\textasciicircum{}}\;2)\;\ne   stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1  ^  2))\;\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1\;\text{\textasciicircum{}}\;2))
uses coefficient_t

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 11 lines
/-- The heat stream from `x²` is not the Burgers stream from `x²`. -/
theorem not_heat :
    Heat.stream .ogf (Polynomial.X ^ 2) ≠
      stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1 ^ 2)) := by
  intro same
  have := congrFun same (Finsupp.single 0 1)
  rw [coefficient_t, Heat.stream, Gimle.Asgard.Examples.PolynomialHeat.square, ofPoly_ogf_apply]
    at this
  simp [MvPolynomial.coeff_X_pow, MvPolynomial.coeff_X, Finsupp.ext_iff, Fin.forall_fin_two,
    Finsupp.single_apply] at this
  norm_num at this

Separate coefficient evidence from convergence

The growth discussion for x2x^2 is unformalized, and finite coefficient ratios do not prove divergence. The affine example below checks only the first iterate, not convergence of its series.1 Kernel checked 1 As recorded

Why divergence is plausible for the quadratic profile

The numerical ratios and the classical Cole–Hopf explanation motivate a radius-zero claim for nonzero viscosity. That claim is not proved here.No claim observations

Exact arithmetic on the recurrence gives the tt-slices un(x)u_n(x) — the coefficient of tnt^n, a polynomial in xx: x2x^2, then 15−2x3\tfrac15 - 2x^3, then −45x+5x4-\tfrac45 x + 5x^4, then 165x2−14x5\tfrac{16}{5}x^2 - 14x^5, as checked in **Compute the first coefficients from x2x^2**. The xx-degree grows by one per tt-degree, so the slices' degrees repeat modulo three, and the coefficients grow. With an=∑k∣cn,k∣ 2−ka_n = \sum_k |c_{n,k}|\,2^{-k}, the norm of the slice on ∣x∣≤12|x| \le \tfrac12, the ratios an+3/ana_{n+3}/a_n at n=3,9,15,21n = 3, 9, 15, 21 are

νan+3/an at n=3,9,15,2103.8, 5.5, 6.3, 6.6plateau1109.4, 16.4, 21.5, 25.8increasing, no plateau1227, 48, 66, 83increasing, no plateau\begin{array}{c|l|l} \nu & a_{n+3}/a_n \text{ at } n = 3, 9, 15, 21 & \\ \hline 0 & 3.8,\ 5.5,\ 6.3,\ 6.6 & \text{plateau} \\ \tfrac{1}{10} & 9.4,\ 16.4,\ 21.5,\ 25.8 & \text{increasing, no plateau} \\ \tfrac{1}{2} & 27,\ 48,\ 66,\ 83 & \text{increasing, no plateau} \end{array}

The plateau at ν=0\nu = 0 is what Cauchy–Kowalevski predicts for the inviscid equation with analytic data. These finite ratios suggest growth but do not prove divergence. The explanation is the classical divergence of the formal heat series (Kowalevski's 1875 example) transported by Cole–Hopf: u=−2ν φx/φu = -2\nu\,\varphi_x/\varphi with φt=νφxx\varphi_t = \nu\varphi_{xx} and φ(0,x)=e−x3/(6ν)\varphi(0, x) = e^{-x^3/(6\nu)}, an entire function of order three, whose heat series diverges; that picture predicts growth like (n!)1/3(n!)^{1/3} asymptotically, which these small nn do not yet show. The explanation is from the literature, not proved here. Divergence does not touch the theorem: the coefficients are exact and unique, which is what a formal statement claims. Certified truncation needs a stream whose series converges; the last sections have one, from a Cole–Hopf potential.

Check the affine profile's first iterate

For initial profile xx, the first iterate is x−txx-tx, so its [tx][tx] coefficient is −1-1. The closed form mentioned below is explanatory only.1 Kernel checked 1 As recorded

Affine data is the exception: from u(0,x)=xu(0, x) = x the solution is x/(1+t)x/(1+t), the viscous term vanishes identically, and the first iterate is x−txx - t x, so [tx]=−1[t x] = -1. Nothing beyond the first iterate is proved.

Theorem affine_coefficient Kernel checkedAs recorded L244–251

Namespace Notebook.Burgers

From x, the coefficient of txt x is −1-1: the start of x/(1+t)x/(1+t).

Statement
stream  .ogf  (1  /  10)  (ofPoly  .ogf  (MvPolynomial.X  1))\text{stream}\;.\text{ogf}\;(1\;/\;10)\;(\text{ofPoly}\;.\text{ogf}\;(\text{MvPolynomial}.\text{X}\;1))  (Finsupp.single  0  1  +  Finsupp.single  1  1)  =  −1\;(\text{Finsupp}.\text{single}\;0\;1\;+\;\text{Finsupp}.\text{single}\;1\;1)\;=\;-1

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 8 lines
/-- From `x`, the coefficient of $t x$ is $-1$: the start of $x/(1+t)$. -/
theorem affine_coefficient :
    stream .ogf (1 / 10) (ofPoly .ogf (MvPolynomial.X 1))
      (Finsupp.single 0 1 + Finsupp.single 1 1) = -1 := by
  have idx : (Finsupp.single 0 1 + Finsupp.single 1 1 : Index 2) 0 = 1 := by simp
  rw [stream_ogf_coeff, idx, show (1 / 10 : ℚ) = ν from rfl, picard_affine_one]
  simp [MvPolynomial.coeff_X_mul', MvPolynomial.coeff_X, Finsupp.ext_iff, Fin.forall_fin_two,
    Finsupp.single_apply, Finsupp.tsub_apply]

Certify convergence and truncation for the front

For ν=12\nu=\tfrac12 and potential 1+e−x1+e^{-x}, the series converges on ∣t∣≤16|t|\le\tfrac16, ∣x∣≤18|x|\le\tfrac18. The error beyond the 16×1616\times16 window is at most 116384\tfrac{1}{16384}, a certified bound rather than an estimate.4 Kernel checked 4 As recorded

Explain the coefficient majorant

A bound on every coefficient gives absolute convergence and a uniform tail bound on a smaller box. Rational side conditions certify each step.No claim observations

Cole–Hopf turns a solution φ\varphi of the heat equation φt=νφxx\varphi_t = \nu\varphi_{xx} into a solution u=−2ν φx/φu = -2\nu\,\varphi_x/\varphi of Burgers. As formal streams this is exact: Streams.ColeHopf.quotient_pde proves it from a Leibniz rule for the derivative of streams and the derivative of the inverse; after those rules the identity is polynomial in φx,φxx,φxxx,φ−1\varphi_x, \varphi_{xx}, \varphi_{xxx}, \varphi^{-1} and closes by ring. Classically, φ(0,x)=1+e−x\varphi(0, x) = 1 + e^{-x} and ν=12\nu = \tfrac12 give the front 1/(1+ex−t/2)1/(1 + e^{x - t/2}), a step from 11 to 00 moving right at speed 12\tfrac12; the stream here is its formal series, and the section after the certificate identifies the two on the box.

A majorant is an explicit bound ∣cn,k∣≤MRt−nRx−k|c_{n,k}| \le M R_t^{-n} R_x^{-k} on every coefficient. It makes the series converge for ∣t∣<Rt|t| < R_t, ∣x∣<Rx|x| < R_x, and it bounds the tail beyond a window — the partial sum over n<Ntn < N_t, k<Nxk < N_x — uniformly on any smaller box. The heat stream of an exponential-sum profile has such a majorant; a calculus of majorants carries it through the derivative, the inverse (at radii where the non-constant part of φ\varphi is small against its constant term, a rational inequality) and the product (which halves the radii); and the library's tail theorem turns the majorant into the uniform error. Every side condition is a rational inequality the kernel decides.

The numbers: the potential fits ρ=1\rho = 1; the inverse is majorized at radii (23,12)(\tfrac23, \tfrac12), where that inequality holds with equality; the product halves them to (13,14)(\tfrac13, \tfrac14); on ∣t∣≤16|t| \le \tfrac16, ∣x∣≤18|x| \le \tfrac18 at window 16×1616 \times 16 the certified error is 12⋅2⋅2−16⋅4=116384\tfrac12 \cdot 2 \cdot 2^{-16} \cdot 4 = \tfrac{1}{16384}. By the closed form identified below (front_field), the true error on that box is near 10−1910^{-19} — a numerical estimate, not a theorem; the certificate is a proof of a bound, not a measurement.

Check the constant term, convergence and error

The front's constant coefficient is 12\tfrac12. The following claims establish the error constant, summation on the box and the uniform truncation bound.4 Kernel checked 4 As recorded

Theorem front_at_origin Kernel checkedAs recorded L302–306

Namespace Notebook.Burgers

The front's constant coefficient, −2ν (∑ciai)/(∑ci)-2\nu\,(\sum c_i a_i)/(\sum c_i), is 12\tfrac12 — as the closed form's u(0,0)u(0, 0) predicts.

Statement
MvPowerSeries.constantCoeff  (ColeHopf.front  (1  /  2)  [(1,  0),  (1,  −1)])  =  1  /  2\text{MvPowerSeries}.\text{constantCoeff}\;(\text{ColeHopf}.\text{front}\;(1\;/\;2)\;\text{[}(1,\;0),\;(1,\;-1)\text{]})\;=\;1\;/\;2

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 5 lines
/-- The front's constant coefficient, $-2\nu\,(\sum c_i a_i)/(\sum c_i)$, is $\tfrac12$ —
as the closed form's $u(0, 0)$ predicts. -/
theorem front_at_origin :
    MvPowerSeries.constantCoeff (ColeHopf.front (1 / 2) [(1, 0), (1, -1)]) = 1 / 2 := by
  exact Gimle.Asgard.Examples.BurgersFront.constantCoeff_front_eq

Theorem front_error Kernel checkedAs recorded L308–313

Namespace Notebook.Burgers

The certified error at window 16×1616 \times 16 is exactly 116384\tfrac{1}{16384}.

Statement
tailBound  (ColeHopf.frontMajorant  (1  /  2)  [(1,  0),  (1,  −1)]  ![2  /  3,  1  /  2]\text{tailBound}\;(\text{ColeHopf}.\text{frontMajorant}\;(1\;/\;2)\;\text{[}(1,\;0),\;(1,\;-1)\text{]}\;!\text{[}2\;/\;3,\;1\;/\;2\text{]}  Gimle.Asgard.Examples.BurgersFront.hr)  Gimle.Asgard.Examples.BurgersFront.box  ![16,  16]  =\;\text{Gimle}.\text{Asgard}.\text{Examples}.\text{BurgersFront}.\text{hr})\;\text{Gimle}.\text{Asgard}.\text{Examples}.\text{BurgersFront}.\text{box}\;!\text{[}16,\;16\text{]}\;=116384\frac{1}{16384}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- The certified error at window $16 \times 16$ is exactly $\tfrac{1}{16384}$. -/
theorem front_error :
    tailBound (ColeHopf.frontMajorant (1 / 2) [(1, 0), (1, -1)] ![2 / 3, 1 / 2]
      Gimle.Asgard.Examples.BurgersFront.hr) Gimle.Asgard.Examples.BurgersFront.box ![16, 16] =
      1 / 16384 := by
  exact Gimle.Asgard.Examples.BurgersFront.error_eq

Theorem front_converges Kernel checkedAs recorded L315–324

Namespace Notebook.Burgers

Convergent. At every point of the box the series of the front sums to its analytic field: absolute convergence, from the majorant.

Statement
(x  :  Fin  2  →  R)  (hx  :  Gimle.Asgard.Examples.BurgersFront.box.Mem  x)  :(\text{x}\;:\;\text{Fin}\;2\;\to \;\mathbb{R} )\;(\text{hx}\;:\;\text{Gimle}.\text{Asgard}.\text{Examples}.\text{BurgersFront}.\text{box}.\text{Mem}\;\text{x})\;:  HasSum  (seriesTerm  .ogf  (ColeHopf.front  (1  /  2)  [(1,  0),  (1,  −1)])  x)\;\text{HasSum}\;(\text{seriesTerm}\;.\text{ogf}\;(\text{ColeHopf}.\text{front}\;(1\;/\;2)\;\text{[}(1,\;0),\;(1,\;-1)\text{]})\;\text{x})  (analyticField  .ogf  (ColeHopf.front  (1  /  2)  [(1,  0),  (1,  −1)])  x)\;(\text{analyticField}\;.\text{ogf}\;(\text{ColeHopf}.\text{front}\;(1\;/\;2)\;\text{[}(1,\;0),\;(1,\;-1)\text{]})\;\text{x})

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 10 lines
/-- **Convergent.** At every point of the box the series of the front sums to
its analytic field: absolute convergence, from the majorant. -/
theorem front_converges (x : Fin 2 → ℝ) (hx : Gimle.Asgard.Examples.BurgersFront.box.Mem x) :
    HasSum (seriesTerm .ogf (ColeHopf.front (1 / 2) [(1, 0), (1, -1)]) x)
      (analyticField .ogf (ColeHopf.front (1 / 2) [(1, 0), (1, -1)]) x) := by
  exact (ColeHopf.certificate Gimle.Asgard.Examples.BurgersFront.hν
    Gimle.Asgard.Examples.BurgersFront.hρ Gimle.Asgard.Examples.BurgersFront.terms
    Gimle.Asgard.Examples.BurgersFront.fits Gimle.Asgard.Examples.BurgersFront.hr
    Gimle.Asgard.Examples.BurgersFront.inside Gimle.Asgard.Examples.BurgersFront.small
    Gimle.Asgard.Examples.BurgersFront.box Gimle.Asgard.Examples.BurgersFront.boxInside).hasSum hx

Theorem front_certified Kernel checkedAs recorded L326–334

Namespace Notebook.Burgers

Certified. Whatever the Burgers circuit at ν=12\nu = \tfrac12 reconstructs from the front's t=0t = 0 slice differs from its 16×1616 \times 16 window by at most 116384\tfrac{1}{16384} everywhere on ∣t∣≤16|t| \le \tfrac16, ∣x∣≤18|x| \le \tfrac18.

Statement
∀  a  unused  v  :  Stream  2,\forall \;\text{a}\;\text{unused}\;\text{v}\;:\;\text{Stream}\;2,  (Burgers.circuit  .ogf  (1  /  2)).Rel\;(\text{Burgers}.\text{circuit}\;.\text{ogf}\;(1\;/\;2)).\text{Rel}  ![a,  ColeHopf.zeroSlice  (ColeHopf.front  (1  /  2)  [(1,  0),  (1,  −1)]),  unused]  ![v,  a]  →\;!\text{[}\text{a},\;\text{ColeHopf}.\text{zeroSlice}\;(\text{ColeHopf}.\text{front}\;(1\;/\;2)\;\text{[}(1,\;0),\;(1,\;-1)\text{]}),\;\text{unused}\text{]}\;!\text{[}\text{v},\;\text{a}\text{]}\;\to   TruncationBound  .ogf  a  Gimle.Asgard.Examples.BurgersFront.box  ![16,  16]  (1  /  16384)\;\text{TruncationBound}\;.\text{ogf}\;\text{a}\;\text{Gimle}.\text{Asgard}.\text{Examples}.\text{BurgersFront}.\text{box}\;!\text{[}16,\;16\text{]}\;(1\;/\;16384)

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 9 lines
/-- **Certified.** Whatever the Burgers circuit at $\nu = \tfrac12$ reconstructs
from the front's $t = 0$ slice differs from its $16 \times 16$ window by at
most $\tfrac{1}{16384}$ everywhere on $|t| \le \tfrac16$, $|x| \le \tfrac18$. -/
theorem front_certified :
    ∀ a unused v : Stream 2,
      (Burgers.circuit .ogf (1 / 2)).Rel
        ![a, ColeHopf.zeroSlice (ColeHopf.front (1 / 2) [(1, 0), (1, -1)]), unused] ![v, a] →
        TruncationBound .ogf a Gimle.Asgard.Examples.BurgersFront.box ![16, 16] (1 / 16384) := by
  exact Gimle.Asgard.Examples.BurgersFront.bound

Identify the sum and test its bounds

On the certified box, the analytic field equals 1/(1+ex−t/2)1/(1+e^{x-t/2}) and lies in [25,35][\tfrac25,\tfrac35]. The upper bound 2750\tfrac{27}{50} is false, with a checked negation at (t,x)=(16,−18)(t,x)=(\tfrac16,-\tfrac18).3 Kernel checked 3 As recorded

Everything so far is about the series. Its analytic field — the sum at a real point, what a plot shows — is now identified: on a box strictly inside the radii of both factors' majorants, the field of a product is the product of the fields (the Cauchy product of two absolutely convergent double series, regrouped along antidiagonals), the field of an inverse is the inverse of the field, and the heat stream of an exponential sum sums to ∑icieνai2t+aix\sum_i c_i e^{\nu a_i^2 t + a_i x} everywhere. On the certified box the front's field is therefore −2ν φx/φ-2\nu\,\varphi_x/\varphi evaluated on the classical heat fields, which is 1/(1+ex−t/2)1/(1 + e^{x - t/2}) — the closed form that was only named above. That this function solves the real Burgers equation is classical and not proved here; what is proved is the equality of the field with it on the box.

Bounds then follow from one inequality, s+1≤ess + 1 \le e^s. On the box ∣x−t/2∣≤524|x - t/2| \le \tfrac{5}{24}, so e±(x−t/2)≥1924e^{\pm(x - t/2)} \ge \tfrac{19}{24}, which gives 25≤u≤35\tfrac25 \le u \le \tfrac35. The tighter u≤2750u \le \tfrac{27}{50} is false: at the corner (t,x)=(16,−18)(t, x) = (\tfrac16, -\tfrac18), u=1/(1+e−5/24)≥2953>2750u = 1/(1 + e^{-5/24}) \ge \tfrac{29}{53} > \tfrac{27}{50}. Its negation is a checked theorem here, restated from the library's not_below: a proved negation, like not_heat, not a decider refutation. The decider's own answer to the same bound, from the series alone, is in the last section (front_band_refuted).

Theorem front_field Kernel checkedAs recorded L366–371

Namespace Notebook.Burgers

Identified. On the box the front's analytic field is the closed form 1/(1+ex−t/2)1/(1 + e^{x - t/2}).

Statement
(x  :  Fin  2  →  R)  (hx  :  Gimle.Asgard.Examples.BurgersFront.box.Mem  x)  :(\text{x}\;:\;\text{Fin}\;2\;\to \;\mathbb{R} )\;(\text{hx}\;:\;\text{Gimle}.\text{Asgard}.\text{Examples}.\text{BurgersFront}.\text{box}.\text{Mem}\;\text{x})\;:  analyticField  .ogf  (ColeHopf.front  (1  /  2)  [(1,  0),  (1,  −1)])  x  =\;\text{analyticField}\;.\text{ogf}\;(\text{ColeHopf}.\text{front}\;(1\;/\;2)\;\text{[}(1,\;0),\;(1,\;-1)\text{]})\;\text{x}\;=  1  /  (1  +  Real.exp  (x  1  −  x  0  /  2))\;1\;/\;(1\;+\;\text{Real}.\text{exp}\;(\text{x}\;1\;-\;\text{x}\;0\;/\;2))

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- **Identified.** On the box the front's analytic field is the closed form
$1/(1 + e^{x - t/2})$. -/
theorem front_field (x : Fin 2 → ℝ) (hx : Gimle.Asgard.Examples.BurgersFront.box.Mem x) :
    analyticField .ogf (ColeHopf.front (1 / 2) [(1, 0), (1, -1)]) x =
      1 / (1 + Real.exp (x 1 - x 0 / 2)) := by
  exact Gimle.Asgard.Examples.BurgersFront.front_field_eq hx

Theorem front_band Kernel checkedAs recorded L373–381

Namespace Notebook.Burgers

Bounded. Whatever the circuit reconstructs from the front's slice has its field in [25,35][\tfrac25, \tfrac35] everywhere on the box.

Statement
∀  a  unused  v  :  Stream  2,\forall \;\text{a}\;\text{unused}\;\text{v}\;:\;\text{Stream}\;2,  (Burgers.circuit  .ogf  (1  /  2)).Rel\;(\text{Burgers}.\text{circuit}\;.\text{ogf}\;(1\;/\;2)).\text{Rel}  ![a,  ColeHopf.zeroSlice  (ColeHopf.front  (1  /  2)  [(1,  0),  (1,  −1)]),  unused]  ![v,  a]  →\;!\text{[}\text{a},\;\text{ColeHopf}.\text{zeroSlice}\;(\text{ColeHopf}.\text{front}\;(1\;/\;2)\;\text{[}(1,\;0),\;(1,\;-1)\text{]}),\;\text{unused}\text{]}\;!\text{[}\text{v},\;\text{a}\text{]}\;\to   ∀  x  :  Fin  2  →  R,  Gimle.Asgard.Examples.BurgersFront.box.Mem  x  →\;\forall \;\text{x}\;:\;\text{Fin}\;2\;\to \;\mathbb{R} ,\;\text{Gimle}.\text{Asgard}.\text{Examples}.\text{BurgersFront}.\text{box}.\text{Mem}\;\text{x}\;\to   2  /  5  ≤  analyticField  .ogf  a  x  ∧  analyticField  .ogf  a  x  ≤  3  /  5\;2\;/\;5\;\le \;\text{analyticField}\;.\text{ogf}\;\text{a}\;\text{x}\;\land \;\text{analyticField}\;.\text{ogf}\;\text{a}\;\text{x}\;\le \;3\;/\;5

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 9 lines
/-- **Bounded.** Whatever the circuit reconstructs from the front's slice has its
field in $[\tfrac25, \tfrac35]$ everywhere on the box. -/
theorem front_band :
    ∀ a unused v : Stream 2,
      (Burgers.circuit .ogf (1 / 2)).Rel
        ![a, ColeHopf.zeroSlice (ColeHopf.front (1 / 2) [(1, 0), (1, -1)]), unused] ![v, a] →
        ∀ x : Fin 2 → ℝ, Gimle.Asgard.Examples.BurgersFront.box.Mem x →
          2 / 5 ≤ analyticField .ogf a x ∧ analyticField .ogf a x ≤ 3 / 5 := by
  exact Gimle.Asgard.Examples.BurgersFront.band

Theorem front_not_below Kernel checkedAs recorded L383–391

Namespace Notebook.Burgers

Refuted, as a proved negation: u≤2750u \le \tfrac{27}{50} on the box fails at the corner (16,−18)(\tfrac16, -\tfrac18), where the front itself is at least 2953\tfrac{29}{53}.

Statement
¬  ∀  a  unused  v  :  Stream  2,\neg \;\forall \;\text{a}\;\text{unused}\;\text{v}\;:\;\text{Stream}\;2,  (Burgers.circuit  .ogf  (1  /  2)).Rel\;(\text{Burgers}.\text{circuit}\;.\text{ogf}\;(1\;/\;2)).\text{Rel}  ![a,  ColeHopf.zeroSlice  (ColeHopf.front  (1  /  2)  [(1,  0),  (1,  −1)]),  unused]  ![v,  a]  →\;!\text{[}\text{a},\;\text{ColeHopf}.\text{zeroSlice}\;(\text{ColeHopf}.\text{front}\;(1\;/\;2)\;\text{[}(1,\;0),\;(1,\;-1)\text{]}),\;\text{unused}\text{]}\;!\text{[}\text{v},\;\text{a}\text{]}\;\to   ∀  x  :  Fin  2  →  R,  Gimle.Asgard.Examples.BurgersFront.box.Mem  x  →\;\forall \;\text{x}\;:\;\text{Fin}\;2\;\to \;\mathbb{R} ,\;\text{Gimle}.\text{Asgard}.\text{Examples}.\text{BurgersFront}.\text{box}.\text{Mem}\;\text{x}\;\to   analyticField  .ogf  a  x  ≤  27  /  50\;\text{analyticField}\;.\text{ogf}\;\text{a}\;\text{x}\;\le \;27\;/\;50

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 9 lines
/-- **Refuted**, as a proved negation: $u \le \tfrac{27}{50}$ on the box fails at the
corner $(\tfrac16, -\tfrac18)$, where the front itself is at least $\tfrac{29}{53}$. -/
theorem front_not_below :
    ¬ ∀ a unused v : Stream 2,
      (Burgers.circuit .ogf (1 / 2)).Rel
        ![a, ColeHopf.zeroSlice (ColeHopf.front (1 / 2) [(1, 0), (1, -1)]), unused] ![v, a] →
        ∀ x : Fin 2 → ℝ, Gimle.Asgard.Examples.BurgersFront.box.Mem x →
          analyticField .ogf a x ≤ 27 / 50 := by
  exact Gimle.Asgard.Examples.BurgersFront.not_below

Inspect the automated certificates and their limits

On the same box, the decider certifies truncation at tolerance 10−410^{-4} and the band [25,35][\tfrac25,\tfrac35], and refutes the upper bound 2750\tfrac{27}{50}. The 10−610^{-6} truncation request remains unknown.2 Kernel checked 3 As recorded 1 Contains sorry

Certify the requested truncation

The decider finds a certificate for tolerance 10−410^{-4} on the 16×1616\times16 window. Its search chooses the certificate; Lean checks the proof it produces.1 Kernel checked 1 As recorded

The claims above restate a certificate someone wrote by hand, in the library. The stream decider writes one itself. A goal names the model burgers, its viscosity, the potential's exponential sum, the output, the window, the box and a tolerance ε\varepsilon; the decider chooses ρ\rho as for the heat boundary and the radii of the inverse on a rational grid, mirrors the tail bound exactly to find the pair with the least certified error, and hands Lean the application of the library's front_truncation with every side condition closed by kernel computation. Lean's check of that application, re-run as part of this file, is the only authority; the mirror only chooses.

Asked for ε=10−4\varepsilon = 10^{-4}, it finds ρ=1\rho = 1 and the radii (23,12)(\tfrac23, \tfrac12) of the example above, with the certified error 116384<10−4\tfrac{1}{16384} < 10^{-4}, and the claim it writes is checked. Asked for ε=10−6\varepsilon = 10^{-6} on the same box and window, no radii on its grid certify it: the directive stays undecided, exhausted, and no claim is written — the decider never refutes a truncation claim, because a majorant bound says nothing about the true error, which by the closed form identified above is far below 10−610^{-6} (a numerical estimate, not a theorem).

Decisionfront_decided · stream · forsetiNever runL426–428
stream burgers viscosity 1/2 interpretation analytic-tail basis ogf potential exponentials [1, 0], [1, -1] truncation u window 16, 16 radius 1/6, 1/8 epsilon 1/10000

Not run yet.

namespace Decided_front_decided
L430–430

Definition forsetiBox : Gimle.Asgard.Streams.Box 2 L432–433

Namespace Notebook.Burgers.Decided_front_decided

⟨![(mkRat  (1)  6),  (mkRat  (1)  8)],  by  decide  +kernel⟩\langle !\text{[}(\text{mkRat}\;(1)\;6),\;(\text{mkRat}\;(1)\;8)\text{]},\;\text{by}\;\text{decide}\;+\text{kernel}\rangle
Lean source · 2 lines
def forsetiBox : Gimle.Asgard.Streams.Box 2 :=
  ⟨![(mkRat (1) 6), (mkRat (1) 8)], by decide +kernel⟩

Definition forsetiRoot : Prop L435–445

Namespace Notebook.Burgers.Decided_front_decided

(∃  a  unused  v  :  Gimle.Asgard.Streams.Stream  2,(\exists \;\text{a}\;\text{unused}\;\text{v}\;:\;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{Stream}\;2,  (Gimle.Asgard.Streams.Burgers.circuit  .ogf  (mkRat  (1)  2)).Rel\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{Burgers}.\text{circuit}\;.\text{ogf}\;(\text{mkRat}\;(1)\;2)).\text{Rel}  ![a,  Gimle.Asgard.Streams.ColeHopf.zeroSlice  (Gimle.Asgard.Streams.ColeHopf.front  (mkRat  (1)  2)  [((mkRat  (1)  1),  (mkRat  (0)  1)),  ((mkRat  (1)  1),  (mkRat  (−1)  1))]),  unused]  ![v,  a])  ∧\;!\text{[}\text{a},\;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{ColeHopf}.\text{zeroSlice}\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{ColeHopf}.\text{front}\;(\text{mkRat}\;(1)\;2)\;\text{[}((\text{mkRat}\;(1)\;1),\;(\text{mkRat}\;(0)\;1)),\;((\text{mkRat}\;(1)\;1),\;(\text{mkRat}\;(-1)\;1))\text{]}),\;\text{unused}\text{]}\;!\text{[}\text{v},\;\text{a}\text{]})\;\land   ∀  a  unused  v  :  Gimle.Asgard.Streams.Stream  2,\;\forall \;\text{a}\;\text{unused}\;\text{v}\;:\;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{Stream}\;2,  (Gimle.Asgard.Streams.Burgers.circuit  .ogf  (mkRat  (1)  2)).Rel\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{Burgers}.\text{circuit}\;.\text{ogf}\;(\text{mkRat}\;(1)\;2)).\text{Rel}  ![a,  Gimle.Asgard.Streams.ColeHopf.zeroSlice  (Gimle.Asgard.Streams.ColeHopf.front  (mkRat  (1)  2)  [((mkRat  (1)  1),  (mkRat  (0)  1)),  ((mkRat  (1)  1),  (mkRat  (−1)  1))]),  unused]  ![v,  a]  →\;!\text{[}\text{a},\;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{ColeHopf}.\text{zeroSlice}\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{ColeHopf}.\text{front}\;(\text{mkRat}\;(1)\;2)\;\text{[}((\text{mkRat}\;(1)\;1),\;(\text{mkRat}\;(0)\;1)),\;((\text{mkRat}\;(1)\;1),\;(\text{mkRat}\;(-1)\;1))\text{]}),\;\text{unused}\text{]}\;!\text{[}\text{v},\;\text{a}\text{]}\;\to   (∀  x,  forsetiBox.Mem  x  →\;(\forall \;\text{x},\;\text{forsetiBox}.\text{Mem}\;\text{x}\;\to   HasSum  (Gimle.Asgard.Streams.seriesTerm  .ogf  a  x)\;\text{HasSum}\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{seriesTerm}\;.\text{ogf}\;\text{a}\;\text{x})  (Gimle.Asgard.Streams.analyticField  .ogf  a  x))  ∧\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{analyticField}\;.\text{ogf}\;\text{a}\;\text{x}))\;\land   Gimle.Asgard.Streams.TruncationBound  .ogf  a  forsetiBox  ![16,  16]  (mkRat  (1)  10000)\;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{TruncationBound}\;.\text{ogf}\;\text{a}\;\text{forsetiBox}\;!\text{[}16,\;16\text{]}\;(\text{mkRat}\;(1)\;10000)
Lean source · 11 lines
def forsetiRoot : Prop :=
  (∃ a unused v : Gimle.Asgard.Streams.Stream 2,
      (Gimle.Asgard.Streams.Burgers.circuit .ogf (mkRat (1) 2)).Rel
        ![a, Gimle.Asgard.Streams.ColeHopf.zeroSlice (Gimle.Asgard.Streams.ColeHopf.front (mkRat (1) 2) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))]), unused] ![v, a]) ∧
  ∀ a unused v : Gimle.Asgard.Streams.Stream 2,
      (Gimle.Asgard.Streams.Burgers.circuit .ogf (mkRat (1) 2)).Rel
        ![a, Gimle.Asgard.Streams.ColeHopf.zeroSlice (Gimle.Asgard.Streams.ColeHopf.front (mkRat (1) 2) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))]), unused] ![v, a] →
    (∀ x, forsetiBox.Mem x →
      HasSum (Gimle.Asgard.Streams.seriesTerm .ogf a x)
      (Gimle.Asgard.Streams.analyticField .ogf a x)) ∧
    Gimle.Asgard.Streams.TruncationBound .ogf a forsetiBox ![16, 16] (mkRat (1) 10000)

Definition forsetiRadii : Fin 2 → ℚ L447–447

Namespace Notebook.Burgers.Decided_front_decided

![(mkRat  (2)  3),  (mkRat  (1)  2)]!\text{[}(\text{mkRat}\;(2)\;3),\;(\text{mkRat}\;(1)\;2)\text{]}
Lean source · 1 line
def forsetiRadii : Fin 2 → ℚ := ![(mkRat (2) 3), (mkRat (1) 2)]

Theorem front_decided Kernel checkedAs recorded L449–504

Namespace Notebook.Burgers.Decided_front_decided

u is the stream the Burgers circuit at viscosity 1/2 rebuilds from the t = 0 slice of the Cole–Hopf front −2ν φ_x/φ of the potential Σ cᵢ·e^(aᵢx) given by the pairs (cᵢ, aᵢ), u_t its other output; its series converges on the box, and its window (16, 16) is within 1/10000 of the sum there. The stream decider proved it. Goal (stream): stream burgers viscosity 1/2 interpretation analytic-tail basis ogf potential exponentials [1, 0], [1, -1] truncation u window 16, 16 radius 1/6, 1/8 epsilon 1/10000

Statement
have  circuit\text{have}\;\text{circuit}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 56 lines
/-- u is the stream the Burgers circuit at viscosity 1/2 rebuilds from the t = 0 slice of the Cole–Hopf front −2ν φ_x/φ of the potential Σ cᵢ·e^(aᵢx) given by the pairs (cᵢ, aᵢ), u_t its other output; its series converges on the box, and its window (16, 16) is within 1/10000 of the sum there. The stream decider proved it. Goal (stream): stream burgers viscosity 1/2 interpretation analytic-tail basis ogf potential exponentials [1, 0], [1, -1] truncation u window 16, 16 radius 1/6, 1/8 epsilon 1/10000 -/
theorem front_decided :
    have circuit := Gimle.Asgard.Streams.Burgers.circuit .ogf (1/2)
    have slice := Gimle.Asgard.Streams.ColeHopf.zeroSlice
      (Gimle.Asgard.Streams.ColeHopf.front (1/2) [(1, 0), (1, -1)])
    (∃ u unused u_t : Gimle.Asgard.Streams.Stream 2,
      circuit.Rel ![u, slice, unused] ![u_t, u]) ∧
    ∀ u unused u_t : Gimle.Asgard.Streams.Stream 2,
      circuit.Rel ![u, slice, unused] ![u_t, u] →
      ∀ t x : ℝ, |t| ≤ 1/6 ∧ |x| ≤ 1/8 →
        HasSum (Gimle.Asgard.Streams.seriesTerm .ogf u ![t, x])
          (Gimle.Asgard.Streams.analyticField .ogf u ![t, x]) ∧
        |Gimle.Asgard.Streams.analyticField .ogf u ![t, x] -
          Gimle.Asgard.Streams.windowField .ogf ![16, 16] u ![t, x]| ≤ 1/10000 := by
  have root : forsetiRoot := by
    unfold forsetiRoot
    refine ⟨⟨_, 0, _, Gimle.Asgard.Streams.ColeHopf.circuit_front ((mkRat (1) 2) : ℚ) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))] (show Gimle.Asgard.Streams.ColeHopf.constantTerm [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))] ≠ 0 by decide +kernel) 0⟩, fun a unused v rel => ⟨fun x hx => ?_, ?_⟩⟩
    · have hc : MvPowerSeries.constantCoeff (Gimle.Asgard.Streams.ColeHopf.expSumHeat ((mkRat (1) 2) : ℚ) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))]) ≠ 0 := by
        rw [Gimle.Asgard.Streams.ColeHopf.constantCoeff_expSumHeat]
        decide +kernel
      simp only [Gimle.Asgard.Streams.ColeHopf.front] at rel
      rw [Gimle.Asgard.Streams.ColeHopf.candidate_quotient ((mkRat (1) 2) : ℚ) _ hc (Gimle.Asgard.Streams.ColeHopf.heatSeries_pde ((mkRat (1) 2) : ℚ) _) a unused v rel]
      exact (Gimle.Asgard.Streams.ColeHopf.certificate (show (0 : ℚ) < ((mkRat (1) 2) : ℚ) by decide +kernel) (show (0 : ℚ) < ((mkRat (1) 1) : ℚ) by decide +kernel) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))] (by decide +kernel) (r := forsetiRadii) (by decide +kernel) (by decide +kernel) (by decide +kernel) forsetiBox (by decide +kernel)).hasSum hx
    · exact Gimle.Asgard.Streams.ColeHopf.front_truncation (show (0 : ℚ) < ((mkRat (1) 2) : ℚ) by decide +kernel) (show (0 : ℚ) < ((mkRat (1) 1) : ℚ) by decide +kernel) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))] (show Gimle.Asgard.Streams.ColeHopf.constantTerm [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))] ≠ 0 by decide +kernel) (by decide +kernel) (r := forsetiRadii) (by decide +kernel) (by decide +kernel) (by decide +kernel) forsetiBox (by decide +kernel) ![16, 16] (by decide +kernel) a unused v rel
  have forsetiFront : Gimle.Asgard.Streams.ColeHopf.front (mkRat (1) 2) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))] = Gimle.Asgard.Streams.ColeHopf.front (1/2) [(1, 0), (1, -1)] := by norm_num [Rat.mkRat_eq_div]
  have forsetiCircuit : Gimle.Asgard.Streams.Burgers.circuit .ogf (mkRat (1) 2) = Gimle.Asgard.Streams.Burgers.circuit .ogf (1/2) := by norm_num [Rat.mkRat_eq_div]
  have forsetiInside : ∀ t x : ℝ, forsetiBox.Mem ![t, x] ↔ |t| ≤ 1/6 ∧ |x| ≤ 1/8 := by
    intro t x
    norm_num [Gimle.Asgard.Streams.Box.Mem, Fin.forall_fin_two, forsetiBox, Rat.mkRat_eq_div]
  have forsetiCast0 : (((mkRat (1) 10000) : ℚ) : ℝ) = (1/10000) := by norm_num [Rat.mkRat_eq_div]
  refine (fun (bridge : _ ↔ forsetiRoot) => bridge.mpr root) ?_
  constructor
  · intro claim
    dsimp only at claim
    unfold forsetiRoot
    rw [forsetiFront, forsetiCircuit]
    obtain ⟨realized, every⟩ := claim
    refine ⟨realized, fun u unused u_t rel => ⟨fun z inside => ?_, fun z inside => ?_⟩⟩
    all_goals
      have point : ![z 0, z 1] = z := by funext i; fin_cases i <;> rfl
      have holds := every u unused u_t rel (z 0) (z 1) ((forsetiInside _ _).mp (point ▸ inside))
      rw [point] at holds
    · exact holds.1
    · rw [forsetiCast0]
      exact holds.2
  · intro lane
    unfold forsetiRoot at lane
    rw [forsetiFront, forsetiCircuit] at lane
    dsimp only
    obtain ⟨realized, every⟩ := lane
    refine ⟨realized, fun u unused u_t rel t x inside => ?_⟩
    obtain ⟨sums, bound⟩ := every u unused u_t rel
    have mem := (forsetiInside t x).mpr inside
    have close := bound _ mem
    rw [forsetiCast0] at close
    exact ⟨sums _ mem, close⟩

Leave the tighter truncation request unresolved

No radii on the search grid certify 10−610^{-6} for this box and window. The request is unknown and has no claim card; it is not refuted.No claim observations
end Decided_front_decided
L513–513
Decisionfront_tighter · stream · forsetiNever runL516–518
stream burgers viscosity 1/2 interpretation analytic-tail basis ogf potential exponentials [1, 0], [1, -1] truncation u window 16, 16 radius 1/6, 1/8 epsilon 1/1000000

Not run yet.

Certify a band from the series alone

A kernel-checked coefficient window and a tail bound certify 25≤u≤35\tfrac25\le u\le\tfrac35 throughout the box, without using the closed form.1 Kernel checked 1 As recorded

front_band above is the library's hand-made bound, through the closed form and Real.add_one_le_exp. The decider has no closed form and uses none. A field claim read as an analytic field, u >= 2/5 and u <= 3/5 on the same box, is answered from the series alone: the decider computes the window of the potential's inverse below 16×1616 \times 16 by the triangular recurrence, and Lean's kernel checks that table against the finite identity (φ⋅Q)α=[α=0](\varphi \cdot Q)_\alpha = [\alpha = 0] — a wrong table loses the proof and admits nothing. The front's window W=−2ν (φx⋅Q)W = -2\nu\,(\varphi_x \cdot Q) then satisfies ∣W(t,x)−W0∣≤∑α≠0∣Wα∣rα|W(t, x) - W_0| \le \sum_{\alpha \ne 0} |W_\alpha| r^\alpha on the box, and the certified error puts the field within 116384\tfrac{1}{16384} of WW. For this box that bound is [0.4477,0.5523][0.4477, 0.5523], inside [25,35][\tfrac25, \tfrac35], and the claim is checked.

Asked whether u≤2750u \le \tfrac{27}{50}, the decider evaluates WW exactly at the corner (16,−18)(\tfrac16, -\tfrac18), where it is 0.55190.5519, above the bound by more than the error, and Lean checks the refutation: the front itself is one reconstruction, and its field at that corner is within 116384\tfrac{1}{16384} of WW. The bound is conservative, so a band inside [0.4477,0.5523][0.4477, 0.5523] that the corners do not leave stays undecided; it is never refuted on that account.

Decisionfront_band_decided · stream · forsetiNever runL547–549
stream burgers viscosity 1/2 interpretation analytic-field basis ogf potential exponentials [1, 0], [1, -1] field u over t in [-1/6, 1/6], x in [-1/8, 1/8] : u >= 2/5 and u <= 3/5

Not run yet.

namespace Decided_front_band_decided
L551–551

Definition forsetiBox : Gimle.Asgard.Streams.Box 2 L553–554

Namespace Notebook.Burgers.Decided_front_band_decided

⟨![(mkRat  (1)  6),  (mkRat  (1)  8)],  by  decide  +kernel⟩\langle !\text{[}(\text{mkRat}\;(1)\;6),\;(\text{mkRat}\;(1)\;8)\text{]},\;\text{by}\;\text{decide}\;+\text{kernel}\rangle
Lean source · 2 lines
def forsetiBox : Gimle.Asgard.Streams.Box 2 :=
  ⟨![(mkRat (1) 6), (mkRat (1) 8)], by decide +kernel⟩

Definition forsetiRadii : Fin 2 → ℚ L556–556

Namespace Notebook.Burgers.Decided_front_band_decided

![(mkRat  (2)  3),  (mkRat  (1)  2)]!\text{[}(\text{mkRat}\;(2)\;3),\;(\text{mkRat}\;(1)\;2)\text{]}
Lean source · 1 line
def forsetiRadii : Fin 2 → ℚ := ![(mkRat (2) 3), (mkRat (1) 2)]

Definition forsetiTable : List (List ℚ) L558–574

Namespace Notebook.Burgers.Decided_front_band_decided

[\text{[}  [(mkRat  (1)  2),  (mkRat  (1)  4),  (mkRat  (0)  1),  (mkRat  (−1)  48),  (mkRat  (0)  1),  (mkRat  (1)  480),  (mkRat  (0)  1),  (mkRat  (−17)  80640),  (mkRat  (0)  1),  (mkRat  (31)  1451520),  (mkRat  (0)  1),  (mkRat  (−691)  319334400),  (mkRat  (0)  1),  (mkRat  (5461)  24908083200),  (mkRat  (0)  1),  (mkRat  (−929569)  41845579776000)],\;\text{[}(\text{mkRat}\;(1)\;2),\;(\text{mkRat}\;(1)\;4),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-1)\;48),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(1)\;480),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-17)\;80640),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(31)\;1451520),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;319334400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;24908083200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;41845579776000)\text{]},  [(mkRat  (−1)  8),  (mkRat  (0)  1),  (mkRat  (1)  32),  (mkRat  (0)  1),  (mkRat  (−1)  192),  (mkRat  (0)  1),  (mkRat  (17)  23040),  (mkRat  (0)  1),  (mkRat  (−31)  322560),  (mkRat  (0)  1),  (mkRat  (691)  58060800),  (mkRat  (0)  1),  (mkRat  (−5461)  3832012800),  (mkRat  (0)  1),  (mkRat  (929569)  5579410636800),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(-1)\;8),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(1)\;32),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-1)\;192),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(17)\;23040),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-31)\;322560),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(691)\;58060800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;3832012800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;5579410636800),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (−1)  64),  (mkRat  (0)  1),  (mkRat  (1)  192),  (mkRat  (0)  1),  (mkRat  (−17)  15360),  (mkRat  (0)  1),  (mkRat  (31)  161280),  (mkRat  (0)  1),  (mkRat  (−691)  23224320),  (mkRat  (0)  1),  (mkRat  (5461)  1277337600),  (mkRat  (0)  1),  (mkRat  (−929569)  1594117324800),  (mkRat  (0)  1),  (mkRat  (3202291)  41845579776000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-1)\;64),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(1)\;192),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-17)\;15360),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(31)\;161280),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;23224320),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;1277337600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;1594117324800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;41845579776000)\text{]},  [(mkRat  (1)  384),  (mkRat  (0)  1),  (mkRat  (−1)  384),  (mkRat  (0)  1),  (mkRat  (17)  18432),  (mkRat  (0)  1),  (mkRat  (−31)  138240),  (mkRat  (0)  1),  (mkRat  (691)  15482880),  (mkRat  (0)  1),  (mkRat  (−5461)  696729600),  (mkRat  (0)  1),  (mkRat  (929569)  735746457600),  (mkRat  (0)  1),  (mkRat  (−3202291)  16738231910400),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(1)\;384),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-1)\;384),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(17)\;18432),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-31)\;138240),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(691)\;15482880),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;696729600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;735746457600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;16738231910400),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (1)  1536),  (mkRat  (0)  1),  (mkRat  (−17)  36864),  (mkRat  (0)  1),  (mkRat  (31)  184320),  (mkRat  (0)  1),  (mkRat  (−691)  15482880),  (mkRat  (0)  1),  (mkRat  (5461)  557383680),  (mkRat  (0)  1),  (mkRat  (−929569)  490497638400),  (mkRat  (0)  1),  (mkRat  (3202291)  9564703948800),  (mkRat  (0)  1),  (mkRat  (−221930581)  4017175658496000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(1)\;1536),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-17)\;36864),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(31)\;184320),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;15482880),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;557383680),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;490497638400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;9564703948800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;4017175658496000)\text{]},  [(mkRat  (−1)  15360),  (mkRat  (0)  1),  (mkRat  (17)  122880),  (mkRat  (0)  1),  (mkRat  (−31)  368640),  (mkRat  (0)  1),  (mkRat  (691)  22118400),  (mkRat  (0)  1),  (mkRat  (−5461)  619315200),  (mkRat  (0)  1),  (mkRat  (929569)  445906944000),  (mkRat  (0)  1),  (mkRat  (−3202291)  7357464576000),  (mkRat  (0)  1),  (mkRat  (221930581)  2678117105664000),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(-1)\;15360),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(17)\;122880),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-31)\;368640),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(691)\;22118400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;619315200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;445906944000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;7357464576000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;2678117105664000),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (−17)  737280),  (mkRat  (0)  1),  (mkRat  (31)  1105920),  (mkRat  (0)  1),  (mkRat  (−691)  44236800),  (mkRat  (0)  1),  (mkRat  (5461)  928972800),  (mkRat  (0)  1),  (mkRat  (−929569)  535088332800),  (mkRat  (0)  1),  (mkRat  (3202291)  7357464576000),  (mkRat  (0)  1),  (mkRat  (−221930581)  2295528947712000),  (mkRat  (0)  1),  (mkRat  (4722116521)  241030539509760000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-17)\;737280),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(31)\;1105920),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;44236800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;928972800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;535088332800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;7357464576000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;2295528947712000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(4722116521)\;241030539509760000)\text{]},  [(mkRat  (17)  10321920),  (mkRat  (0)  1),  (mkRat  (−31)  5160960),  (mkRat  (0)  1),  (mkRat  (691)  123863040),  (mkRat  (0)  1),  (mkRat  (−5461)  1857945600),  (mkRat  (0)  1),  (mkRat  (929569)  832359628800),  (mkRat  (0)  1),  (mkRat  (−3202291)  9364045824000),  (mkRat  (0)  1),  (mkRat  (221930581)  2472108097536000),  (mkRat  (0)  1),  (mkRat  (−4722116521)  224961836875776000),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(17)\;10321920),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-31)\;5160960),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(691)\;123863040),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;1857945600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;832359628800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;9364045824000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;2472108097536000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-4722116521)\;224961836875776000),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (31)  41287680),  (mkRat  (0)  1),  (mkRat  (−691)  495452160),  (mkRat  (0)  1),  (mkRat  (5461)  4954521600),  (mkRat  (0)  1),  (mkRat  (−929569)  1664719257600),  (mkRat  (0)  1),  (mkRat  (3202291)  14982473318400),  (mkRat  (0)  1),  (mkRat  (−221930581)  3296144130048000),  (mkRat  (0)  1),  (mkRat  (4722116521)  257099242143744000),  (mkRat  (0)  1),  (mkRat  (−968383680827)  215963363400744960000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(31)\;41287680),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;495452160),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;4954521600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;1664719257600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;14982473318400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;3296144130048000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(4722116521)\;257099242143744000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-968383680827)\;215963363400744960000)\text{]},  [(mkRat  (−31)  743178240),  (mkRat  (0)  1),  (mkRat  (691)  2972712960),  (mkRat  (0)  1),  (mkRat  (−5461)  17836277760),  (mkRat  (0)  1),  (mkRat  (929569)  4280706662400),  (mkRat  (0)  1),  (mkRat  (−3202291)  29964946636800),  (mkRat  (0)  1),  (mkRat  (221930581)  5393690394624000),  (mkRat  (0)  1),  (mkRat  (−4722116521)  355983566045184000),  (mkRat  (0)  1),  (mkRat  (968383680827)  259156036080893952000),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(-31)\;743178240),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(691)\;2972712960),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;17836277760),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;4280706662400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;29964946636800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;5393690394624000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-4722116521)\;355983566045184000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(968383680827)\;259156036080893952000),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (−691)  29727129600),  (mkRat  (0)  1),  (mkRat  (5461)  89181388800),  (mkRat  (0)  1),  (mkRat  (−929569)  14269022208000),  (mkRat  (0)  1),  (mkRat  (3202291)  74912366592000),  (mkRat  (0)  1),  (mkRat  (−221930581)  10787380789248000),  (mkRat  (0)  1),  (mkRat  (4722116521)  593305943408640000),  (mkRat  (0)  1),  (mkRat  (−968383680827)  370222908686991360000),  (mkRat  (0)  1),  (mkRat  (14717667114151)  19436702706067046400000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;29727129600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;89181388800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;14269022208000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;74912366592000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;10787380789248000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(4722116521)\;593305943408640000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-968383680827)\;370222908686991360000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(14717667114151)\;19436702706067046400000)\text{]},  [(mkRat  (691)  653996851200),  (mkRat  (0)  1),  (mkRat  (−5461)  653996851200),  (mkRat  (0)  1),  (mkRat  (929569)  62783697715200),  (mkRat  (0)  1),  (mkRat  (−3202291)  235438866432000),  (mkRat  (0)  1),  (mkRat  (221930581)  26369153040384000),  (mkRat  (0)  1),  (mkRat  (−4722116521)  1186611886817280000),  (mkRat  (0)  1),  (mkRat  (968383680827)  626531076239523840000),  (mkRat  (0)  1),  (mkRat  (−14717667114151)  28507163968898334720000),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(691)\;653996851200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;653996851200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;62783697715200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;235438866432000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;26369153040384000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-4722116521)\;1186611886817280000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(968383680827)\;626531076239523840000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-14717667114151)\;28507163968898334720000),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (5461)  7847962214400),  (mkRat  (0)  1),  (mkRat  (−929569)  376702186291200),  (mkRat  (0)  1),  (mkRat  (3202291)  941755465728000),  (mkRat  (0)  1),  (mkRat  (−221930581)  79107459121152000),  (mkRat  (0)  1),  (mkRat  (4722116521)  2847868528361472000),  (mkRat  (0)  1),  (mkRat  (−968383680827)  1253062152479047680000),  (mkRat  (0)  1),  (mkRat  (14717667114151)  48869423946682859520000),  (mkRat  (0)  1),  (mkRat  (−2093660879252671)  20525158057606800998400000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;7847962214400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;376702186291200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;941755465728000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;79107459121152000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(4722116521)\;2847868528361472000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-968383680827)\;1253062152479047680000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(14717667114151)\;48869423946682859520000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-2093660879252671)\;20525158057606800998400000)\text{]},  [(mkRat  (−5461)  204047017574400),  (mkRat  (0)  1),  (mkRat  (929569)  3264752281190400),  (mkRat  (0)  1),  (mkRat  (−3202291)  4897128421785600),  (mkRat  (0)  1),  (mkRat  (221930581)  293827705307136000),  (mkRat  (0)  1),  (mkRat  (−4722116521)  8227175748599808000),  (mkRat  (0)  1),  (mkRat  (968383680827)  2961783269495930880000),  (mkRat  (0)  1),  (mkRat  (−14717667114151)  97738847893365719040000),  (mkRat  (0)  1),  (mkRat  (2093660879252671)  35576940633185121730560000),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(-5461)\;204047017574400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;3264752281190400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;4897128421785600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;293827705307136000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-4722116521)\;8227175748599808000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(968383680827)\;2961783269495930880000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-14717667114151)\;97738847893365719040000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(2093660879252671)\;35576940633185121730560000),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (−929569)  45706531936665600),  (mkRat  (0)  1),  (mkRat  (3202291)  34279898952499200),  (mkRat  (0)  1),  (mkRat  (−221930581)  1371195958099968000),  (mkRat  (0)  1),  (mkRat  (4722116521)  28795115120099328000),  (mkRat  (0)  1),  (mkRat  (−968383680827)  8292993154588606464000),  (mkRat  (0)  1),  (mkRat  (14717667114151)  228057311751186677760000),  (mkRat  (0)  1),  (mkRat  (−2093660879252671)  71153881266370243461120000),  (mkRat  (0)  1),  (mkRat  (86125672563201181)  7471157532968875563417600000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;45706531936665600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;34279898952499200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;1371195958099968000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(4722116521)\;28795115120099328000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-968383680827)\;8292993154588606464000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(14717667114151)\;228057311751186677760000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-2093660879252671)\;71153881266370243461120000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(86125672563201181)\;7471157532968875563417600000)\text{]},  [(mkRat  (929569)  1371195958099968000),  (mkRat  (0)  1),  (mkRat  (−3202291)  342798989524992000),  (mkRat  (0)  1),  (mkRat  (221930581)  8227175748599808000),  (mkRat  (0)  1),  (mkRat  (−4722116521)  123407636228997120000),  (mkRat  (0)  1),  (mkRat  (968383680827)  27643310515295354880000),  (mkRat  (0)  1),  (mkRat  (−14717667114151)  621974486594145484800000),  (mkRat  (0)  1),  (mkRat  (2093660879252671)  164201264460854407987200000),  (mkRat  (0)  1),  (mkRat  (−86125672563201181)  14942315065937751126835200000),  (mkRat  (0)  1)]]\;\text{[}(\text{mkRat}\;(929569)\;1371195958099968000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;342798989524992000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;8227175748599808000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-4722116521)\;123407636228997120000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(968383680827)\;27643310515295354880000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-14717667114151)\;621974486594145484800000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(2093660879252671)\;164201264460854407987200000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-86125672563201181)\;14942315065937751126835200000),\;(\text{mkRat}\;(0)\;1)\text{]}\text{]}
Lean source · 17 lines
def forsetiTable : List (List ℚ) := [
    [(mkRat (1) 2), (mkRat (1) 4), (mkRat (0) 1), (mkRat (-1) 48), (mkRat (0) 1), (mkRat (1) 480), (mkRat (0) 1), (mkRat (-17) 80640), (mkRat (0) 1), (mkRat (31) 1451520), (mkRat (0) 1), (mkRat (-691) 319334400), (mkRat (0) 1), (mkRat (5461) 24908083200), (mkRat (0) 1), (mkRat (-929569) 41845579776000)],
    [(mkRat (-1) 8), (mkRat (0) 1), (mkRat (1) 32), (mkRat (0) 1), (mkRat (-1) 192), (mkRat (0) 1), (mkRat (17) 23040), (mkRat (0) 1), (mkRat (-31) 322560), (mkRat (0) 1), (mkRat (691) 58060800), (mkRat (0) 1), (mkRat (-5461) 3832012800), (mkRat (0) 1), (mkRat (929569) 5579410636800), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (-1) 64), (mkRat (0) 1), (mkRat (1) 192), (mkRat (0) 1), (mkRat (-17) 15360), (mkRat (0) 1), (mkRat (31) 161280), (mkRat (0) 1), (mkRat (-691) 23224320), (mkRat (0) 1), (mkRat (5461) 1277337600), (mkRat (0) 1), (mkRat (-929569) 1594117324800), (mkRat (0) 1), (mkRat (3202291) 41845579776000)],
    [(mkRat (1) 384), (mkRat (0) 1), (mkRat (-1) 384), (mkRat (0) 1), (mkRat (17) 18432), (mkRat (0) 1), (mkRat (-31) 138240), (mkRat (0) 1), (mkRat (691) 15482880), (mkRat (0) 1), (mkRat (-5461) 696729600), (mkRat (0) 1), (mkRat (929569) 735746457600), (mkRat (0) 1), (mkRat (-3202291) 16738231910400), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (1) 1536), (mkRat (0) 1), (mkRat (-17) 36864), (mkRat (0) 1), (mkRat (31) 184320), (mkRat (0) 1), (mkRat (-691) 15482880), (mkRat (0) 1), (mkRat (5461) 557383680), (mkRat (0) 1), (mkRat (-929569) 490497638400), (mkRat (0) 1), (mkRat (3202291) 9564703948800), (mkRat (0) 1), (mkRat (-221930581) 4017175658496000)],
    [(mkRat (-1) 15360), (mkRat (0) 1), (mkRat (17) 122880), (mkRat (0) 1), (mkRat (-31) 368640), (mkRat (0) 1), (mkRat (691) 22118400), (mkRat (0) 1), (mkRat (-5461) 619315200), (mkRat (0) 1), (mkRat (929569) 445906944000), (mkRat (0) 1), (mkRat (-3202291) 7357464576000), (mkRat (0) 1), (mkRat (221930581) 2678117105664000), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (-17) 737280), (mkRat (0) 1), (mkRat (31) 1105920), (mkRat (0) 1), (mkRat (-691) 44236800), (mkRat (0) 1), (mkRat (5461) 928972800), (mkRat (0) 1), (mkRat (-929569) 535088332800), (mkRat (0) 1), (mkRat (3202291) 7357464576000), (mkRat (0) 1), (mkRat (-221930581) 2295528947712000), (mkRat (0) 1), (mkRat (4722116521) 241030539509760000)],
    [(mkRat (17) 10321920), (mkRat (0) 1), (mkRat (-31) 5160960), (mkRat (0) 1), (mkRat (691) 123863040), (mkRat (0) 1), (mkRat (-5461) 1857945600), (mkRat (0) 1), (mkRat (929569) 832359628800), (mkRat (0) 1), (mkRat (-3202291) 9364045824000), (mkRat (0) 1), (mkRat (221930581) 2472108097536000), (mkRat (0) 1), (mkRat (-4722116521) 224961836875776000), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (31) 41287680), (mkRat (0) 1), (mkRat (-691) 495452160), (mkRat (0) 1), (mkRat (5461) 4954521600), (mkRat (0) 1), (mkRat (-929569) 1664719257600), (mkRat (0) 1), (mkRat (3202291) 14982473318400), (mkRat (0) 1), (mkRat (-221930581) 3296144130048000), (mkRat (0) 1), (mkRat (4722116521) 257099242143744000), (mkRat (0) 1), (mkRat (-968383680827) 215963363400744960000)],
    [(mkRat (-31) 743178240), (mkRat (0) 1), (mkRat (691) 2972712960), (mkRat (0) 1), (mkRat (-5461) 17836277760), (mkRat (0) 1), (mkRat (929569) 4280706662400), (mkRat (0) 1), (mkRat (-3202291) 29964946636800), (mkRat (0) 1), (mkRat (221930581) 5393690394624000), (mkRat (0) 1), (mkRat (-4722116521) 355983566045184000), (mkRat (0) 1), (mkRat (968383680827) 259156036080893952000), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (-691) 29727129600), (mkRat (0) 1), (mkRat (5461) 89181388800), (mkRat (0) 1), (mkRat (-929569) 14269022208000), (mkRat (0) 1), (mkRat (3202291) 74912366592000), (mkRat (0) 1), (mkRat (-221930581) 10787380789248000), (mkRat (0) 1), (mkRat (4722116521) 593305943408640000), (mkRat (0) 1), (mkRat (-968383680827) 370222908686991360000), (mkRat (0) 1), (mkRat (14717667114151) 19436702706067046400000)],
    [(mkRat (691) 653996851200), (mkRat (0) 1), (mkRat (-5461) 653996851200), (mkRat (0) 1), (mkRat (929569) 62783697715200), (mkRat (0) 1), (mkRat (-3202291) 235438866432000), (mkRat (0) 1), (mkRat (221930581) 26369153040384000), (mkRat (0) 1), (mkRat (-4722116521) 1186611886817280000), (mkRat (0) 1), (mkRat (968383680827) 626531076239523840000), (mkRat (0) 1), (mkRat (-14717667114151) 28507163968898334720000), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (5461) 7847962214400), (mkRat (0) 1), (mkRat (-929569) 376702186291200), (mkRat (0) 1), (mkRat (3202291) 941755465728000), (mkRat (0) 1), (mkRat (-221930581) 79107459121152000), (mkRat (0) 1), (mkRat (4722116521) 2847868528361472000), (mkRat (0) 1), (mkRat (-968383680827) 1253062152479047680000), (mkRat (0) 1), (mkRat (14717667114151) 48869423946682859520000), (mkRat (0) 1), (mkRat (-2093660879252671) 20525158057606800998400000)],
    [(mkRat (-5461) 204047017574400), (mkRat (0) 1), (mkRat (929569) 3264752281190400), (mkRat (0) 1), (mkRat (-3202291) 4897128421785600), (mkRat (0) 1), (mkRat (221930581) 293827705307136000), (mkRat (0) 1), (mkRat (-4722116521) 8227175748599808000), (mkRat (0) 1), (mkRat (968383680827) 2961783269495930880000), (mkRat (0) 1), (mkRat (-14717667114151) 97738847893365719040000), (mkRat (0) 1), (mkRat (2093660879252671) 35576940633185121730560000), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (-929569) 45706531936665600), (mkRat (0) 1), (mkRat (3202291) 34279898952499200), (mkRat (0) 1), (mkRat (-221930581) 1371195958099968000), (mkRat (0) 1), (mkRat (4722116521) 28795115120099328000), (mkRat (0) 1), (mkRat (-968383680827) 8292993154588606464000), (mkRat (0) 1), (mkRat (14717667114151) 228057311751186677760000), (mkRat (0) 1), (mkRat (-2093660879252671) 71153881266370243461120000), (mkRat (0) 1), (mkRat (86125672563201181) 7471157532968875563417600000)],
    [(mkRat (929569) 1371195958099968000), (mkRat (0) 1), (mkRat (-3202291) 342798989524992000), (mkRat (0) 1), (mkRat (221930581) 8227175748599808000), (mkRat (0) 1), (mkRat (-4722116521) 123407636228997120000), (mkRat (0) 1), (mkRat (968383680827) 27643310515295354880000), (mkRat (0) 1), (mkRat (-14717667114151) 621974486594145484800000), (mkRat (0) 1), (mkRat (2093660879252671) 164201264460854407987200000), (mkRat (0) 1), (mkRat (-86125672563201181) 14942315065937751126835200000), (mkRat (0) 1)]]

Definition forsetiQ (k : Gimle.Asgard.Streams.Lowering.Degrees 2) : ℚ L576–576

Namespace Notebook.Burgers.Decided_front_band_decided

(forsetiTable.getD  (k  0)  []).getD  (k  1)  0(\text{forsetiTable}.\text{getD}\;(\text{k}\;0)\;\text{[}\text{]}).\text{getD}\;(\text{k}\;1)\;0
Lean source · 1 line
def forsetiQ (k : Gimle.Asgard.Streams.Lowering.Degrees 2) : ℚ := (forsetiTable.getD (k 0) []).getD (k 1) 0

Definition forsetiRoot : Prop L578–585

Namespace Notebook.Burgers.Decided_front_band_decided

∀  a  unused  v  :  Gimle.Asgard.Streams.Stream  2,\forall \;\text{a}\;\text{unused}\;\text{v}\;:\;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{Stream}\;2,  (Gimle.Asgard.Streams.Burgers.circuit  .ogf  (mkRat  (1)  2)).Rel\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{Burgers}.\text{circuit}\;.\text{ogf}\;(\text{mkRat}\;(1)\;2)).\text{Rel}  ![a,  Gimle.Asgard.Streams.ColeHopf.zeroSlice  (Gimle.Asgard.Streams.ColeHopf.front  (mkRat  (1)  2)  [((mkRat  (1)  1),  (mkRat  (0)  1)),  ((mkRat  (1)  1),  (mkRat  (−1)  1))]),  unused]  ![v,  a]  →\;!\text{[}\text{a},\;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{ColeHopf}.\text{zeroSlice}\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{ColeHopf}.\text{front}\;(\text{mkRat}\;(1)\;2)\;\text{[}((\text{mkRat}\;(1)\;1),\;(\text{mkRat}\;(0)\;1)),\;((\text{mkRat}\;(1)\;1),\;(\text{mkRat}\;(-1)\;1))\text{]}),\;\text{unused}\text{]}\;!\text{[}\text{v},\;\text{a}\text{]}\;\to   ∀  x,  forsetiBox.Mem  x  →\;\forall \;\text{x},\;\text{forsetiBox}.\text{Mem}\;\text{x}\;\to   HasSum  (Gimle.Asgard.Streams.seriesTerm  .ogf  a  x)\;\text{HasSum}\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{seriesTerm}\;.\text{ogf}\;\text{a}\;\text{x})  (Gimle.Asgard.Streams.analyticField  .ogf  a  x)  ∧\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{analyticField}\;.\text{ogf}\;\text{a}\;\text{x})\;\land   (((mkRat  (2)  5)  :  Q)  :  R)  ≤  Gimle.Asgard.Streams.analyticField  .ogf  a  x  ∧  Gimle.Asgard.Streams.analyticField  .ogf  a  x  ≤  (((mkRat  (3)  5)  :  Q)  :  R)\;(((\text{mkRat}\;(2)\;5)\;:\;\mathbb{Q} )\;:\;\mathbb{R} )\;\le \;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{analyticField}\;.\text{ogf}\;\text{a}\;\text{x}\;\land \;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{analyticField}\;.\text{ogf}\;\text{a}\;\text{x}\;\le \;(((\text{mkRat}\;(3)\;5)\;:\;\mathbb{Q} )\;:\;\mathbb{R} )
Lean source · 8 lines
def forsetiRoot : Prop :=
  ∀ a unused v : Gimle.Asgard.Streams.Stream 2,
      (Gimle.Asgard.Streams.Burgers.circuit .ogf (mkRat (1) 2)).Rel
        ![a, Gimle.Asgard.Streams.ColeHopf.zeroSlice (Gimle.Asgard.Streams.ColeHopf.front (mkRat (1) 2) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))]), unused] ![v, a] →
    ∀ x, forsetiBox.Mem x →
      HasSum (Gimle.Asgard.Streams.seriesTerm .ogf a x)
        (Gimle.Asgard.Streams.analyticField .ogf a x) ∧
      (((mkRat (2) 5) : ℚ) : ℝ) ≤ Gimle.Asgard.Streams.analyticField .ogf a x ∧ Gimle.Asgard.Streams.analyticField .ogf a x ≤ (((mkRat (3) 5) : ℚ) : ℝ)

Theorem front_band_decided Kernel checkedAs recorded L587–635

Namespace Notebook.Burgers.Decided_front_band_decided

u is the stream the Burgers circuit at viscosity 1/2 rebuilds from the t = 0 slice of the Cole–Hopf front −2ν φ_x/φ of the potential Σ cᵢ·e^(aᵢx) given by the pairs (cᵢ, aᵢ), u_t its other output; its series converges at every point of the box, and its sum, the analytic field, stays within the band there. The stream decider proved it. Goal (stream): stream burgers viscosity 1/2 interpretation analytic-field basis ogf potential exponentials [1, 0], [1, -1] field u over t in [-1/6, 1/6], x in [-1/8, 1/8] : u >= 2/5 and u <= 3/5

Statement
have  circuit\text{have}\;\text{circuit}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 49 lines
/-- u is the stream the Burgers circuit at viscosity 1/2 rebuilds from the t = 0 slice of the Cole–Hopf front −2ν φ_x/φ of the potential Σ cᵢ·e^(aᵢx) given by the pairs (cᵢ, aᵢ), u_t its other output; its series converges at every point of the box, and its sum, the analytic field, stays within the band there. The stream decider proved it. Goal (stream): stream burgers viscosity 1/2 interpretation analytic-field basis ogf potential exponentials [1, 0], [1, -1] field u over t in [-1/6, 1/6], x in [-1/8, 1/8] : u >= 2/5 and u <= 3/5 -/
theorem front_band_decided :
    have circuit := Gimle.Asgard.Streams.Burgers.circuit .ogf (1/2)
    have slice := Gimle.Asgard.Streams.ColeHopf.zeroSlice
      (Gimle.Asgard.Streams.ColeHopf.front (1/2) [(1, 0), (1, -1)])
    ∀ u unused u_t : Gimle.Asgard.Streams.Stream 2,
      circuit.Rel ![u, slice, unused] ![u_t, u] →
      ∀ t x : ℝ, |t| ≤ 1/6 ∧ |x| ≤ 1/8 →
        HasSum (Gimle.Asgard.Streams.seriesTerm .ogf u ![t, x])
          (Gimle.Asgard.Streams.analyticField .ogf u ![t, x]) ∧
        2/5 ≤ Gimle.Asgard.Streams.analyticField .ogf u ![t, x] ∧
        Gimle.Asgard.Streams.analyticField .ogf u ![t, x] ≤ 3/5 := by
  have root : forsetiRoot := by
    unfold forsetiRoot
    intro a unused v rel x hx
    refine ⟨?_, (Gimle.Asgard.Streams.ColeHopf.front_band_of_window (lo := ((mkRat (2) 5) : ℚ)) (hi := ((mkRat (3) 5) : ℚ)) (ε := (mkRat (1) 16384)) (show (0 : ℚ) < ((mkRat (1) 2) : ℚ) by decide +kernel) (show (0 : ℚ) < ((mkRat (1) 1) : ℚ) by decide +kernel) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))] (show Gimle.Asgard.Streams.ColeHopf.constantTerm [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))] ≠ 0 by decide +kernel) (by decide +kernel) (r := forsetiRadii) (by decide +kernel) (by decide +kernel) (by decide +kernel) forsetiBox (by decide +kernel) ![16, 16] (by decide +kernel) (by decide +kernel) (Q := forsetiQ) (by decide +kernel) (by decide +kernel) (by decide +kernel) a unused v rel x hx)⟩
    have hc : MvPowerSeries.constantCoeff (Gimle.Asgard.Streams.ColeHopf.expSumHeat ((mkRat (1) 2) : ℚ) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))]) ≠ 0 := by
      rw [Gimle.Asgard.Streams.ColeHopf.constantCoeff_expSumHeat]
      decide +kernel
    simp only [Gimle.Asgard.Streams.ColeHopf.front] at rel
    rw [Gimle.Asgard.Streams.ColeHopf.candidate_quotient ((mkRat (1) 2) : ℚ) _ hc (Gimle.Asgard.Streams.ColeHopf.heatSeries_pde ((mkRat (1) 2) : ℚ) _) a unused v rel]
    exact (Gimle.Asgard.Streams.ColeHopf.certificate (show (0 : ℚ) < ((mkRat (1) 2) : ℚ) by decide +kernel) (show (0 : ℚ) < ((mkRat (1) 1) : ℚ) by decide +kernel) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))] (by decide +kernel) (r := forsetiRadii) (by decide +kernel) (by decide +kernel) (by decide +kernel) forsetiBox (by decide +kernel)).hasSum hx
  have forsetiFront : Gimle.Asgard.Streams.ColeHopf.front (mkRat (1) 2) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))] = Gimle.Asgard.Streams.ColeHopf.front (1/2) [(1, 0), (1, -1)] := by norm_num [Rat.mkRat_eq_div]
  have forsetiCircuit : Gimle.Asgard.Streams.Burgers.circuit .ogf (mkRat (1) 2) = Gimle.Asgard.Streams.Burgers.circuit .ogf (1/2) := by norm_num [Rat.mkRat_eq_div]
  have forsetiInside : ∀ t x : ℝ, forsetiBox.Mem ![t, x] ↔ |t| ≤ 1/6 ∧ |x| ≤ 1/8 := by
    intro t x
    norm_num [Gimle.Asgard.Streams.Box.Mem, Fin.forall_fin_two, forsetiBox, Rat.mkRat_eq_div]
  have forsetiCast0 : (((mkRat (2) 5) : ℚ) : ℝ) = (2/5) := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast1 : (((mkRat (3) 5) : ℚ) : ℝ) = (3/5) := by norm_num [Rat.mkRat_eq_div]
  refine (fun (bridge : _ ↔ forsetiRoot) => bridge.mpr root) ?_
  constructor
  · intro claim
    dsimp only at claim
    unfold forsetiRoot
    rw [forsetiFront, forsetiCircuit]
    intro u unused u_t rel z inside
    have point : ![z 0, z 1] = z := by funext i; fin_cases i <;> rfl
    have holds := claim u unused u_t rel (z 0) (z 1) ((forsetiInside _ _).mp (point ▸ inside))
    rw [point] at holds
    set_option linter.unusedSimpArgs false in simp only [forsetiCast0, forsetiCast1]
    exact holds
  · intro lane
    unfold forsetiRoot at lane
    rw [forsetiFront, forsetiCircuit] at lane
    dsimp only
    intro u unused u_t rel t x inside
    have holds := lane u unused u_t rel ![t, x] ((forsetiInside t x).mpr inside)
    set_option linter.unusedSimpArgs false in simp only [forsetiCast0, forsetiCast1] at holds
    exact holds

Refute the tighter upper bound

At (t,x)=(16,−18)(t,x)=(\tfrac16,-\tfrac18), the window exceeds 2750\tfrac{27}{50} by more than the certified error. Lean checks the counterexample; the positive claim below remains refuted, not proved by its sorry.1 Contains sorry 1 As recorded
end Decided_front_band_decided
L645–645
Decisionfront_band_refuted · stream · forsetiNever runL648–650
stream burgers viscosity 1/2 interpretation analytic-field basis ogf potential exponentials [1, 0], [1, -1] field u over t in [-1/6, 1/6], x in [-1/8, 1/8] : u <= 27/50

Not run yet.

namespace Decided_front_band_refuted
L652–652

Definition forsetiBox : Gimle.Asgard.Streams.Box 2 L654–655

Namespace Notebook.Burgers.Decided_front_band_refuted

⟨![(mkRat  (1)  6),  (mkRat  (1)  8)],  by  decide  +kernel⟩\langle !\text{[}(\text{mkRat}\;(1)\;6),\;(\text{mkRat}\;(1)\;8)\text{]},\;\text{by}\;\text{decide}\;+\text{kernel}\rangle
Lean source · 2 lines
def forsetiBox : Gimle.Asgard.Streams.Box 2 :=
  ⟨![(mkRat (1) 6), (mkRat (1) 8)], by decide +kernel⟩

Definition forsetiRadii : Fin 2 → ℚ L657–657

Namespace Notebook.Burgers.Decided_front_band_refuted

![(mkRat  (2)  3),  (mkRat  (1)  2)]!\text{[}(\text{mkRat}\;(2)\;3),\;(\text{mkRat}\;(1)\;2)\text{]}
Lean source · 1 line
def forsetiRadii : Fin 2 → ℚ := ![(mkRat (2) 3), (mkRat (1) 2)]

Definition forsetiTable : List (List ℚ) L659–675

Namespace Notebook.Burgers.Decided_front_band_refuted

[\text{[}  [(mkRat  (1)  2),  (mkRat  (1)  4),  (mkRat  (0)  1),  (mkRat  (−1)  48),  (mkRat  (0)  1),  (mkRat  (1)  480),  (mkRat  (0)  1),  (mkRat  (−17)  80640),  (mkRat  (0)  1),  (mkRat  (31)  1451520),  (mkRat  (0)  1),  (mkRat  (−691)  319334400),  (mkRat  (0)  1),  (mkRat  (5461)  24908083200),  (mkRat  (0)  1),  (mkRat  (−929569)  41845579776000)],\;\text{[}(\text{mkRat}\;(1)\;2),\;(\text{mkRat}\;(1)\;4),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-1)\;48),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(1)\;480),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-17)\;80640),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(31)\;1451520),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;319334400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;24908083200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;41845579776000)\text{]},  [(mkRat  (−1)  8),  (mkRat  (0)  1),  (mkRat  (1)  32),  (mkRat  (0)  1),  (mkRat  (−1)  192),  (mkRat  (0)  1),  (mkRat  (17)  23040),  (mkRat  (0)  1),  (mkRat  (−31)  322560),  (mkRat  (0)  1),  (mkRat  (691)  58060800),  (mkRat  (0)  1),  (mkRat  (−5461)  3832012800),  (mkRat  (0)  1),  (mkRat  (929569)  5579410636800),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(-1)\;8),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(1)\;32),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-1)\;192),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(17)\;23040),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-31)\;322560),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(691)\;58060800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;3832012800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;5579410636800),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (−1)  64),  (mkRat  (0)  1),  (mkRat  (1)  192),  (mkRat  (0)  1),  (mkRat  (−17)  15360),  (mkRat  (0)  1),  (mkRat  (31)  161280),  (mkRat  (0)  1),  (mkRat  (−691)  23224320),  (mkRat  (0)  1),  (mkRat  (5461)  1277337600),  (mkRat  (0)  1),  (mkRat  (−929569)  1594117324800),  (mkRat  (0)  1),  (mkRat  (3202291)  41845579776000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-1)\;64),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(1)\;192),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-17)\;15360),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(31)\;161280),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;23224320),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;1277337600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;1594117324800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;41845579776000)\text{]},  [(mkRat  (1)  384),  (mkRat  (0)  1),  (mkRat  (−1)  384),  (mkRat  (0)  1),  (mkRat  (17)  18432),  (mkRat  (0)  1),  (mkRat  (−31)  138240),  (mkRat  (0)  1),  (mkRat  (691)  15482880),  (mkRat  (0)  1),  (mkRat  (−5461)  696729600),  (mkRat  (0)  1),  (mkRat  (929569)  735746457600),  (mkRat  (0)  1),  (mkRat  (−3202291)  16738231910400),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(1)\;384),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-1)\;384),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(17)\;18432),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-31)\;138240),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(691)\;15482880),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;696729600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;735746457600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;16738231910400),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (1)  1536),  (mkRat  (0)  1),  (mkRat  (−17)  36864),  (mkRat  (0)  1),  (mkRat  (31)  184320),  (mkRat  (0)  1),  (mkRat  (−691)  15482880),  (mkRat  (0)  1),  (mkRat  (5461)  557383680),  (mkRat  (0)  1),  (mkRat  (−929569)  490497638400),  (mkRat  (0)  1),  (mkRat  (3202291)  9564703948800),  (mkRat  (0)  1),  (mkRat  (−221930581)  4017175658496000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(1)\;1536),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-17)\;36864),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(31)\;184320),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;15482880),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;557383680),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;490497638400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;9564703948800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;4017175658496000)\text{]},  [(mkRat  (−1)  15360),  (mkRat  (0)  1),  (mkRat  (17)  122880),  (mkRat  (0)  1),  (mkRat  (−31)  368640),  (mkRat  (0)  1),  (mkRat  (691)  22118400),  (mkRat  (0)  1),  (mkRat  (−5461)  619315200),  (mkRat  (0)  1),  (mkRat  (929569)  445906944000),  (mkRat  (0)  1),  (mkRat  (−3202291)  7357464576000),  (mkRat  (0)  1),  (mkRat  (221930581)  2678117105664000),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(-1)\;15360),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(17)\;122880),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-31)\;368640),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(691)\;22118400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;619315200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;445906944000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;7357464576000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;2678117105664000),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (−17)  737280),  (mkRat  (0)  1),  (mkRat  (31)  1105920),  (mkRat  (0)  1),  (mkRat  (−691)  44236800),  (mkRat  (0)  1),  (mkRat  (5461)  928972800),  (mkRat  (0)  1),  (mkRat  (−929569)  535088332800),  (mkRat  (0)  1),  (mkRat  (3202291)  7357464576000),  (mkRat  (0)  1),  (mkRat  (−221930581)  2295528947712000),  (mkRat  (0)  1),  (mkRat  (4722116521)  241030539509760000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-17)\;737280),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(31)\;1105920),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;44236800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;928972800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;535088332800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;7357464576000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;2295528947712000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(4722116521)\;241030539509760000)\text{]},  [(mkRat  (17)  10321920),  (mkRat  (0)  1),  (mkRat  (−31)  5160960),  (mkRat  (0)  1),  (mkRat  (691)  123863040),  (mkRat  (0)  1),  (mkRat  (−5461)  1857945600),  (mkRat  (0)  1),  (mkRat  (929569)  832359628800),  (mkRat  (0)  1),  (mkRat  (−3202291)  9364045824000),  (mkRat  (0)  1),  (mkRat  (221930581)  2472108097536000),  (mkRat  (0)  1),  (mkRat  (−4722116521)  224961836875776000),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(17)\;10321920),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-31)\;5160960),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(691)\;123863040),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;1857945600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;832359628800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;9364045824000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;2472108097536000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-4722116521)\;224961836875776000),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (31)  41287680),  (mkRat  (0)  1),  (mkRat  (−691)  495452160),  (mkRat  (0)  1),  (mkRat  (5461)  4954521600),  (mkRat  (0)  1),  (mkRat  (−929569)  1664719257600),  (mkRat  (0)  1),  (mkRat  (3202291)  14982473318400),  (mkRat  (0)  1),  (mkRat  (−221930581)  3296144130048000),  (mkRat  (0)  1),  (mkRat  (4722116521)  257099242143744000),  (mkRat  (0)  1),  (mkRat  (−968383680827)  215963363400744960000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(31)\;41287680),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;495452160),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;4954521600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;1664719257600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;14982473318400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;3296144130048000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(4722116521)\;257099242143744000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-968383680827)\;215963363400744960000)\text{]},  [(mkRat  (−31)  743178240),  (mkRat  (0)  1),  (mkRat  (691)  2972712960),  (mkRat  (0)  1),  (mkRat  (−5461)  17836277760),  (mkRat  (0)  1),  (mkRat  (929569)  4280706662400),  (mkRat  (0)  1),  (mkRat  (−3202291)  29964946636800),  (mkRat  (0)  1),  (mkRat  (221930581)  5393690394624000),  (mkRat  (0)  1),  (mkRat  (−4722116521)  355983566045184000),  (mkRat  (0)  1),  (mkRat  (968383680827)  259156036080893952000),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(-31)\;743178240),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(691)\;2972712960),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;17836277760),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;4280706662400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;29964946636800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;5393690394624000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-4722116521)\;355983566045184000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(968383680827)\;259156036080893952000),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (−691)  29727129600),  (mkRat  (0)  1),  (mkRat  (5461)  89181388800),  (mkRat  (0)  1),  (mkRat  (−929569)  14269022208000),  (mkRat  (0)  1),  (mkRat  (3202291)  74912366592000),  (mkRat  (0)  1),  (mkRat  (−221930581)  10787380789248000),  (mkRat  (0)  1),  (mkRat  (4722116521)  593305943408640000),  (mkRat  (0)  1),  (mkRat  (−968383680827)  370222908686991360000),  (mkRat  (0)  1),  (mkRat  (14717667114151)  19436702706067046400000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-691)\;29727129600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;89181388800),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;14269022208000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;74912366592000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;10787380789248000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(4722116521)\;593305943408640000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-968383680827)\;370222908686991360000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(14717667114151)\;19436702706067046400000)\text{]},  [(mkRat  (691)  653996851200),  (mkRat  (0)  1),  (mkRat  (−5461)  653996851200),  (mkRat  (0)  1),  (mkRat  (929569)  62783697715200),  (mkRat  (0)  1),  (mkRat  (−3202291)  235438866432000),  (mkRat  (0)  1),  (mkRat  (221930581)  26369153040384000),  (mkRat  (0)  1),  (mkRat  (−4722116521)  1186611886817280000),  (mkRat  (0)  1),  (mkRat  (968383680827)  626531076239523840000),  (mkRat  (0)  1),  (mkRat  (−14717667114151)  28507163968898334720000),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(691)\;653996851200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-5461)\;653996851200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;62783697715200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;235438866432000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;26369153040384000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-4722116521)\;1186611886817280000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(968383680827)\;626531076239523840000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-14717667114151)\;28507163968898334720000),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (5461)  7847962214400),  (mkRat  (0)  1),  (mkRat  (−929569)  376702186291200),  (mkRat  (0)  1),  (mkRat  (3202291)  941755465728000),  (mkRat  (0)  1),  (mkRat  (−221930581)  79107459121152000),  (mkRat  (0)  1),  (mkRat  (4722116521)  2847868528361472000),  (mkRat  (0)  1),  (mkRat  (−968383680827)  1253062152479047680000),  (mkRat  (0)  1),  (mkRat  (14717667114151)  48869423946682859520000),  (mkRat  (0)  1),  (mkRat  (−2093660879252671)  20525158057606800998400000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(5461)\;7847962214400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;376702186291200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;941755465728000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;79107459121152000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(4722116521)\;2847868528361472000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-968383680827)\;1253062152479047680000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(14717667114151)\;48869423946682859520000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-2093660879252671)\;20525158057606800998400000)\text{]},  [(mkRat  (−5461)  204047017574400),  (mkRat  (0)  1),  (mkRat  (929569)  3264752281190400),  (mkRat  (0)  1),  (mkRat  (−3202291)  4897128421785600),  (mkRat  (0)  1),  (mkRat  (221930581)  293827705307136000),  (mkRat  (0)  1),  (mkRat  (−4722116521)  8227175748599808000),  (mkRat  (0)  1),  (mkRat  (968383680827)  2961783269495930880000),  (mkRat  (0)  1),  (mkRat  (−14717667114151)  97738847893365719040000),  (mkRat  (0)  1),  (mkRat  (2093660879252671)  35576940633185121730560000),  (mkRat  (0)  1)],\;\text{[}(\text{mkRat}\;(-5461)\;204047017574400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(929569)\;3264752281190400),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;4897128421785600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;293827705307136000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-4722116521)\;8227175748599808000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(968383680827)\;2961783269495930880000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-14717667114151)\;97738847893365719040000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(2093660879252671)\;35576940633185121730560000),\;(\text{mkRat}\;(0)\;1)\text{]},  [(mkRat  (0)  1),  (mkRat  (−929569)  45706531936665600),  (mkRat  (0)  1),  (mkRat  (3202291)  34279898952499200),  (mkRat  (0)  1),  (mkRat  (−221930581)  1371195958099968000),  (mkRat  (0)  1),  (mkRat  (4722116521)  28795115120099328000),  (mkRat  (0)  1),  (mkRat  (−968383680827)  8292993154588606464000),  (mkRat  (0)  1),  (mkRat  (14717667114151)  228057311751186677760000),  (mkRat  (0)  1),  (mkRat  (−2093660879252671)  71153881266370243461120000),  (mkRat  (0)  1),  (mkRat  (86125672563201181)  7471157532968875563417600000)],\;\text{[}(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-929569)\;45706531936665600),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(3202291)\;34279898952499200),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-221930581)\;1371195958099968000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(4722116521)\;28795115120099328000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-968383680827)\;8292993154588606464000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(14717667114151)\;228057311751186677760000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-2093660879252671)\;71153881266370243461120000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(86125672563201181)\;7471157532968875563417600000)\text{]},  [(mkRat  (929569)  1371195958099968000),  (mkRat  (0)  1),  (mkRat  (−3202291)  342798989524992000),  (mkRat  (0)  1),  (mkRat  (221930581)  8227175748599808000),  (mkRat  (0)  1),  (mkRat  (−4722116521)  123407636228997120000),  (mkRat  (0)  1),  (mkRat  (968383680827)  27643310515295354880000),  (mkRat  (0)  1),  (mkRat  (−14717667114151)  621974486594145484800000),  (mkRat  (0)  1),  (mkRat  (2093660879252671)  164201264460854407987200000),  (mkRat  (0)  1),  (mkRat  (−86125672563201181)  14942315065937751126835200000),  (mkRat  (0)  1)]]\;\text{[}(\text{mkRat}\;(929569)\;1371195958099968000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-3202291)\;342798989524992000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(221930581)\;8227175748599808000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-4722116521)\;123407636228997120000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(968383680827)\;27643310515295354880000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-14717667114151)\;621974486594145484800000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(2093660879252671)\;164201264460854407987200000),\;(\text{mkRat}\;(0)\;1),\;(\text{mkRat}\;(-86125672563201181)\;14942315065937751126835200000),\;(\text{mkRat}\;(0)\;1)\text{]}\text{]}
Lean source · 17 lines
def forsetiTable : List (List ℚ) := [
    [(mkRat (1) 2), (mkRat (1) 4), (mkRat (0) 1), (mkRat (-1) 48), (mkRat (0) 1), (mkRat (1) 480), (mkRat (0) 1), (mkRat (-17) 80640), (mkRat (0) 1), (mkRat (31) 1451520), (mkRat (0) 1), (mkRat (-691) 319334400), (mkRat (0) 1), (mkRat (5461) 24908083200), (mkRat (0) 1), (mkRat (-929569) 41845579776000)],
    [(mkRat (-1) 8), (mkRat (0) 1), (mkRat (1) 32), (mkRat (0) 1), (mkRat (-1) 192), (mkRat (0) 1), (mkRat (17) 23040), (mkRat (0) 1), (mkRat (-31) 322560), (mkRat (0) 1), (mkRat (691) 58060800), (mkRat (0) 1), (mkRat (-5461) 3832012800), (mkRat (0) 1), (mkRat (929569) 5579410636800), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (-1) 64), (mkRat (0) 1), (mkRat (1) 192), (mkRat (0) 1), (mkRat (-17) 15360), (mkRat (0) 1), (mkRat (31) 161280), (mkRat (0) 1), (mkRat (-691) 23224320), (mkRat (0) 1), (mkRat (5461) 1277337600), (mkRat (0) 1), (mkRat (-929569) 1594117324800), (mkRat (0) 1), (mkRat (3202291) 41845579776000)],
    [(mkRat (1) 384), (mkRat (0) 1), (mkRat (-1) 384), (mkRat (0) 1), (mkRat (17) 18432), (mkRat (0) 1), (mkRat (-31) 138240), (mkRat (0) 1), (mkRat (691) 15482880), (mkRat (0) 1), (mkRat (-5461) 696729600), (mkRat (0) 1), (mkRat (929569) 735746457600), (mkRat (0) 1), (mkRat (-3202291) 16738231910400), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (1) 1536), (mkRat (0) 1), (mkRat (-17) 36864), (mkRat (0) 1), (mkRat (31) 184320), (mkRat (0) 1), (mkRat (-691) 15482880), (mkRat (0) 1), (mkRat (5461) 557383680), (mkRat (0) 1), (mkRat (-929569) 490497638400), (mkRat (0) 1), (mkRat (3202291) 9564703948800), (mkRat (0) 1), (mkRat (-221930581) 4017175658496000)],
    [(mkRat (-1) 15360), (mkRat (0) 1), (mkRat (17) 122880), (mkRat (0) 1), (mkRat (-31) 368640), (mkRat (0) 1), (mkRat (691) 22118400), (mkRat (0) 1), (mkRat (-5461) 619315200), (mkRat (0) 1), (mkRat (929569) 445906944000), (mkRat (0) 1), (mkRat (-3202291) 7357464576000), (mkRat (0) 1), (mkRat (221930581) 2678117105664000), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (-17) 737280), (mkRat (0) 1), (mkRat (31) 1105920), (mkRat (0) 1), (mkRat (-691) 44236800), (mkRat (0) 1), (mkRat (5461) 928972800), (mkRat (0) 1), (mkRat (-929569) 535088332800), (mkRat (0) 1), (mkRat (3202291) 7357464576000), (mkRat (0) 1), (mkRat (-221930581) 2295528947712000), (mkRat (0) 1), (mkRat (4722116521) 241030539509760000)],
    [(mkRat (17) 10321920), (mkRat (0) 1), (mkRat (-31) 5160960), (mkRat (0) 1), (mkRat (691) 123863040), (mkRat (0) 1), (mkRat (-5461) 1857945600), (mkRat (0) 1), (mkRat (929569) 832359628800), (mkRat (0) 1), (mkRat (-3202291) 9364045824000), (mkRat (0) 1), (mkRat (221930581) 2472108097536000), (mkRat (0) 1), (mkRat (-4722116521) 224961836875776000), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (31) 41287680), (mkRat (0) 1), (mkRat (-691) 495452160), (mkRat (0) 1), (mkRat (5461) 4954521600), (mkRat (0) 1), (mkRat (-929569) 1664719257600), (mkRat (0) 1), (mkRat (3202291) 14982473318400), (mkRat (0) 1), (mkRat (-221930581) 3296144130048000), (mkRat (0) 1), (mkRat (4722116521) 257099242143744000), (mkRat (0) 1), (mkRat (-968383680827) 215963363400744960000)],
    [(mkRat (-31) 743178240), (mkRat (0) 1), (mkRat (691) 2972712960), (mkRat (0) 1), (mkRat (-5461) 17836277760), (mkRat (0) 1), (mkRat (929569) 4280706662400), (mkRat (0) 1), (mkRat (-3202291) 29964946636800), (mkRat (0) 1), (mkRat (221930581) 5393690394624000), (mkRat (0) 1), (mkRat (-4722116521) 355983566045184000), (mkRat (0) 1), (mkRat (968383680827) 259156036080893952000), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (-691) 29727129600), (mkRat (0) 1), (mkRat (5461) 89181388800), (mkRat (0) 1), (mkRat (-929569) 14269022208000), (mkRat (0) 1), (mkRat (3202291) 74912366592000), (mkRat (0) 1), (mkRat (-221930581) 10787380789248000), (mkRat (0) 1), (mkRat (4722116521) 593305943408640000), (mkRat (0) 1), (mkRat (-968383680827) 370222908686991360000), (mkRat (0) 1), (mkRat (14717667114151) 19436702706067046400000)],
    [(mkRat (691) 653996851200), (mkRat (0) 1), (mkRat (-5461) 653996851200), (mkRat (0) 1), (mkRat (929569) 62783697715200), (mkRat (0) 1), (mkRat (-3202291) 235438866432000), (mkRat (0) 1), (mkRat (221930581) 26369153040384000), (mkRat (0) 1), (mkRat (-4722116521) 1186611886817280000), (mkRat (0) 1), (mkRat (968383680827) 626531076239523840000), (mkRat (0) 1), (mkRat (-14717667114151) 28507163968898334720000), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (5461) 7847962214400), (mkRat (0) 1), (mkRat (-929569) 376702186291200), (mkRat (0) 1), (mkRat (3202291) 941755465728000), (mkRat (0) 1), (mkRat (-221930581) 79107459121152000), (mkRat (0) 1), (mkRat (4722116521) 2847868528361472000), (mkRat (0) 1), (mkRat (-968383680827) 1253062152479047680000), (mkRat (0) 1), (mkRat (14717667114151) 48869423946682859520000), (mkRat (0) 1), (mkRat (-2093660879252671) 20525158057606800998400000)],
    [(mkRat (-5461) 204047017574400), (mkRat (0) 1), (mkRat (929569) 3264752281190400), (mkRat (0) 1), (mkRat (-3202291) 4897128421785600), (mkRat (0) 1), (mkRat (221930581) 293827705307136000), (mkRat (0) 1), (mkRat (-4722116521) 8227175748599808000), (mkRat (0) 1), (mkRat (968383680827) 2961783269495930880000), (mkRat (0) 1), (mkRat (-14717667114151) 97738847893365719040000), (mkRat (0) 1), (mkRat (2093660879252671) 35576940633185121730560000), (mkRat (0) 1)],
    [(mkRat (0) 1), (mkRat (-929569) 45706531936665600), (mkRat (0) 1), (mkRat (3202291) 34279898952499200), (mkRat (0) 1), (mkRat (-221930581) 1371195958099968000), (mkRat (0) 1), (mkRat (4722116521) 28795115120099328000), (mkRat (0) 1), (mkRat (-968383680827) 8292993154588606464000), (mkRat (0) 1), (mkRat (14717667114151) 228057311751186677760000), (mkRat (0) 1), (mkRat (-2093660879252671) 71153881266370243461120000), (mkRat (0) 1), (mkRat (86125672563201181) 7471157532968875563417600000)],
    [(mkRat (929569) 1371195958099968000), (mkRat (0) 1), (mkRat (-3202291) 342798989524992000), (mkRat (0) 1), (mkRat (221930581) 8227175748599808000), (mkRat (0) 1), (mkRat (-4722116521) 123407636228997120000), (mkRat (0) 1), (mkRat (968383680827) 27643310515295354880000), (mkRat (0) 1), (mkRat (-14717667114151) 621974486594145484800000), (mkRat (0) 1), (mkRat (2093660879252671) 164201264460854407987200000), (mkRat (0) 1), (mkRat (-86125672563201181) 14942315065937751126835200000), (mkRat (0) 1)]]

Definition forsetiQ (k : Gimle.Asgard.Streams.Lowering.Degrees 2) : ℚ L677–677

Namespace Notebook.Burgers.Decided_front_band_refuted

(forsetiTable.getD  (k  0)  []).getD  (k  1)  0(\text{forsetiTable}.\text{getD}\;(\text{k}\;0)\;\text{[}\text{]}).\text{getD}\;(\text{k}\;1)\;0
Lean source · 1 line
def forsetiQ (k : Gimle.Asgard.Streams.Lowering.Degrees 2) : ℚ := (forsetiTable.getD (k 0) []).getD (k 1) 0

Definition forsetiPoint : Fin 2 → ℚ L679–679

Namespace Notebook.Burgers.Decided_front_band_refuted

![(mkRat  (1)  6),  (mkRat  (−1)  8)]!\text{[}(\text{mkRat}\;(1)\;6),\;(\text{mkRat}\;(-1)\;8)\text{]}
Lean source · 1 line
def forsetiPoint : Fin 2 → ℚ := ![(mkRat (1) 6), (mkRat (-1) 8)]

Definition forsetiRoot : Prop L681–688

Namespace Notebook.Burgers.Decided_front_band_refuted

∀  a  unused  v  :  Gimle.Asgard.Streams.Stream  2,\forall \;\text{a}\;\text{unused}\;\text{v}\;:\;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{Stream}\;2,  (Gimle.Asgard.Streams.Burgers.circuit  .ogf  (mkRat  (1)  2)).Rel\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{Burgers}.\text{circuit}\;.\text{ogf}\;(\text{mkRat}\;(1)\;2)).\text{Rel}  ![a,  Gimle.Asgard.Streams.ColeHopf.zeroSlice  (Gimle.Asgard.Streams.ColeHopf.front  (mkRat  (1)  2)  [((mkRat  (1)  1),  (mkRat  (0)  1)),  ((mkRat  (1)  1),  (mkRat  (−1)  1))]),  unused]  ![v,  a]  →\;!\text{[}\text{a},\;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{ColeHopf}.\text{zeroSlice}\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{ColeHopf}.\text{front}\;(\text{mkRat}\;(1)\;2)\;\text{[}((\text{mkRat}\;(1)\;1),\;(\text{mkRat}\;(0)\;1)),\;((\text{mkRat}\;(1)\;1),\;(\text{mkRat}\;(-1)\;1))\text{]}),\;\text{unused}\text{]}\;!\text{[}\text{v},\;\text{a}\text{]}\;\to   ∀  x,  forsetiBox.Mem  x  →\;\forall \;\text{x},\;\text{forsetiBox}.\text{Mem}\;\text{x}\;\to   HasSum  (Gimle.Asgard.Streams.seriesTerm  .ogf  a  x)\;\text{HasSum}\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{seriesTerm}\;.\text{ogf}\;\text{a}\;\text{x})  (Gimle.Asgard.Streams.analyticField  .ogf  a  x)  ∧\;(\text{Gimle}.\text{Asgard}.\text{Streams}.\text{analyticField}\;.\text{ogf}\;\text{a}\;\text{x})\;\land   Gimle.Asgard.Streams.analyticField  .ogf  a  x  ≤  (((mkRat  (27)  50)  :  Q)  :  R)\;\text{Gimle}.\text{Asgard}.\text{Streams}.\text{analyticField}\;.\text{ogf}\;\text{a}\;\text{x}\;\le \;(((\text{mkRat}\;(27)\;50)\;:\;\mathbb{Q} )\;:\;\mathbb{R} )
Lean source · 8 lines
def forsetiRoot : Prop :=
  ∀ a unused v : Gimle.Asgard.Streams.Stream 2,
      (Gimle.Asgard.Streams.Burgers.circuit .ogf (mkRat (1) 2)).Rel
        ![a, Gimle.Asgard.Streams.ColeHopf.zeroSlice (Gimle.Asgard.Streams.ColeHopf.front (mkRat (1) 2) [((mkRat (1) 1), (mkRat (0) 1)), ((mkRat (1) 1), (mkRat (-1) 1))]), unused] ![v, a] →
    ∀ x, forsetiBox.Mem x →
      HasSum (Gimle.Asgard.Streams.seriesTerm .ogf a x)
        (Gimle.Asgard.Streams.analyticField .ogf a x) ∧
      Gimle.Asgard.Streams.analyticField .ogf a x ≤ (((mkRat (27) 50) : ℚ) : ℝ)

Theorem front_band_refuted Contains sorryAs recorded L690–701

Namespace Notebook.Burgers.Decided_front_band_refuted

u is the stream the Burgers circuit at viscosity 1/2 rebuilds from the t = 0 slice of the Cole–Hopf front −2ν φ_x/φ of the potential Σ cᵢ·e^(aᵢx) given by the pairs (cᵢ, aᵢ), u_t its other output; its series converges at every point of the box, and its sum, the analytic field, stays within the band there. The stream decider refuted it. Goal (stream): stream burgers viscosity 1/2 interpretation analytic-field basis ogf potential exponentials [1, 0], [1, -1] field u over t in [-1/6, 1/6], x in [-1/8, 1/8] : u <= 27/50

Statement
have  circuit\text{have}\;\text{circuit}

Unfinished: the statement’s proof contains a placeholder.

Assumptions: propext, sorryAx, Classical.choice, Quot.sound

Lean source & proof · 12 lines
/-- u is the stream the Burgers circuit at viscosity 1/2 rebuilds from the t = 0 slice of the Cole–Hopf front −2ν φ_x/φ of the potential Σ cᵢ·e^(aᵢx) given by the pairs (cᵢ, aᵢ), u_t its other output; its series converges at every point of the box, and its sum, the analytic field, stays within the band there. The stream decider refuted it. Goal (stream): stream burgers viscosity 1/2 interpretation analytic-field basis ogf potential exponentials [1, 0], [1, -1] field u over t in [-1/6, 1/6], x in [-1/8, 1/8] : u <= 27/50 -/
theorem front_band_refuted :
    have circuit := Gimle.Asgard.Streams.Burgers.circuit .ogf (1/2)
    have slice := Gimle.Asgard.Streams.ColeHopf.zeroSlice
      (Gimle.Asgard.Streams.ColeHopf.front (1/2) [(1, 0), (1, -1)])
    ∀ u unused u_t : Gimle.Asgard.Streams.Stream 2,
      circuit.Rel ![u, slice, unused] ![u_t, u] →
      ∀ t x : ℝ, |t| ≤ 1/6 ∧ |x| ≤ 1/8 →
        HasSum (Gimle.Asgard.Streams.seriesTerm .ogf u ![t, x])
          (Gimle.Asgard.Streams.analyticField .ogf u ![t, x]) ∧
        Gimle.Asgard.Streams.analyticField .ogf u ![t, x] ≤ 27/50 := by
  sorry
end Decided_front_band_refuted
L703–703
end Notebook.Burgers
L706–706

Scope and unresolved requests

Formal uniqueness does not establish convergence. The x2x^2 divergence explanation and the affine closed form are not proved here. For the selected Cole–Hopf front, the series, truncation and field bounds are certified on the stated box only; the real PDE identity is not formalized here.

The tighter truncation request front_tighter remains unknown. The positive band request front_band_refuted is refuted by a checked witness, while front_not_below is a checked theorem of the negation. Neither a failed majorant search nor a numerical estimate is a proof of failure.