A 3-mode truncation of Navier–Stokes: the energy stays in its ball

import Mathlib

L1–1

import Gimle.Forseti.Syntax.Certificate

L2–2

import Gimle.Forseti.Examples.GalerkinNS.T3

L3–3

import Gimle.Forseti.Examples.GalerkinNS.T3Below12

L4–4

import Gimle.Forseti.Examples.GalerkinNS.T3Below9

L5–5

Two-dimensional incompressible flow on the periodic square, kept to three cosine modes of the vorticity, forced in one of them and damped in all; in simulation it settles to a steady state. It is the smallest member of a family of finite truncations of the Navier–Stokes equations; NS_K5.lean and NS_B2.lean are two more. The theorem is one theorem over the whole family (forseti-lean's GalerkinNS.Family): the energy identity and the certificate hold for every member, for every $C > f^2/(8\nu^2)$ the set $E \le C$ is invariant, and Lean checks that each compiled member is an instance. What this notebook adds is the concrete ball for this member's start, decided against its compiled circuit, and the storage and triad identities that explain why the family identity holds.

Read the argument in three stages: derive the family energy bound, add control of individual amplitudes through enstrophy, then sharpen the energy bound for this start with trapping sets that exclude the laminar equilibrium. The decided queries at the end include both refuted and unresolved bounds.

The equations

Two-dimensional incompressible flow on the periodic square, in vorticity form, keeps only the cosine modes $(1, 0)$ , $(1, 1)$ , $(2, 1)$ of the vorticity, with viscosity $\nu = \tfrac{1}{10}$ and a constant force $f = 1$ on the mode $(1, 1)$ . Writing $a_k$ for the amplitude of $\cos(k \cdot x)$ and $\lambda_k = |k|^2$ , projecting the equations onto the modes gives, for every mode $k$ (the projection is taken as read here; Lean checks everything from the coefficients on),

a_k' = -\nu \lambda_k a_k + f\,[k = (1,1)] + \sum_{\text{triads} \ni k} C_k\, a_P a_Q,

where $[k = (1,1)]$ is $1$ on the forced mode and $0$ otherwise, and a *triad* $\{k, P, Q\}$ is three modes whose wavevectors, each taken with a sign, sum to zero: $\pm k \pm P \pm Q = 0$ . Its three coefficients are exact rationals fixed by the geometry. This member has 1 triad. In full, writing $a_{10}$ for $a_{(1,0)}$ :

\begin{aligned} a_{10}' &= - \tfrac{1}{10} a_{10} - \tfrac{3}{20} a_{11} a_{21} \\ a_{11}' &= 1 - \tfrac{1}{5} a_{11} + \tfrac{2}{5} a_{10} a_{21} \\ a_{21}' &= - \tfrac{1}{2} a_{21} - \tfrac{1}{4} a_{10} a_{11} \end{aligned}

Proved. From the start where every amplitude is $1$ , a solution exists for all $t \ge 0$ , is unique, and its energy $E = \sum_k a_k^2/\lambda_k$ satisfies $0 \le E \le 13$ throughout, and in fact $E \le 9$ : below the laminar level $\tfrac{25}{2}$ , which no ball about the origin can pass, from a degree-four tube around the focus the start approaches in simulation, trapped under a decrease that holds on the set only (below9_contract); an ellipsoid with a centre and cross terms gave $12$ first (below12_contract; the section before the claims has both). Decided by the trajectory decider from named Lean contracts; the artifacts replay without the solver. Its enstrophy $Z = \sum_k a_k^2$ satisfies $0 \le Z \le 26$ throughout, by the same decider from a second named contract, so every amplitude satisfies $|a_k| \le 6$ (amplitude_bound).

Refuted. $E \le 1$ for all $t \ge 0$ : false at the start, where $E = \tfrac{17}{10}$ .

Unknown. $E \le 8$ for all $t \ge 0$ . A simulation from the start peaks near $7.0$ , so it is probably true; the contracts prove only $9$ , and the start does not refute it. The decider says so rather than guess. No reweighting of the modes about the origin can close it: the energy and the enstrophy are the only diagonal quadratics this member's triads conserve (only_two below), and every closed trapping set that contains the origin contains the laminar equilibrium, whose energy is $25/2$ — from the origin the flow runs along the forced mode alone and tends to that state. No ellipsoid was found at $E \le 10$ ; the tube that gives $9$ is of degree four, and at $8$ its certificate has no room. A search, not a proof that none exists.

Not claimed. Anything about the Navier–Stokes *equations*: this is a finite truncation, and nothing here says how it relates to the fluid, to other truncations, or to the limit. Nothing about the shape of the flow beyond the ball; the simulation is evidence, and no status reads it.

The system, compiled

The equations are declared once, in Asgard's language, and compiled to a circuit whose exact field Lean draws and reads:

namespace Notebook.NST3

L83–83

open Gimle.Asgard Gimle.Asgard.Dynamics Gimle.Forseti Gimle.Forseti.Trajectory
  Gimle.Forseti.GalerkinNS Gimle.Forseti.Examples.GalerkinNS.T3

L84–85

model diagram `Gimle.Forseti.Examples.GalerkinNS.T3.compiled` L87–87

Observations a10 a11 a21 E Z R

Evidence · not proofsimulate Gimle.Forseti.Examples.GalerkinNS.T3.compiled · forsetiNever runL88–88

Not run yet.

What a simulation shows

The run integrates the compiled field with RK4 in floating point. The energy starts at $\tfrac{17}{10}$ , peaks near $7.0$ , and then settles at about $4.2$ , a steady state. That is evidence about this run and nothing more: it does not enter any status.

Derive the reusable energy bound

Triad cancellation gives the energy identity; a sum-of-squares certificate then makes each energy ball with threshold above

25/2

invariant. The same argument applies to the finite family under its stated hypotheses. Sharper bounds for this particular start need the later local trapping argument.6 Kernel checked 6 As recorded

Cancel the triad energy transfers

Weighting each mode's stored energy by

1/\lambda_k

cancels the cubic transfers within each triad. This yields the energy identity of the compiled three-mode field.2 Kernel checked 2 As recorded

The invariant is built from two kinds of piece. Each mode $k$ is a *storage element*: its own squared amplitude obeys

(a_k^2)' = -2\nu\lambda_k a_k^2 + 2 f a_k\,[k = (1,1)] + \sum_{\text{triads} \ni k} 2 C_k\, a_k a_P a_Q.

Each triad is a *lossless three-port*: weight the three cubic flows it feeds into its modes by $1/\lambda_k$ and they sum to zero, so a triad only moves energy between its modes. Here is one triad of this member, checked as plain arithmetic:

Theorem `triad_lossless` Kernel checkedAs recorded L122–127

Namespace Notebook.NST3

The triad $\{a_{(1,0)}, a_{(1,1)}, a_{(2,1)}\}$ with weights $1/\lambda$ : its three energy flows cancel exactly, and so do its three enstrophy flows, with weights $1$ .

Statement

(1\;:\;\mathbb{R} )\;\cdot \;(-3/20)\;+\;(1/2\;:\;\mathbb{R} )\;\cdot \;(2/5)\;+\;(1/5\;:\;\mathbb{R} )\;\cdot \;(-1/4)\;=\;0\;\land

\;(-3/20\;:\;\mathbb{R} )\;+\;(2/5)\;+\;(-1/4)\;=\;0

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines

/-- The triad $\{a_{(1,0)}, a_{(1,1)}, a_{(2,1)}\}$ with weights $1/\lambda$: its three energy flows cancel exactly, and so do its
three enstrophy flows, with weights $1$. -/
theorem triad_lossless :
    (1 : ℝ) * (-3/20) + (1/2 : ℝ) * (2/5) + (1/5 : ℝ) * (-1/4) = 0 ∧
    (-3/20 : ℝ) + (2/5) + (-1/4) = 0 := by
  constructor <;> norm_num

Summing the storage identities with the weights $1/\lambda_k$ , every cubic term cancels triad by triad, and what remains is the energy identity

E' = -2\nu Z + f\, a_{(1,1)}, \qquad Z = \sum_k a_k^2,

which Lean checks for the compiled field by expanding both sides.

Theorem `energy_rate` Kernel checkedAs recorded L138–143

Namespace Notebook.NST3

The energy identity for the compiled field.

Statement

(\text{x}\;:\;\text{Point}\;3)\;:

\;(\sum \;\text{i},\;2\;\cdot \;(!\text{[}(1\;/\;1\;:\;\mathbb{R} ),\;(1\;/\;2\;:\;\mathbb{R} ),\;(1\;/\;5\;:\;\mathbb{R} )\text{]}\;:\;\text{Fin}\;3\;\to \;\mathbb{R} )\;\text{i}\;\cdot \;\text{x}\;\text{i}\;\cdot \;\text{Gimle}.\text{Forseti}.\text{Nonlinear}.\text{field}\;\text{compiled}\;\text{x}\;\text{i})\;=

\;-2\;\cdot \;(1\;/\;10\;:\;\mathbb{R} )\;\cdot \;(\text{x}\;0\;\cdot \;\text{x}\;0\;+\;\text{x}\;1\;\cdot \;\text{x}\;1\;+\;\text{x}\;2\;\cdot \;\text{x}\;2)\;+\;(1\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;1

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines

/-- The energy identity for the compiled field. -/
theorem energy_rate (x : Point 3) :
    (∑ i, 2 * (![(1 / 1 : ℝ), (1 / 2 : ℝ), (1 / 5 : ℝ)] : Fin 3 → ℝ) i * x i * Gimle.Forseti.Nonlinear.field compiled x i) =
      -2 * (1 / 10 : ℝ) * (x 0 * x 0 + x 1 * x 1 + x 2 * x 2) + (1 / 1 : ℝ) * x 1 := by
  rw [field_eq]
  exact energy_identity x

Turn the identity into a trapping ball

The certificate makes energy decrease above

25/2

. For a start inside

E \le 13

, it supplies a trapping ball; this bound applies to the finite ODE system, without a claim about the full PDE.2 Kernel checked 2 As recorded

Since $Z \ge E$ (every $\lambda_k \ge 1$ ) and the forcing acts on one mode, the energy identity gives a differential inequality with an explicit certificate:

2\nu\Big(\frac{f^2}{8\nu^2} - E\Big) - E' = \nu\Big(a_{(1,1)} - \frac{f}{2\nu}\Big)^2 + 2\nu \sum_{k \ne (1,1)} \Big(1 - \frac{1}{\lambda_k}\Big) a_k^2 \;\ge\; 0.

So $E$ decreases whenever it exceeds $f^2/(8\nu^2) = \tfrac{25}{2}$ , and any ball above that level traps the flow forever. The level is not an artefact of the proof: the laminar state, with only the forced mode excited at $a_{(1,1)} = f/(2\nu)$ , is an equilibrium with exactly that energy, and the trajectory from rest along the forced mode alone, $a_{(1,1)}(t) = \tfrac{f}{2\nu}(1 - e^{-2\nu t})$ with every other mode at zero (a single mode feeds no triad), climbs from $E = 0$ to it, so every smaller ball is left. The claim below uses $13$ , a whisker above.

Theorem `laminar_energy` Kernel checkedAs recorded L168–170

Namespace Notebook.NST3

The laminar equilibrium's energy, the least trappable level.

Statement

(1\;:\;\mathbb{R} )\;\text{\textasciicircum{}}\;2\;/\;(8\;\cdot \;(1/10)\;\text{\textasciicircum{}}\;2)\;=\;25/2

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 3 lines

/-- The laminar equilibrium's energy, the least trappable level. -/
theorem laminar_energy : (1 : ℝ) ^ 2 / (8 * (1/10) ^ 2) = 25/2 := by
  norm_num

Theorem `certificate_here` Kernel checkedAs recorded L172–176

Namespace Notebook.NST3

The certificate, checked for the compiled field: the gap is a sum of squares.

Statement

(\text{x}\;:\;\text{Point}\;3)\;:

\;\text{trapping}.\text{alpha}\;\cdot \;(\text{trapping}.\text{inner}\;-\;\text{trapping}.\text{energy}\;\text{x})\;-\;\text{trapping}.\text{rate}\;(\text{Gimle}.\text{Forseti}.\text{Nonlinear}.\text{field}\;\text{compiled})\;\text{x}\;=

\;(1\;/\;10\;:\;\mathbb{R} )\;\cdot \;(\text{x}\;1\;-\;5\;/\;1)\;\text{\textasciicircum{}}\;2\;+\;(4\;/\;25\;:\;\mathbb{R} )\;\cdot \;\text{x}\;2\;\text{\textasciicircum{}}\;2

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 5 lines

/-- The certificate, checked for the compiled field: the gap is a sum of squares. -/
theorem certificate_here (x : Point 3) :
    trapping.alpha * (trapping.inner - trapping.energy x) - trapping.rate (Gimle.Forseti.Nonlinear.field compiled) x =
      (1 / 10 : ℝ) * (x 1 - 5 / 1) ^ 2 + (4 / 25 : ℝ) * x 2 ^ 2 := by
  exact certificate x

Connect this system to the finite family

The compiled field is an instance of the family field. At this viscosity and forcing, any family member satisfying the mode hypotheses has a unique global trajectory inside each ball

E \le C

with

C>25/2

, provided its initial state is inside that ball.2 Kernel checked 2 As recorded

The three notebooks prove three members. The library also proves the family: for every finite list of nonzero modes, with the forcing on one of them that equals $(1,1)$ , every viscosity $\nu > 0$ and forcing $f$ , the energy identity and the certificate hold, and for every $C > f^2/(8\nu^2)$ the set $E \le C$ is invariant: from a start inside it a solution exists for all $t \ge$ any start time, is unique, and stays inside (GalerkinNS.Family). Such a list is a Galerkin truncation when its modes are distinct up to sign; that reading, the projection, is taken as read, and from the family field on everything is Lean. Two claims tie this member to it: Lean restates the library's check (field_eq_family) that its compiled field is the family field at its modes, and the family theorem at this viscosity and forcing.

Theorem `is_family_member` Kernel checkedAs recorded L199–203

Namespace Notebook.NST3

This member's compiled field is the family field at its modes (the library's field_eq_family, restated).

Statement

\text{Nonlinear}.\text{field}\;\text{compiled}\;=\;\text{Family}.\text{field}\;(1\;/\;10\;:\;\mathbb{R} )\;(1\;/\;1\;:\;\mathbb{R} )\;\text{modes}\;\text{forcedIndex}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 5 lines

/-- This member's compiled field is the family field at its modes (the library's
`field_eq_family`, restated). -/
theorem is_family_member :
    Nonlinear.field compiled = Family.field (1 / 10 : ℝ) (1 / 1 : ℝ) modes forcedIndex := by
  exact field_eq_family

Theorem `every_member` Kernel checkedAs recorded L205–218

Namespace Notebook.NST3

Every member. At $\nu = \tfrac{1}{10}$ , $f = 1$ : for any nonzero modes containing $(1,1)$ and any $C > \tfrac{25}{2}$ , from a start with $E \le C$ a solution exists for all $t \ge$ any start time, is unique, and keeps $E \le C$ ; the forcing sits on the mode $(1,1)$ .

Statement

\text{\{}\text{n}\;:\;\mathbb{N} \text{\}}\;(\text{k}\;:\;\text{Fin}\;\text{n}\;\to \;\text{Family}.\text{Wave})\;(\text{hk}\;:\;\forall \;\text{i},\;\text{k}\;\text{i}\;\ne \;0)\;(\text{forced}\;:\;\text{Fin}\;\text{n})

\;(\text{hf}\;:\;\text{k}\;\text{forced}\;=\;(1,\;1))\;(\text{C}\;:\;\mathbb{R} )\;(\text{hC}\;:\;(1\;:\;\mathbb{R} )\;\text{\textasciicircum{}}\;2\;/\;(8\;\cdot \;(1\;/\;10\;:\;\mathbb{R} )\;\text{\textasciicircum{}}\;2)\;<\;\text{C})

\;(\text{time}\;:\;\text{TimeDomain})\;(\text{x}_{0}\;:\;\text{Point}\;\text{n})\;(\text{initial}\;:\;\text{Family}.\text{energy}\;\text{k}\;\text{x}_{0}\;\le \;\text{C})\;:

\;(\exists \;\text{state},\;\text{Nonlinear}.\text{Solves}\;(\text{Family}.\text{field}\;(1\;/\;10\;:\;\mathbb{R} )\;1\;\text{k}\;\text{forced})\;\text{time}\;\text{x}_{0}\;\text{state})\;\land

\;(\forall \;\text{x}\;\text{y}\;:\;\text{Signal}\;\text{n},\;\text{Nonlinear}.\text{Solves}\;(\text{Family}.\text{field}\;(1\;/\;10\;:\;\mathbb{R} )\;1\;\text{k}\;\text{forced})\;\text{time}\;\text{x}_{0}\;\text{x}\;\to

\;\text{Nonlinear}.\text{Solves}\;(\text{Family}.\text{field}\;(1\;/\;10\;:\;\mathbb{R} )\;1\;\text{k}\;\text{forced})\;\text{time}\;\text{x}_{0}\;\text{y}\;\to

\;\text{Set}.\text{EqOn}\;\text{x}\;\text{y}\;\text{time}.\text{domain})\;\land

\;(\forall \;\text{state},\;\text{Nonlinear}.\text{Solves}\;(\text{Family}.\text{field}\;(1\;/\;10\;:\;\mathbb{R} )\;1\;\text{k}\;\text{forced})\;\text{time}\;\text{x}_{0}\;\text{state}\;\to

\;\forall \;\text{t}\;\in \;\text{time}.\text{domain},\;\text{Family}.\text{energy}\;\text{k}\;(\text{state}\;\text{t})\;\le \;\text{C})

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 14 lines

/-- **Every member.** At $\nu = \tfrac{1}{10}$, $f = 1$: for any nonzero modes
containing $(1,1)$ and any $C > \tfrac{25}{2}$, from a start with $E \le C$ a
solution exists for all $t \ge$ any start time, is unique, and keeps
$E \le C$; the forcing sits on the mode $(1,1)$. -/
theorem every_member {n : ℕ} (k : Fin n → Family.Wave) (hk : ∀ i, k i ≠ 0) (forced : Fin n)
    (hf : k forced = (1, 1)) (C : ℝ) (hC : (1 : ℝ) ^ 2 / (8 * (1 / 10 : ℝ) ^ 2) < C)
    (time : TimeDomain) (x₀ : Point n) (initial : Family.energy k x₀ ≤ C) :
    (∃ state, Nonlinear.Solves (Family.field (1 / 10 : ℝ) 1 k forced) time x₀ state) ∧
    (∀ x y : Signal n, Nonlinear.Solves (Family.field (1 / 10 : ℝ) 1 k forced) time x₀ x →
      Nonlinear.Solves (Family.field (1 / 10 : ℝ) 1 k forced) time x₀ y →
        Set.EqOn x y time.domain) ∧
    (∀ state, Nonlinear.Solves (Family.field (1 / 10 : ℝ) 1 k forced) time x₀ state →
      ∀ t ∈ time.domain, Family.energy k (state t) ≤ C) := by
  exact Family.trapped (1 / 10 : ℝ) 1 (by norm_num) k hk forced hf C hC time x₀ initial

Bound enstrophy and individual amplitudes

The enstrophy certificate gives

Z \le 26

for the stated start, hence

|a_k| \le 6

for every amplitude. Energy and enstrophy also span the diagonal quadratic invariants conserved by these triads; this is a statement about this finite system.5 Kernel checked 5 As recorded

Derive the enstrophy certificate

The triads conserve enstrophy as well as energy. Its dissipation identity supplies a second trapping certificate, whose bound controls each amplitude.4 Kernel checked 4 As recorded

The triads are lossless for the weights $1$ as well as for $1/\lambda_k$ (triad_lossless above states both for one triad; the member file does for every triad), so the enstrophy $Z = \sum_k a_k^2$ has an identity of its own, $Z' = -2\nu \sum_k \lambda_k a_k^2 + 2 f a_{(1,1)}$ , and a certificate of its own, $2\nu(f^2/(4\nu^2) - Z) - Z' = 2\nu \sum_{k \ne (1,1)} (\lambda_k - 1) a_k^2 + 2\nu (a_{(1,1)} - f/(2\nu))^2$ . The level $f^2/(4\nu^2) = 25$ is again the laminar state's, and every ball above it traps, for every member of the family (forseti-lean's Family.trapped_enstrophy; the level does not depend on the modes). What the enstrophy ball adds: it bounds every amplitude by $\sqrt{C}$ , where the energy ball bounds $a_k$ only by $\sqrt{\lambda_k C}$ ; here every amplitude stays within $\sqrt{26} < 6$ for all time, as amplitude_bound says of any state in the ball the decider establishes below.

Theorem `enstrophy_rate` Kernel checkedAs recorded L248–253

Namespace Notebook.NST3

The enstrophy identity for the compiled field.

Statement

(\text{x}\;:\;\text{Point}\;3)\;:

\;(\sum \;\text{i},\;2\;\cdot \;\text{x}\;\text{i}\;\cdot \;\text{Gimle}.\text{Forseti}.\text{Nonlinear}.\text{field}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{compiled}\;\text{x}\;\text{i})\;=

\;-2\;\cdot \;(1\;/\;10\;:\;\mathbb{R} )\;\cdot \;(\text{x}\;0\;\cdot \;\text{x}\;0\;+\;(2\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;1\;\cdot \;\text{x}\;1\;+\;(5\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;2\;\cdot \;\text{x}\;2)\;+\;2\;\cdot \;(1\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;1

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines

/-- The enstrophy identity for the compiled field. -/
theorem enstrophy_rate (x : Point 3) :
    (∑ i, 2 * x i * Gimle.Forseti.Nonlinear.field Gimle.Forseti.Examples.GalerkinNS.T3.compiled x i) =
      -2 * (1 / 10 : ℝ) * (x 0 * x 0 + (2 / 1 : ℝ) * x 1 * x 1 + (5 / 1 : ℝ) * x 2 * x 2) + 2 * (1 / 1 : ℝ) * x 1 := by
  rw [Gimle.Forseti.Examples.GalerkinNS.T3.field_eq]
  exact Gimle.Forseti.Examples.GalerkinNS.T3.enstrophy_identity x

Theorem `laminar_enstrophy` Kernel checkedAs recorded L255–257

Namespace Notebook.NST3

The laminar state's enstrophy, the least trappable level.

Statement

(1\;/\;1\;:\;\mathbb{R} )\;\text{\textasciicircum{}}\;2\;/\;(4\;\cdot \;(1\;/\;10)\;\text{\textasciicircum{}}\;2)\;=\;25\;/\;1

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 3 lines

/-- The laminar state's enstrophy, the least trappable level. -/
theorem laminar_enstrophy : (1 / 1 : ℝ) ^ 2 / (4 * (1 / 10) ^ 2) = 25 / 1 := by
  norm_num

Theorem `enstrophy_certificate_here` Kernel checkedAs recorded L259–263

Namespace Notebook.NST3

The enstrophy certificate, checked for the compiled field: the gap is a sum of squares.

Statement

(\text{x}\;:\;\text{Point}\;3)\;:

\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{trappingZ}.\text{alpha}\;\cdot \;(\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{trappingZ}.\text{inner}\;-\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{trappingZ}.\text{energy}\;\text{x})\;-\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{trappingZ}.\text{rate}\;(\text{Gimle}.\text{Forseti}.\text{Nonlinear}.\text{field}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{compiled})\;\text{x}\;=

\;(2\;\cdot \;(1\;/\;10)\;:\;\mathbb{R} )\;\cdot \;(\text{x}\;1\;-\;5\;/\;1)\;\text{\textasciicircum{}}\;2\;+\;(4\;/\;5\;:\;\mathbb{R} )\;\cdot \;\text{x}\;2\;\text{\textasciicircum{}}\;2

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 5 lines

/-- The enstrophy certificate, checked for the compiled field: the gap is a sum of squares. -/
theorem enstrophy_certificate_here (x : Point 3) :
    Gimle.Forseti.Examples.GalerkinNS.T3.trappingZ.alpha * (Gimle.Forseti.Examples.GalerkinNS.T3.trappingZ.inner - Gimle.Forseti.Examples.GalerkinNS.T3.trappingZ.energy x) - Gimle.Forseti.Examples.GalerkinNS.T3.trappingZ.rate (Gimle.Forseti.Nonlinear.field Gimle.Forseti.Examples.GalerkinNS.T3.compiled) x =
      (2 * (1 / 10) : ℝ) * (x 1 - 5 / 1) ^ 2 + (4 / 5 : ℝ) * x 2 ^ 2 := by
  exact Gimle.Forseti.Examples.GalerkinNS.T3.certificateZ x

Theorem `amplitude_bound` Kernel checkedAs recorded L265–271

Namespace Notebook.NST3

In the enstrophy ball every amplitude is bounded: $a_k^2 \le Z \le 26$ .

Statement

(\text{x}\;:\;\text{Point}\;3)\;(\text{h}\;:\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{enstrophy}\;\text{x}\;\le \;26)\;(\text{i}\;:\;\text{Fin}\;3)\;:

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 7 lines

/-- In the enstrophy ball every amplitude is bounded: $a_k^2 \le Z \le 26$. -/
theorem amplitude_bound (x : Point 3) (h : Gimle.Forseti.Examples.GalerkinNS.T3.enstrophy x ≤ 26) (i : Fin 3) :
    |x i| ≤ 6 := by
  rw [Gimle.Forseti.Examples.GalerkinNS.T3.enstrophy_eq_trappingZ, Gimle.Forseti.Examples.GalerkinNS.T3.enstrophy_eq_family] at h
  have := Gimle.Forseti.GalerkinNS.Family.mode_sq_le_enstrophy x i
  rw [abs_le]
  constructor <;> nlinarith

Explain the limit of diagonal reweighting

Every diagonal weighting conserved by the triads is a combination of the energy and enstrophy weights. A tighter bound for this start needs a different trapping set; this does not exclude other kinds of invariants.1 Kernel checked 1 As recorded

And these two are all there is. A weighting $w$ of the modes for which every triad is lossless — one linear equation per triad — is a combination of $1/\lambda$ and $1$ (only_two, a linear_combination of the triad equations with multipliers the generator computed exactly). No reweighting of the modes about the origin traps tighter than the energy and the enstrophy; a trapping set for the energy bound left unknown above would have to be centred away from the laminar line (the design study says how far that has been tried). The lens $\{E \le C_E\} \cap \{Z \le C_Z\}$ is the region both balls give together.

Theorem `only_two` Kernel checkedAs recorded L290–297

Namespace Notebook.NST3

Only two diagonal invariants. Every weighting for which this member's triads are lossless is a combination of $1/\lambda$ and $1$ .

Statement

(\text{w}\;:\;\text{Fin}\;3\;\to \;\mathbb{R} )

\;(\text{h0}\;:\;\text{w}\;0\;\cdot \;(-3\;/\;20)\;+\;\text{w}\;1\;\cdot \;(2\;/\;5)\;+\;\text{w}\;2\;\cdot \;(-1\;/\;4)\;=\;0)\;:

\;\exists \;\alpha \;\beta \;:\;\mathbb{R} ,\;\text{w}\;0\;=\;\alpha \;\cdot \;(1\;/\;1)\;+\;\beta \;\land

\;\text{w}\;1\;=\;\alpha \;\cdot \;(1\;/\;2)\;+\;\beta \;\land

\;\text{w}\;2\;=\;\alpha \;\cdot \;(1\;/\;5)\;+\;\beta

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 8 lines

/-- **Only two diagonal invariants.** Every weighting for which this member's
triads are lossless is a combination of $1/\lambda$ and $1$. -/
theorem only_two (w : Fin 3 → ℝ)
    (h0 : w 0 * (-3 / 20) + w 1 * (2 / 5) + w 2 * (-1 / 4) = 0) :
    ∃ α β : ℝ, w 0 = α * (1 / 1) + β ∧
      w 1 = α * (1 / 2) + β ∧
      w 2 = α * (1 / 5) + β := by
  exact Gimle.Forseti.Examples.GalerkinNS.T3.only_two_diagonal w h0

Sharpen the bound for this initial state

The ellipsoid gives

E \le 12

and a quartic tube gives

E \le 9

for the start

(1,1,1)

. They exclude the laminar equilibrium by requiring decrease only on the trapping set. The requested bound

E \le 8

remains unknown.5 Kernel checked 5 As recorded

Every set the global decrease can trap contains every equilibrium: at an equilibrium the rate is zero, so $V' \le \alpha(C' - V)$ forces $V \le C'$ there. The laminar state $(0, 5, 0)$ is an equilibrium (laminar_equilibrium), so no such set, whatever its weights or centre, has $\max E$ below $\tfrac{25}{2}$ . A set that excludes it needs a decrease that holds *on the set only*: at a first contact with the boundary the rate is still $\le \alpha(C' - C) < 0$ , so the set is never left (the library's LocalTrapping, by a barrier lemma).

This member has three equilibria: the laminar saddle and a mirror pair of stable foci at $E \approx 4.22$ (an exact computation in the design study, not a theorem); in simulation the start settles on one of them.

Trap the trajectory in an ellipsoid

The ellipsoid contains the start, excludes the laminar point, and lies inside

E \le 12

. Its local decrease certificate supplies the trapping argument in the imported library.3 Kernel checked 3 As recorded

A search (the design study's spike, task 196) found an ellipsoid $V = (x - c)^\top P (x - c) \le 1$ with cross terms and a centre near that focus that contains the start, excludes the laminar point ( $V \approx 2.54$ there), and lies inside $E \le 12$ ; on it the decrease holds by an explicit degree-four sum of squares with a multiplier $\sigma \ge 0$ : $\alpha(C' - V) - V' + \sigma(V - 1)$ is a sum of squares everywhere, so where $V \le 1$ the decrease follows. All of it is rational and every identity is ring; the library states the contract below12_contract, which the decider cited for $E \le 12$ until the tube below superseded it; its own theorems are restated here.

Theorem `laminar_is_equilibrium` Kernel checkedAs recorded L336–338

Namespace Notebook.NST3

The laminar state is an equilibrium of the compiled field, restated.

Statement

\text{field}\;!\text{[}0,\;5,\;0\text{]}\;=\;0

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 3 lines

/-- The laminar state is an equilibrium of the compiled field, restated. -/
theorem laminar_is_equilibrium : field ![0, 5, 0] = 0 := by
  exact laminar_equilibrium

Theorem `ellipsoid_excludes_laminar` Kernel checkedAs recorded L340–343

Namespace Notebook.NST3

The ellipsoid excludes it and holds the start, restated.

Statement

1\;<\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{V}\;!\text{[}0,\;5,\;0\text{]}\;\land

\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{V}\;!\text{[}1,\;1,\;1\text{]}\;<\;1

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines

/-- The ellipsoid excludes it and holds the start, restated. -/
theorem ellipsoid_excludes_laminar : 1 < Gimle.Forseti.Examples.GalerkinNS.T3.V ![0, 5, 0] ∧
    Gimle.Forseti.Examples.GalerkinNS.T3.V ![1, 1, 1] < 1 := by
  exact ⟨laminar_outside, start_inside⟩

Theorem `ellipsoid_below_twelve` Kernel checkedAs recorded L345–348

Namespace Notebook.NST3

Inside the ellipsoid the energy is at most 12, restated.

Statement

(\text{x}\;:\;\text{Point}\;3)\;(\text{hx}\;:\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{V}\;\text{x}\;\le \;1)\;:

\;\text{energy}\;\text{x}\;\le \;12

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines

/-- Inside the ellipsoid the energy is at most `12`, restated. -/
theorem ellipsoid_below_twelve (x : Point 3) (hx : Gimle.Forseti.Examples.GalerkinNS.T3.V x ≤ 1) :
    energy x ≤ 12 := by
  exact contained x hx

Tighten the bound with a quartic tube

The tube contains the same start and lies inside

E \le 9

. Its decrease certificate holds on the set; numerical evidence suggesting

E \le 8

does not certify that stronger bound.2 Kernel checked 2 As recorded

Tighter than the ellipsoid: with the whole orbit from the start held inside, the same search over a degree-four $V$ finds a thin tube around the focus, inside $E \le 9$ (numerically $E \le 7.985$ on it; at $8$ the containment certificate has no room), with the decrease on the set by a degree-six sum of squares. The library takes a polynomial $V$ (PolynomialTrapping) and states below9_contract; the decider cites it below (for $13$ , $10$ and $12$ alike).

Theorem `tube_excludes_laminar` Kernel checkedAs recorded L365–368

Namespace Notebook.NST3

The tube excludes the laminar point and holds the start, restated.

Statement

1\;<\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{tubeV}\;!\text{[}0,\;5,\;0\text{]}\;\land

\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{tubeV}\;!\text{[}1,\;1,\;1\text{]}\;<\;1

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines

/-- The tube excludes the laminar point and holds the start, restated. -/
theorem tube_excludes_laminar : 1 < Gimle.Forseti.Examples.GalerkinNS.T3.tubeV ![0, 5, 0] ∧
    Gimle.Forseti.Examples.GalerkinNS.T3.tubeV ![1, 1, 1] < 1 := by
  exact ⟨tube_laminar_outside, tube_start_inside⟩

Theorem `tube_below_nine` Kernel checkedAs recorded L370–373

Namespace Notebook.NST3

Inside the tube the energy is at most 9, restated.

Statement

(\text{x}\;:\;\text{Point}\;3)\;(\text{hx}\;:\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{tubeV}\;\text{x}\;\le \;1)\;:

\;\text{energy}\;\text{x}\;\le \;9

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines

/-- Inside the tube the energy is at most `9`, restated. -/
theorem tube_below_nine (x : Point 3) (hx : Gimle.Forseti.Examples.GalerkinNS.T3.tubeV x ≤ 1) :
    energy x ≤ 9 := by
  exact tube_contained x hx

Inspect the decided trajectory contracts

The queries certify energy bounds

13

10

and

12

, and enstrophy bound

26

, for the stated start. The energy bound

1

is refuted; energy bound

8

and enstrophy bound

20

remain unknown. Unknown requests may have no claim card, so the claim counts do not list every unresolved query.24 Kernel checked 25 As recorded 1 Contains sorry

Existence for all time, uniqueness and the sets come from the library's trapping theorems: the ball from the general one that traps the Lorenz system (Lorenz.lean), the ellipsoid and the tube from its variants with the decrease on the set, each by clamping the field to a box, solving on every $[0, n]$ , gluing, and fencing at the boundary. Every claim below is decided against the compiled circuit.

Inspect the energy bound of thirteen

The query certifies existence, uniqueness and

0 \le E \le 13

for all time from

(1,1,1)

. The current decision uses the stronger tube contract.5 Kernel checked 5 As recorded

Decisionin_ball · trajectory · forsetiNever runL399–399

trajectory ns-t3 from (1, 1, 1) at 0 observe E always : E >= 0 and E <= 13

Not run yet.

namespace DecidedShared_5a37f797df5f

L401–401

Definition `forsetiTime` `: Gimle.Asgard.Dynamics.TimeDomain` L403–404

Namespace Notebook.NST3.DecidedShared_5a37f797df5f

\langle \texttt{"time"},\;(((\text{mkRat}\;(0)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} )\rangle

Lean source · 2 lines

def forsetiTime : Gimle.Asgard.Dynamics.TimeDomain :=
  ⟨"time", (((mkRat (0) 1) : ℚ) : ℝ)⟩

Definition `forsetiInitial` `: Gimle.Asgard.Point 3` L406–407

Namespace Notebook.NST3.DecidedShared_5a37f797df5f

!\text{[}(((\text{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} ),\;(((\text{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} ),\;(((\text{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} )\text{]}

Lean source · 2 lines

def forsetiInitial : Gimle.Asgard.Point 3 :=
  ![(((mkRat (1) 1) : ℚ) : ℝ), (((mkRat (1) 1) : ℚ) : ℝ), (((mkRat (1) 1) : ℚ) : ℝ)]

Definition `forsetiObservation` `: Fin 6` L409–409

Namespace Notebook.NST3.DecidedShared_5a37f797df5f

\langle 3,\;\text{by}\;\text{decide}\rangle

Lean source · 1 line

def forsetiObservation : Fin 6 := ⟨3, by decide⟩

Definition `forsetiIdentities` `: Prop` L411–415

Namespace Notebook.NST3.DecidedShared_5a37f797df5f

\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{evolution}.\text{states}.\text{map}\;(\text{·}.\text{initialId})\;=\;\text{[}\texttt{"initial-a10"},\;\texttt{"initial-a11"},\;\texttt{"initial-a21"}\text{]}\;\land

\;(\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{body}.\text{observations}.\text{get}\;\text{forsetiObservation}).\text{port}.\text{id}\;=

\;\texttt{"obs-e"}\;\land

\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{evolution}.\text{axis}.\text{id}\;=\;\texttt{"time"}

Lean source · 5 lines

def forsetiIdentities : Prop :=
  Gimle.Forseti.Examples.GalerkinNS.T3.evolution.states.map (·.initialId) = ["initial-a10", "initial-a11", "initial-a21"] ∧
  (Gimle.Forseti.Examples.GalerkinNS.T3.body.observations.get forsetiObservation).port.id =
    "obs-e" ∧
  Gimle.Forseti.Examples.GalerkinNS.T3.evolution.axis.id = "time"

end DecidedShared_5a37f797df5f

L417–417

namespace Decided_in_ball

L419–419

open DecidedShared_5a37f797df5f

L421–421

Example `example (line 423)` Kernel checkedAs recorded L423–423

Namespace Notebook.NST3.Decided_in_ball

Checked statement, as this project’s notation prints it

\text{forsetiTime}\;=\;\text{forsetiTime}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiTime Notebook.NST3.DecidedShared_5a37f797df5f.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiTime = @DecidedShared_5a37f797df5f.forsetiTime := rfl

Example `example (line 424)` Kernel checkedAs recorded L424–424

Namespace Notebook.NST3.Decided_in_ball

Checked statement, as this project’s notation prints it

\text{forsetiInitial}\;=\;\text{forsetiInitial}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiInitial Notebook.NST3.DecidedShared_5a37f797df5f.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiInitial = @DecidedShared_5a37f797df5f.forsetiInitial := rfl

Example `example (line 425)` Kernel checkedAs recorded L425–425

Namespace Notebook.NST3.Decided_in_ball

Checked statement, as this project’s notation prints it

\text{forsetiObservation}\;=\;\text{forsetiObservation}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiObservation
  Notebook.NST3.DecidedShared_5a37f797df5f.forsetiObservation

Assumptions: none

Lean source & proof · 1 line

example : @forsetiObservation = @DecidedShared_5a37f797df5f.forsetiObservation := rfl

Example `example (line 426)` Kernel checkedAs recorded L426–426

Namespace Notebook.NST3.Decided_in_ball

Checked statement, as this project’s notation prints it

\text{forsetiIdentities}\;=\;\text{forsetiIdentities}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiIdentities Notebook.NST3.DecidedShared_5a37f797df5f.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiIdentities = @DecidedShared_5a37f797df5f.forsetiIdentities := rfl

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L428–429

Namespace Notebook.NST3.Decided_in_ball

(.\text{and}\;(.\text{atom}\;.\text{ge}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle ))\;(.\text{atom}\;.\text{le}\;(.\text{add}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )\;(.\text{neg}\;(.\text{constant}\;(\text{mkRat}\;(13)\;1))))))

Lean source · 2 lines

def forsetiPost : Gimle.Forseti.Syntax.Formula 1 :=
  (.and (.atom .ge (.var ⟨0, by decide⟩)) (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (13) 1))))))

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L431–434

Namespace Notebook.NST3.Decided_in_ball

\langle \langle \text{[}\texttt{"E"}\text{]},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide}\rangle ,

\;(.\text{and}\;(.\text{atom}\;.\text{le}\;(.\text{neg}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )))\;(.\text{atom}\;.\text{le}\;(.\text{add}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )\;(.\text{neg}\;(.\text{constant}\;(\text{mkRat}\;(9)\;1)))))),

\;\text{forsetiPost}\rangle

Lean source · 4 lines

def forsetiLeaf : Gimle.Forseti.Syntax.Goal :=
  ⟨⟨["E"], by decide, by decide, by decide⟩,
    (.and (.atom .le (.neg (.var ⟨0, by decide⟩))) (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (9) 1)))))),
    forsetiPost⟩

Definition `forsetiContract` `: Prop` L436–441

Namespace Notebook.NST3.Decided_in_ball

\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{observed}\;\text{forsetiTime}

\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Initialized}\;\text{forsetiTime}\;(\text{fun}\;\text{\_}\;=>\;\text{True})

\;(\text{·}\;=\;\text{forsetiInitial}))

\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Always}\;\text{forsetiTime}

\;\text{fun}\;\text{o}\;=>\;\text{forsetiPost}.\text{holds}\;(\text{fun}\;\text{\_}\;=>\;\text{o}\;\text{forsetiObservation}))

Lean source · 6 lines

def forsetiContract : Prop :=
  Gimle.Forseti.Trajectory.Contract Gimle.Forseti.Examples.GalerkinNS.T3.observed forsetiTime
    (Gimle.Forseti.Trajectory.Initialized forsetiTime (fun _ => True)
      (· = forsetiInitial))
    (Gimle.Forseti.Trajectory.Always forsetiTime
      fun o => forsetiPost.holds (fun _ => o forsetiObservation))

Definition `forsetiRoot` `: Prop` L443–443

Namespace Notebook.NST3.Decided_in_ball

\text{forsetiIdentities}\;\land \;\text{forsetiContract}

Lean source · 1 line

def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem `in_ball` Kernel checkedAs recorded L445–486

Namespace Notebook.NST3.Decided_in_ball

E is output 3 of the compiled circuit, the port obs-e; the input's initial wires (initial-a10, initial-a11, initial-a21) start at (1, 1, 1) at time = 0. The trajectory decider proved it. Goal (trajectory): trajectory ns-t3 interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-e as E always : E >= 0 and E <= 13

Statement

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

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 42 lines

/-- E is output 3 of the compiled circuit, the port obs-e; the input's initial wires (initial-a10, initial-a11, initial-a21) start at (1, 1, 1) at time = 0. The trajectory decider proved it. Goal (trajectory): trajectory ns-t3 interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-e as E always : E >= 0 and E <= 13 -/
theorem in_ball :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.T3.observed
    have time : Gimle.Asgard.Dynamics.TimeDomain := ⟨"time", 0⟩
    ∀ u : Gimle.Asgard.Dynamics.Signal (0 + 3),
      Gimle.Asgard.Dynamics.signalRight u 0 = ![1, 1, 1] →
      (∃ y : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y) ∧
      (∀ y y' : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y → circuit.Rel time u y' →
        ∀ t ≥ 0, y t = y' t) ∧
      (∀ y : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y →
        ∀ t ≥ 0, have E := y t 3; E ≥ 0 ∧ E ≤ 13) := by
  have root : forsetiRoot := by
    unfold forsetiRoot forsetiIdentities forsetiContract
    refine ⟨⟨by decide, by decide, by decide⟩, ?_⟩
    have time : forsetiTime = Gimle.Forseti.Examples.GalerkinNS.T3.evolution.time := by simp [forsetiTime, Gimle.Asgard.Model.Evolution.time, Gimle.Forseti.Examples.GalerkinNS.T3.evolution] <;> norm_num [Rat.mkRat_eq_div]
    have init : forsetiInitial = Gimle.Forseti.Examples.GalerkinNS.T3.compiled.initial := by rw [Gimle.Forseti.Examples.GalerkinNS.T3.initial_eq]; funext i; fin_cases i <;> norm_num [forsetiInitial, Rat.mkRat_eq_div]
    have obs : forsetiObservation = Gimle.Forseti.Examples.GalerkinNS.T3.energyIndex := rfl
    rw [time, init, obs]
    refine Gimle.Forseti.Trajectory.Contract.consequence Gimle.Forseti.Examples.GalerkinNS.T3.below9_contract (fun _ admitted => admitted) ?_
    intro o band t within
    have leaf := Gimle.Forseti.Syntax.EntailmentCertificate.sound forsetiLeaf ⟨[⟨⟨[]⟩, [⟨[((mkRat (1) 1), (.constant (mkRat (1) 1)))]⟩, ⟨[]⟩]⟩, ⟨⟨[((mkRat (4) 1), (.constant (mkRat (1) 1)))]⟩, [⟨[]⟩, ⟨[((mkRat (1) 1), (.constant (mkRat (1) 1)))]⟩]⟩]⟩ (by decide +kernel)
    apply leaf
    simp only [forsetiLeaf, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval]
    obtain ⟨low, high⟩ := band t within
    refine ⟨?_, ?_⟩ <;> norm_num [Rat.mkRat_eq_div] <;> linarith
  have forsetiCast0 : (((mkRat (13) 1) : ℚ) : ℝ) = 13 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast1 : (((mkRat (0) 1) : ℚ) : ℝ) = 0 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast2 : (((mkRat (1) 1) : ℚ) : ℝ) = 1 := by norm_num [Rat.mkRat_eq_div]
  refine (fun (bridge : _ ↔ forsetiContract) => bridge.mpr (show forsetiIdentities ∧ forsetiContract from root).2) ?_
  constructor
  · intro claim
    unfold forsetiContract
    set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc] at claim
    refine ⟨?_, ?_, ?_⟩ <;> set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc]
    · exact fun u start => (claim u start).1
    · exact fun u start => (claim u start).2.1
    · exact fun u start => (claim u start).2.2
  · intro lane
    unfold forsetiContract at lane
    obtain ⟨realizable, unique, holds⟩ := lane
    set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc] at realizable unique holds ⊢
    exact fun u start => ⟨realizable u start, unique u start, holds u start⟩

Inspect the refuted energy bound of one

The start already has

E=17/10>1

. A checked refutation is recorded beside the notebook; the false positive claim below deliberately uses sorry.4 Kernel checked 5 As recorded 1 Contains sorry

end Decided_in_ball

L495–495

Decisionbelow_one · trajectory · forsetiNever runL498–498

trajectory ns-t3 from (1, 1, 1) at 0 observe E always : E <= 1

Not run yet.

namespace Decided_below_one

L500–500

open DecidedShared_5a37f797df5f

L502–502

Example `example (line 504)` Kernel checkedAs recorded L504–504

Namespace Notebook.NST3.Decided_below_one

Checked statement, as this project’s notation prints it

\text{forsetiTime}\;=\;\text{forsetiTime}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiTime Notebook.NST3.DecidedShared_5a37f797df5f.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiTime = @DecidedShared_5a37f797df5f.forsetiTime := rfl

Example `example (line 505)` Kernel checkedAs recorded L505–505

Namespace Notebook.NST3.Decided_below_one

Checked statement, as this project’s notation prints it

\text{forsetiInitial}\;=\;\text{forsetiInitial}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiInitial Notebook.NST3.DecidedShared_5a37f797df5f.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiInitial = @DecidedShared_5a37f797df5f.forsetiInitial := rfl

Example `example (line 506)` Kernel checkedAs recorded L506–506

Namespace Notebook.NST3.Decided_below_one

Checked statement, as this project’s notation prints it

\text{forsetiObservation}\;=\;\text{forsetiObservation}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiObservation
  Notebook.NST3.DecidedShared_5a37f797df5f.forsetiObservation

Assumptions: none

Lean source & proof · 1 line

example : @forsetiObservation = @DecidedShared_5a37f797df5f.forsetiObservation := rfl

Example `example (line 507)` Kernel checkedAs recorded L507–507

Namespace Notebook.NST3.Decided_below_one

Checked statement, as this project’s notation prints it

\text{forsetiIdentities}\;=\;\text{forsetiIdentities}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiIdentities Notebook.NST3.DecidedShared_5a37f797df5f.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiIdentities = @DecidedShared_5a37f797df5f.forsetiIdentities := rfl

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L509–510

Namespace Notebook.NST3.Decided_below_one

(.\text{atom}\;.\text{le}\;(.\text{add}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )\;(.\text{neg}\;(.\text{constant}\;(\text{mkRat}\;(1)\;1)))))

Lean source · 2 lines

def forsetiPost : Gimle.Forseti.Syntax.Formula 1 :=
  (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (1) 1)))))

Definition `forsetiContract` `: Prop` L512–517

Namespace Notebook.NST3.Decided_below_one

\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{observed}\;\text{forsetiTime}

\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Initialized}\;\text{forsetiTime}\;(\text{fun}\;\text{\_}\;=>\;\text{True})

\;(\text{·}\;=\;\text{forsetiInitial}))

\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Always}\;\text{forsetiTime}

\;\text{fun}\;\text{o}\;=>\;\text{forsetiPost}.\text{holds}\;(\text{fun}\;\text{\_}\;=>\;\text{o}\;\text{forsetiObservation}))

Lean source · 6 lines

def forsetiContract : Prop :=
  Gimle.Forseti.Trajectory.Contract Gimle.Forseti.Examples.GalerkinNS.T3.observed forsetiTime
    (Gimle.Forseti.Trajectory.Initialized forsetiTime (fun _ => True)
      (· = forsetiInitial))
    (Gimle.Forseti.Trajectory.Always forsetiTime
      fun o => forsetiPost.holds (fun _ => o forsetiObservation))

Definition `forsetiRoot` `: Prop` L519–519

Namespace Notebook.NST3.Decided_below_one

\text{forsetiIdentities}\;\land \;\text{forsetiContract}

Lean source · 1 line

def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem `below_one` Contains sorryAs recorded L521–532

Namespace Notebook.NST3.Decided_below_one

E is output 3 of the compiled circuit, the port obs-e; the input's initial wires (initial-a10, initial-a11, initial-a21) start at (1, 1, 1) at time = 0. The trajectory decider refuted it. Goal (trajectory): trajectory ns-t3 interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-e as E always : E <= 1

Statement

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

Unfinished: the statement’s proof contains a placeholder.

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

Lean source & proof · 12 lines

/-- E is output 3 of the compiled circuit, the port obs-e; the input's initial wires (initial-a10, initial-a11, initial-a21) start at (1, 1, 1) at time = 0. The trajectory decider refuted it. Goal (trajectory): trajectory ns-t3 interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-e as E always : E <= 1 -/
theorem below_one :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.T3.observed
    have time : Gimle.Asgard.Dynamics.TimeDomain := ⟨"time", 0⟩
    ∀ u : Gimle.Asgard.Dynamics.Signal (0 + 3),
      Gimle.Asgard.Dynamics.signalRight u 0 = ![1, 1, 1] →
      (∃ y : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y) ∧
      (∀ y y' : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y → circuit.Rel time u y' →
        ∀ t ≥ 0, y t = y' t) ∧
      (∀ y : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y →
        ∀ t ≥ 0, have E := y t 3; E ≤ 1) := by
  sorry

Inspect the energy bound of ten

The tube contract proves

E \le 9

, so it also certifies the requested bound

E \le 10

for the same initialized trajectory.5 Kernel checked 5 As recorded

end Decided_below_one

L541–541

Decisionbelow_10 · trajectory · forsetiNever runL544–544

trajectory ns-t3 from (1, 1, 1) at 0 observe E always : E <= 10

Not run yet.

namespace Decided_below_10

L546–546

open DecidedShared_5a37f797df5f

L548–548

Example `example (line 550)` Kernel checkedAs recorded L550–550

Namespace Notebook.NST3.Decided_below_10

Checked statement, as this project’s notation prints it

\text{forsetiTime}\;=\;\text{forsetiTime}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiTime Notebook.NST3.DecidedShared_5a37f797df5f.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiTime = @DecidedShared_5a37f797df5f.forsetiTime := rfl

Example `example (line 551)` Kernel checkedAs recorded L551–551

Namespace Notebook.NST3.Decided_below_10

Checked statement, as this project’s notation prints it

\text{forsetiInitial}\;=\;\text{forsetiInitial}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiInitial Notebook.NST3.DecidedShared_5a37f797df5f.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiInitial = @DecidedShared_5a37f797df5f.forsetiInitial := rfl

Example `example (line 552)` Kernel checkedAs recorded L552–552

Namespace Notebook.NST3.Decided_below_10

Checked statement, as this project’s notation prints it

\text{forsetiObservation}\;=\;\text{forsetiObservation}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiObservation
  Notebook.NST3.DecidedShared_5a37f797df5f.forsetiObservation

Assumptions: none

Lean source & proof · 1 line

example : @forsetiObservation = @DecidedShared_5a37f797df5f.forsetiObservation := rfl

Example `example (line 553)` Kernel checkedAs recorded L553–553

Namespace Notebook.NST3.Decided_below_10

Checked statement, as this project’s notation prints it

\text{forsetiIdentities}\;=\;\text{forsetiIdentities}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiIdentities Notebook.NST3.DecidedShared_5a37f797df5f.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiIdentities = @DecidedShared_5a37f797df5f.forsetiIdentities := rfl

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L555–556

Namespace Notebook.NST3.Decided_below_10

(.\text{atom}\;.\text{le}\;(.\text{add}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )\;(.\text{neg}\;(.\text{constant}\;(\text{mkRat}\;(10)\;1)))))

Lean source · 2 lines

def forsetiPost : Gimle.Forseti.Syntax.Formula 1 :=
  (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (10) 1)))))

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L558–561

Namespace Notebook.NST3.Decided_below_10

\langle \langle \text{[}\texttt{"E"}\text{]},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide}\rangle ,

\;(.\text{and}\;(.\text{atom}\;.\text{le}\;(.\text{neg}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )))\;(.\text{atom}\;.\text{le}\;(.\text{add}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )\;(.\text{neg}\;(.\text{constant}\;(\text{mkRat}\;(9)\;1)))))),

\;\text{forsetiPost}\rangle

Lean source · 4 lines

def forsetiLeaf : Gimle.Forseti.Syntax.Goal :=
  ⟨⟨["E"], by decide, by decide, by decide⟩,
    (.and (.atom .le (.neg (.var ⟨0, by decide⟩))) (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (9) 1)))))),
    forsetiPost⟩

Definition `forsetiContract` `: Prop` L563–568

Namespace Notebook.NST3.Decided_below_10

\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{observed}\;\text{forsetiTime}

\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Initialized}\;\text{forsetiTime}\;(\text{fun}\;\text{\_}\;=>\;\text{True})

\;(\text{·}\;=\;\text{forsetiInitial}))

\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Always}\;\text{forsetiTime}

\;\text{fun}\;\text{o}\;=>\;\text{forsetiPost}.\text{holds}\;(\text{fun}\;\text{\_}\;=>\;\text{o}\;\text{forsetiObservation}))

Lean source · 6 lines

def forsetiContract : Prop :=
  Gimle.Forseti.Trajectory.Contract Gimle.Forseti.Examples.GalerkinNS.T3.observed forsetiTime
    (Gimle.Forseti.Trajectory.Initialized forsetiTime (fun _ => True)
      (· = forsetiInitial))
    (Gimle.Forseti.Trajectory.Always forsetiTime
      fun o => forsetiPost.holds (fun _ => o forsetiObservation))

Definition `forsetiRoot` `: Prop` L570–570

Namespace Notebook.NST3.Decided_below_10

\text{forsetiIdentities}\;\land \;\text{forsetiContract}

Lean source · 1 line

def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem `below_10` Kernel checkedAs recorded L572–613

Namespace Notebook.NST3.Decided_below_10

Statement

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

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 42 lines

/-- E is output 3 of the compiled circuit, the port obs-e; the input's initial wires (initial-a10, initial-a11, initial-a21) start at (1, 1, 1) at time = 0. The trajectory decider proved it. Goal (trajectory): trajectory ns-t3 interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-e as E always : E <= 10 -/
theorem below_10 :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.T3.observed
    have time : Gimle.Asgard.Dynamics.TimeDomain := ⟨"time", 0⟩
    ∀ u : Gimle.Asgard.Dynamics.Signal (0 + 3),
      Gimle.Asgard.Dynamics.signalRight u 0 = ![1, 1, 1] →
      (∃ y : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y) ∧
      (∀ y y' : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y → circuit.Rel time u y' →
        ∀ t ≥ 0, y t = y' t) ∧
      (∀ y : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y →
        ∀ t ≥ 0, have E := y t 3; E ≤ 10) := by
  have root : forsetiRoot := by
    unfold forsetiRoot forsetiIdentities forsetiContract
    refine ⟨⟨by decide, by decide, by decide⟩, ?_⟩
    have time : forsetiTime = Gimle.Forseti.Examples.GalerkinNS.T3.evolution.time := by simp [forsetiTime, Gimle.Asgard.Model.Evolution.time, Gimle.Forseti.Examples.GalerkinNS.T3.evolution] <;> norm_num [Rat.mkRat_eq_div]
    have init : forsetiInitial = Gimle.Forseti.Examples.GalerkinNS.T3.compiled.initial := by rw [Gimle.Forseti.Examples.GalerkinNS.T3.initial_eq]; funext i; fin_cases i <;> norm_num [forsetiInitial, Rat.mkRat_eq_div]
    have obs : forsetiObservation = Gimle.Forseti.Examples.GalerkinNS.T3.energyIndex := rfl
    rw [time, init, obs]
    refine Gimle.Forseti.Trajectory.Contract.consequence Gimle.Forseti.Examples.GalerkinNS.T3.below9_contract (fun _ admitted => admitted) ?_
    intro o band t within
    have leaf := Gimle.Forseti.Syntax.EntailmentCertificate.sound forsetiLeaf ⟨[⟨⟨[((mkRat (1) 1), (.constant (mkRat (1) 1)))]⟩, [⟨[]⟩, ⟨[((mkRat (1) 1), (.constant (mkRat (1) 1)))]⟩]⟩]⟩ (by decide +kernel)
    apply leaf
    simp only [forsetiLeaf, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval]
    obtain ⟨low, high⟩ := band t within
    refine ⟨?_, ?_⟩ <;> norm_num [Rat.mkRat_eq_div] <;> linarith
  have forsetiCast0 : (((mkRat (10) 1) : ℚ) : ℝ) = 10 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast1 : (((mkRat (0) 1) : ℚ) : ℝ) = 0 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast2 : (((mkRat (1) 1) : ℚ) : ℝ) = 1 := by norm_num [Rat.mkRat_eq_div]
  refine (fun (bridge : _ ↔ forsetiContract) => bridge.mpr (show forsetiIdentities ∧ forsetiContract from root).2) ?_
  constructor
  · intro claim
    unfold forsetiContract
    set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc] at claim
    refine ⟨?_, ?_, ?_⟩ <;> set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc]
    · exact fun u start => (claim u start).1
    · exact fun u start => (claim u start).2.1
    · exact fun u start => (claim u start).2.2
  · intro lane
    unfold forsetiContract at lane
    obtain ⟨realizable, unique, holds⟩ := lane
    set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc] at realizable unique holds ⊢
    exact fun u start => ⟨realizable u start, unique u start, holds u start⟩

Compare a certified bound with an unresolved one

The request

E \le 8

remains unknown; the next request

E \le 12

is certified from the tube contract. The earlier ellipsoid argument explains another route to

12

, but neither certificate settles

8

.5 Kernel checked 5 As recorded

end Decided_below_10

L623–623

Decisionbelow_8 · trajectory · forsetiNever runL626–626

trajectory ns-t3 from (1, 1, 1) at 0 observe E always : E <= 8

Not run yet.

Decisionbelow_12 · trajectory · forsetiNever runL628–628

trajectory ns-t3 from (1, 1, 1) at 0 observe E always : E <= 12

Not run yet.

namespace Decided_below_12

L630–630

open DecidedShared_5a37f797df5f

L632–632

Example `example (line 634)` Kernel checkedAs recorded L634–634

Namespace Notebook.NST3.Decided_below_12

Checked statement, as this project’s notation prints it

\text{forsetiTime}\;=\;\text{forsetiTime}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiTime Notebook.NST3.DecidedShared_5a37f797df5f.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiTime = @DecidedShared_5a37f797df5f.forsetiTime := rfl

Example `example (line 635)` Kernel checkedAs recorded L635–635

Namespace Notebook.NST3.Decided_below_12

Checked statement, as this project’s notation prints it

\text{forsetiInitial}\;=\;\text{forsetiInitial}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiInitial Notebook.NST3.DecidedShared_5a37f797df5f.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiInitial = @DecidedShared_5a37f797df5f.forsetiInitial := rfl

Example `example (line 636)` Kernel checkedAs recorded L636–636

Namespace Notebook.NST3.Decided_below_12

Checked statement, as this project’s notation prints it

\text{forsetiObservation}\;=\;\text{forsetiObservation}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiObservation
  Notebook.NST3.DecidedShared_5a37f797df5f.forsetiObservation

Assumptions: none

Lean source & proof · 1 line

example : @forsetiObservation = @DecidedShared_5a37f797df5f.forsetiObservation := rfl

Example `example (line 637)` Kernel checkedAs recorded L637–637

Namespace Notebook.NST3.Decided_below_12

Checked statement, as this project’s notation prints it

\text{forsetiIdentities}\;=\;\text{forsetiIdentities}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_5a37f797df5f.forsetiIdentities Notebook.NST3.DecidedShared_5a37f797df5f.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiIdentities = @DecidedShared_5a37f797df5f.forsetiIdentities := rfl

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L639–640

Namespace Notebook.NST3.Decided_below_12

(.\text{atom}\;.\text{le}\;(.\text{add}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )\;(.\text{neg}\;(.\text{constant}\;(\text{mkRat}\;(12)\;1)))))

Lean source · 2 lines

def forsetiPost : Gimle.Forseti.Syntax.Formula 1 :=
  (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (12) 1)))))

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L642–645

Namespace Notebook.NST3.Decided_below_12

\langle \langle \text{[}\texttt{"E"}\text{]},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide}\rangle ,

\;(.\text{and}\;(.\text{atom}\;.\text{le}\;(.\text{neg}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )))\;(.\text{atom}\;.\text{le}\;(.\text{add}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )\;(.\text{neg}\;(.\text{constant}\;(\text{mkRat}\;(9)\;1)))))),

\;\text{forsetiPost}\rangle

Lean source · 4 lines

def forsetiLeaf : Gimle.Forseti.Syntax.Goal :=
  ⟨⟨["E"], by decide, by decide, by decide⟩,
    (.and (.atom .le (.neg (.var ⟨0, by decide⟩))) (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (9) 1)))))),
    forsetiPost⟩

Definition `forsetiContract` `: Prop` L647–652

Namespace Notebook.NST3.Decided_below_12

\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{observed}\;\text{forsetiTime}

\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Initialized}\;\text{forsetiTime}\;(\text{fun}\;\text{\_}\;=>\;\text{True})

\;(\text{·}\;=\;\text{forsetiInitial}))

\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Always}\;\text{forsetiTime}

\;\text{fun}\;\text{o}\;=>\;\text{forsetiPost}.\text{holds}\;(\text{fun}\;\text{\_}\;=>\;\text{o}\;\text{forsetiObservation}))

Lean source · 6 lines

def forsetiContract : Prop :=
  Gimle.Forseti.Trajectory.Contract Gimle.Forseti.Examples.GalerkinNS.T3.observed forsetiTime
    (Gimle.Forseti.Trajectory.Initialized forsetiTime (fun _ => True)
      (· = forsetiInitial))
    (Gimle.Forseti.Trajectory.Always forsetiTime
      fun o => forsetiPost.holds (fun _ => o forsetiObservation))

Definition `forsetiRoot` `: Prop` L654–654

Namespace Notebook.NST3.Decided_below_12

\text{forsetiIdentities}\;\land \;\text{forsetiContract}

Lean source · 1 line

def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem `below_12` Kernel checkedAs recorded L656–697

Namespace Notebook.NST3.Decided_below_12

Statement

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

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 42 lines

/-- E is output 3 of the compiled circuit, the port obs-e; the input's initial wires (initial-a10, initial-a11, initial-a21) start at (1, 1, 1) at time = 0. The trajectory decider proved it. Goal (trajectory): trajectory ns-t3 interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-e as E always : E <= 12 -/
theorem below_12 :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.T3.observed
    have time : Gimle.Asgard.Dynamics.TimeDomain := ⟨"time", 0⟩
    ∀ u : Gimle.Asgard.Dynamics.Signal (0 + 3),
      Gimle.Asgard.Dynamics.signalRight u 0 = ![1, 1, 1] →
      (∃ y : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y) ∧
      (∀ y y' : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y → circuit.Rel time u y' →
        ∀ t ≥ 0, y t = y' t) ∧
      (∀ y : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y →
        ∀ t ≥ 0, have E := y t 3; E ≤ 12) := by
  have root : forsetiRoot := by
    unfold forsetiRoot forsetiIdentities forsetiContract
    refine ⟨⟨by decide, by decide, by decide⟩, ?_⟩
    have time : forsetiTime = Gimle.Forseti.Examples.GalerkinNS.T3.evolution.time := by simp [forsetiTime, Gimle.Asgard.Model.Evolution.time, Gimle.Forseti.Examples.GalerkinNS.T3.evolution] <;> norm_num [Rat.mkRat_eq_div]
    have init : forsetiInitial = Gimle.Forseti.Examples.GalerkinNS.T3.compiled.initial := by rw [Gimle.Forseti.Examples.GalerkinNS.T3.initial_eq]; funext i; fin_cases i <;> norm_num [forsetiInitial, Rat.mkRat_eq_div]
    have obs : forsetiObservation = Gimle.Forseti.Examples.GalerkinNS.T3.energyIndex := rfl
    rw [time, init, obs]
    refine Gimle.Forseti.Trajectory.Contract.consequence Gimle.Forseti.Examples.GalerkinNS.T3.below9_contract (fun _ admitted => admitted) ?_
    intro o band t within
    have leaf := Gimle.Forseti.Syntax.EntailmentCertificate.sound forsetiLeaf ⟨[⟨⟨[((mkRat (3) 1), (.constant (mkRat (1) 1)))]⟩, [⟨[]⟩, ⟨[((mkRat (1) 1), (.constant (mkRat (1) 1)))]⟩]⟩]⟩ (by decide +kernel)
    apply leaf
    simp only [forsetiLeaf, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval]
    obtain ⟨low, high⟩ := band t within
    refine ⟨?_, ?_⟩ <;> norm_num [Rat.mkRat_eq_div] <;> linarith
  have forsetiCast0 : (((mkRat (12) 1) : ℚ) : ℝ) = 12 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast1 : (((mkRat (0) 1) : ℚ) : ℝ) = 0 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast2 : (((mkRat (1) 1) : ℚ) : ℝ) = 1 := by norm_num [Rat.mkRat_eq_div]
  refine (fun (bridge : _ ↔ forsetiContract) => bridge.mpr (show forsetiIdentities ∧ forsetiContract from root).2) ?_
  constructor
  · intro claim
    unfold forsetiContract
    set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc] at claim
    refine ⟨?_, ?_, ?_⟩ <;> set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc]
    · exact fun u start => (claim u start).1
    · exact fun u start => (claim u start).2.1
    · exact fun u start => (claim u start).2.2
  · intro lane
    unfold forsetiContract at lane
    obtain ⟨realizable, unique, holds⟩ := lane
    set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc] at realizable unique holds ⊢
    exact fun u start => ⟨realizable u start, unique u start, holds u start⟩

Inspect the enstrophy bound of twenty-six

The enstrophy contract certifies existence, uniqueness and

0 \le Z \le 26

for all time from the stated start. This supports the amplitude bounds above; the later request

Z \le 20

remains unknown.5 Kernel checked 5 As recorded

end Decided_below_12

L707–707

Decisionin_enstrophy_ball · trajectory · forsetiNever runL710–710

trajectory ns-t3 from (1, 1, 1) at 0 observe Z always : Z >= 0 and Z <= 26

Not run yet.

namespace DecidedShared_05178f0d2091

L712–712

Definition `forsetiTime` `: Gimle.Asgard.Dynamics.TimeDomain` L714–715

Namespace Notebook.NST3.DecidedShared_05178f0d2091

\langle \texttt{"time"},\;(((\text{mkRat}\;(0)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} )\rangle

Lean source · 2 lines

def forsetiTime : Gimle.Asgard.Dynamics.TimeDomain :=
  ⟨"time", (((mkRat (0) 1) : ℚ) : ℝ)⟩

Definition `forsetiInitial` `: Gimle.Asgard.Point 3` L717–718

Namespace Notebook.NST3.DecidedShared_05178f0d2091

!\text{[}(((\text{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} ),\;(((\text{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} ),\;(((\text{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} )\text{]}

Lean source · 2 lines

def forsetiInitial : Gimle.Asgard.Point 3 :=
  ![(((mkRat (1) 1) : ℚ) : ℝ), (((mkRat (1) 1) : ℚ) : ℝ), (((mkRat (1) 1) : ℚ) : ℝ)]

Definition `forsetiObservation` `: Fin 6` L720–720

Namespace Notebook.NST3.DecidedShared_05178f0d2091

\langle 4,\;\text{by}\;\text{decide}\rangle

Lean source · 1 line

def forsetiObservation : Fin 6 := ⟨4, by decide⟩

Definition `forsetiIdentities` `: Prop` L722–726

Namespace Notebook.NST3.DecidedShared_05178f0d2091

\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{evolution}.\text{states}.\text{map}\;(\text{·}.\text{initialId})\;=\;\text{[}\texttt{"initial-a10"},\;\texttt{"initial-a11"},\;\texttt{"initial-a21"}\text{]}\;\land

\;(\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{body}.\text{observations}.\text{get}\;\text{forsetiObservation}).\text{port}.\text{id}\;=

\;\texttt{"obs-z"}\;\land

\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{evolution}.\text{axis}.\text{id}\;=\;\texttt{"time"}

Lean source · 5 lines

def forsetiIdentities : Prop :=
  Gimle.Forseti.Examples.GalerkinNS.T3.evolution.states.map (·.initialId) = ["initial-a10", "initial-a11", "initial-a21"] ∧
  (Gimle.Forseti.Examples.GalerkinNS.T3.body.observations.get forsetiObservation).port.id =
    "obs-z" ∧
  Gimle.Forseti.Examples.GalerkinNS.T3.evolution.axis.id = "time"

end DecidedShared_05178f0d2091

L728–728

namespace Decided_in_enstrophy_ball

L730–730

open DecidedShared_05178f0d2091

L732–732

Example `example (line 734)` Kernel checkedAs recorded L734–734

Namespace Notebook.NST3.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it

\text{forsetiTime}\;=\;\text{forsetiTime}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_05178f0d2091.forsetiTime Notebook.NST3.DecidedShared_05178f0d2091.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiTime = @DecidedShared_05178f0d2091.forsetiTime := rfl

Example `example (line 735)` Kernel checkedAs recorded L735–735

Namespace Notebook.NST3.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it

\text{forsetiInitial}\;=\;\text{forsetiInitial}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_05178f0d2091.forsetiInitial Notebook.NST3.DecidedShared_05178f0d2091.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiInitial = @DecidedShared_05178f0d2091.forsetiInitial := rfl

Example `example (line 736)` Kernel checkedAs recorded L736–736

Namespace Notebook.NST3.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it

\text{forsetiObservation}\;=\;\text{forsetiObservation}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_05178f0d2091.forsetiObservation
  Notebook.NST3.DecidedShared_05178f0d2091.forsetiObservation

Assumptions: none

Lean source & proof · 1 line

example : @forsetiObservation = @DecidedShared_05178f0d2091.forsetiObservation := rfl

Example `example (line 737)` Kernel checkedAs recorded L737–737

Namespace Notebook.NST3.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it

\text{forsetiIdentities}\;=\;\text{forsetiIdentities}

Kernel form, without notation

Eq Notebook.NST3.DecidedShared_05178f0d2091.forsetiIdentities Notebook.NST3.DecidedShared_05178f0d2091.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiIdentities = @DecidedShared_05178f0d2091.forsetiIdentities := rfl

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L739–740

Namespace Notebook.NST3.Decided_in_enstrophy_ball

(.\text{and}\;(.\text{atom}\;.\text{ge}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle ))\;(.\text{atom}\;.\text{le}\;(.\text{add}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )\;(.\text{neg}\;(.\text{constant}\;(\text{mkRat}\;(26)\;1))))))

Lean source · 2 lines

def forsetiPost : Gimle.Forseti.Syntax.Formula 1 :=
  (.and (.atom .ge (.var ⟨0, by decide⟩)) (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (26) 1))))))

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L742–745

Namespace Notebook.NST3.Decided_in_enstrophy_ball

\langle \langle \text{[}\texttt{"Z"}\text{]},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide}\rangle ,

\;(.\text{and}\;(.\text{atom}\;.\text{le}\;(.\text{neg}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )))\;(.\text{atom}\;.\text{le}\;(.\text{add}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )\;(.\text{neg}\;(.\text{constant}\;(\text{mkRat}\;(26)\;1)))))),

\;\text{forsetiPost}\rangle

Lean source · 4 lines

def forsetiLeaf : Gimle.Forseti.Syntax.Goal :=
  ⟨⟨["Z"], by decide, by decide, by decide⟩,
    (.and (.atom .le (.neg (.var ⟨0, by decide⟩))) (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (26) 1)))))),
    forsetiPost⟩

Definition `forsetiContract` `: Prop` L747–752

Namespace Notebook.NST3.Decided_in_enstrophy_ball

\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3}.\text{observed}\;\text{forsetiTime}

\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Initialized}\;\text{forsetiTime}\;(\text{fun}\;\text{\_}\;=>\;\text{True})

\;(\text{·}\;=\;\text{forsetiInitial}))

\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Always}\;\text{forsetiTime}

\;\text{fun}\;\text{o}\;=>\;\text{forsetiPost}.\text{holds}\;(\text{fun}\;\text{\_}\;=>\;\text{o}\;\text{forsetiObservation}))

Lean source · 6 lines

def forsetiContract : Prop :=
  Gimle.Forseti.Trajectory.Contract Gimle.Forseti.Examples.GalerkinNS.T3.observed forsetiTime
    (Gimle.Forseti.Trajectory.Initialized forsetiTime (fun _ => True)
      (· = forsetiInitial))
    (Gimle.Forseti.Trajectory.Always forsetiTime
      fun o => forsetiPost.holds (fun _ => o forsetiObservation))

Definition `forsetiRoot` `: Prop` L754–754

Namespace Notebook.NST3.Decided_in_enstrophy_ball

\text{forsetiIdentities}\;\land \;\text{forsetiContract}

Lean source · 1 line

def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem `in_enstrophy_ball` Kernel checkedAs recorded L756–797

Namespace Notebook.NST3.Decided_in_enstrophy_ball

Z is output 4 of the compiled circuit, the port obs-z; the input's initial wires (initial-a10, initial-a11, initial-a21) start at (1, 1, 1) at time = 0. The trajectory decider proved it. Goal (trajectory): trajectory ns-t3 interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-z as Z always : Z >= 0 and Z <= 26

Statement

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

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 42 lines

/-- Z is output 4 of the compiled circuit, the port obs-z; the input's initial wires (initial-a10, initial-a11, initial-a21) start at (1, 1, 1) at time = 0. The trajectory decider proved it. Goal (trajectory): trajectory ns-t3 interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-z as Z always : Z >= 0 and Z <= 26 -/
theorem in_enstrophy_ball :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.T3.observed
    have time : Gimle.Asgard.Dynamics.TimeDomain := ⟨"time", 0⟩
    ∀ u : Gimle.Asgard.Dynamics.Signal (0 + 3),
      Gimle.Asgard.Dynamics.signalRight u 0 = ![1, 1, 1] →
      (∃ y : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y) ∧
      (∀ y y' : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y → circuit.Rel time u y' →
        ∀ t ≥ 0, y t = y' t) ∧
      (∀ y : Gimle.Asgard.Dynamics.Signal 6, circuit.Rel time u y →
        ∀ t ≥ 0, have Z := y t 4; Z ≥ 0 ∧ Z ≤ 26) := by
  have root : forsetiRoot := by
    unfold forsetiRoot forsetiIdentities forsetiContract
    refine ⟨⟨by decide, by decide, by decide⟩, ?_⟩
    have time : forsetiTime = Gimle.Forseti.Examples.GalerkinNS.T3.evolution.time := by simp [forsetiTime, Gimle.Asgard.Model.Evolution.time, Gimle.Forseti.Examples.GalerkinNS.T3.evolution] <;> norm_num [Rat.mkRat_eq_div]
    have init : forsetiInitial = Gimle.Forseti.Examples.GalerkinNS.T3.compiled.initial := by rw [Gimle.Forseti.Examples.GalerkinNS.T3.initial_eq]; funext i; fin_cases i <;> norm_num [forsetiInitial, Rat.mkRat_eq_div]
    have obs : forsetiObservation = Gimle.Forseti.Examples.GalerkinNS.T3.enstrophyIndex := rfl
    rw [time, init, obs]
    refine Gimle.Forseti.Trajectory.Contract.consequence Gimle.Forseti.Examples.GalerkinNS.T3.enstrophy_contract (fun _ admitted => admitted) ?_
    intro o band t within
    have leaf := Gimle.Forseti.Syntax.EntailmentCertificate.sound forsetiLeaf ⟨[⟨⟨[]⟩, [⟨[((mkRat (1) 1), (.constant (mkRat (1) 1)))]⟩, ⟨[]⟩]⟩, ⟨⟨[]⟩, [⟨[]⟩, ⟨[((mkRat (1) 1), (.constant (mkRat (1) 1)))]⟩]⟩]⟩ (by decide +kernel)
    apply leaf
    simp only [forsetiLeaf, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval]
    obtain ⟨low, high⟩ := band t within
    refine ⟨?_, ?_⟩ <;> norm_num [Rat.mkRat_eq_div] <;> linarith
  have forsetiCast0 : (((mkRat (26) 1) : ℚ) : ℝ) = 26 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast1 : (((mkRat (0) 1) : ℚ) : ℝ) = 0 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast2 : (((mkRat (1) 1) : ℚ) : ℝ) = 1 := by norm_num [Rat.mkRat_eq_div]
  refine (fun (bridge : _ ↔ forsetiContract) => bridge.mpr (show forsetiIdentities ∧ forsetiContract from root).2) ?_
  constructor
  · intro claim
    unfold forsetiContract
    set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc] at claim
    refine ⟨?_, ?_, ?_⟩ <;> set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc]
    · exact fun u start => (claim u start).1
    · exact fun u start => (claim u start).2.1
    · exact fun u start => (claim u start).2.2
  · intro lane
    unfold forsetiContract at lane
    obtain ⟨realizable, unique, holds⟩ := lane
    set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Trajectory.Realizable, Gimle.Forseti.Trajectory.Unique, Gimle.Forseti.Trajectory.Holds, Gimle.Forseti.Trajectory.Initialized, Gimle.Forseti.Trajectory.Always, Set.EqOn, Gimle.Asgard.Dynamics.TimeDomain.domain, Set.mem_Ici, forsetiTime, forsetiInitial, forsetiPost, forsetiObservation, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, true_and, forsetiCast0, forsetiCast1, forsetiCast2, ← sub_eq_add_neg, sub_zero, sub_nonpos, sub_neg, sub_eq_zero, sub_nonneg, sub_pos, ge_iff_le, gt_iff_lt, and_assoc, or_assoc] at realizable unique holds ⊢
    exact fun u start => ⟨realizable u start, unique u start, holds u start⟩

end Decided_in_enstrophy_ball

L799–799

Decisionenstrophy_below_20 · trajectory · forsetiNever runL802–802

trajectory ns-t3 from (1, 1, 1) at 0 observe Z always : Z <= 20

Not run yet.

Scope and unresolved bounds

These are statements about the compiled three-mode ODE at the stated viscosity, forcing and initial state. They do not establish an approximation or limiting theorem for the Navier–Stokes PDE. Simulations and certificate searches guide the questions but are not proofs. The requests $E \le 8$ and $Z \le 20$ remain unknown; their absence from a section's claim counts does not make them settled.

#print axioms triad_lossless

L815–815

#print axioms energy_rate

L816–816

#print axioms laminar_energy

L817–817

#print axioms laminar_is_equilibrium

L818–818

#print axioms ellipsoid_excludes_laminar

L819–819

#print axioms ellipsoid_below_twelve

L820–820

#print axioms tube_excludes_laminar

L821–821

#print axioms tube_below_nine

L822–822

#print axioms certificate_here

L823–823

#print axioms is_family_member

L824–824

#print axioms every_member

L825–825

#print axioms enstrophy_rate

L826–826

#print axioms laminar_enstrophy

L827–827

#print axioms enstrophy_certificate_here

L828–828

#print axioms amplitude_bound

L829–829

#print axioms only_two

L830–830

end Notebook.NST3

L832–832

The equations

The system, compiled

model diagram Gimle.Forseti.Examples.GalerkinNS.T3.compiled L87–87

What a simulation shows

Derive the reusable energy bound

Cancel the triad energy transfers

Theorem triad_lossless Kernel checkedAs recorded L122–127

Theorem energy_rate Kernel checkedAs recorded L138–143

Turn the identity into a trapping ball

Theorem laminar_energy Kernel checkedAs recorded L168–170

Theorem certificate_here Kernel checkedAs recorded L172–176

Connect this system to the finite family

Theorem is_family_member Kernel checkedAs recorded L199–203

Theorem every_member Kernel checkedAs recorded L205–218

Bound enstrophy and individual amplitudes

Derive the enstrophy certificate

Theorem enstrophy_rate Kernel checkedAs recorded L248–253

Theorem laminar_enstrophy Kernel checkedAs recorded L255–257

Theorem enstrophy_certificate_here Kernel checkedAs recorded L259–263

Theorem amplitude_bound Kernel checkedAs recorded L265–271

Explain the limit of diagonal reweighting

Theorem only_two Kernel checkedAs recorded L290–297

Sharpen the bound for this initial state

Trap the trajectory in an ellipsoid

Theorem laminar_is_equilibrium Kernel checkedAs recorded L336–338

Theorem ellipsoid_excludes_laminar Kernel checkedAs recorded L340–343

Theorem ellipsoid_below_twelve Kernel checkedAs recorded L345–348

Tighten the bound with a quartic tube

Theorem tube_excludes_laminar Kernel checkedAs recorded L365–368

Theorem tube_below_nine Kernel checkedAs recorded L370–373

Inspect the decided trajectory contracts

Inspect the energy bound of thirteen

Definition forsetiTime : Gimle.Asgard.Dynamics.TimeDomain L403–404

Definition forsetiInitial : Gimle.Asgard.Point 3 L406–407

Definition forsetiObservation : Fin 6 L409–409

Definition forsetiIdentities : Prop L411–415

Example example (line 423) Kernel checkedAs recorded L423–423

Example example (line 424) Kernel checkedAs recorded L424–424

Example example (line 425) Kernel checkedAs recorded L425–425

Example example (line 426) Kernel checkedAs recorded L426–426

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L428–429

Definition forsetiLeaf : Gimle.Forseti.Syntax.Goal L431–434

Definition forsetiContract : Prop L436–441

Definition forsetiRoot : Prop L443–443

Theorem in_ball Kernel checkedAs recorded L445–486

Inspect the refuted energy bound of one

Example example (line 504) Kernel checkedAs recorded L504–504

Example example (line 505) Kernel checkedAs recorded L505–505

Example example (line 506) Kernel checkedAs recorded L506–506

Example example (line 507) Kernel checkedAs recorded L507–507

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L509–510

Definition forsetiContract : Prop L512–517

Definition forsetiRoot : Prop L519–519

Theorem below_one Contains sorryAs recorded L521–532

Inspect the energy bound of ten

Example example (line 550) Kernel checkedAs recorded L550–550

Example example (line 551) Kernel checkedAs recorded L551–551

Example example (line 552) Kernel checkedAs recorded L552–552

Example example (line 553) Kernel checkedAs recorded L553–553

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L555–556

Definition forsetiLeaf : Gimle.Forseti.Syntax.Goal L558–561

Definition forsetiContract : Prop L563–568

Definition forsetiRoot : Prop L570–570

Theorem below_10 Kernel checkedAs recorded L572–613

Compare a certified bound with an unresolved one

Example example (line 634) Kernel checkedAs recorded L634–634

Example example (line 635) Kernel checkedAs recorded L635–635

Example example (line 636) Kernel checkedAs recorded L636–636

Example example (line 637) Kernel checkedAs recorded L637–637

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L639–640

Definition forsetiLeaf : Gimle.Forseti.Syntax.Goal L642–645

Definition forsetiContract : Prop L647–652

Definition forsetiRoot : Prop L654–654

Theorem below_12 Kernel checkedAs recorded L656–697

Inspect the enstrophy bound of twenty-six

Definition forsetiTime : Gimle.Asgard.Dynamics.TimeDomain L714–715

Definition forsetiInitial : Gimle.Asgard.Point 3 L717–718

Definition forsetiObservation : Fin 6 L720–720

Definition forsetiIdentities : Prop L722–726

Example example (line 734) Kernel checkedAs recorded L734–734

model diagram `Gimle.Forseti.Examples.GalerkinNS.T3.compiled` L87–87

Theorem `triad_lossless` Kernel checkedAs recorded L122–127

Theorem `energy_rate` Kernel checkedAs recorded L138–143

Theorem `laminar_energy` Kernel checkedAs recorded L168–170

Theorem `certificate_here` Kernel checkedAs recorded L172–176

Theorem `is_family_member` Kernel checkedAs recorded L199–203

Theorem `every_member` Kernel checkedAs recorded L205–218

Theorem `enstrophy_rate` Kernel checkedAs recorded L248–253

Theorem `laminar_enstrophy` Kernel checkedAs recorded L255–257

Theorem `enstrophy_certificate_here` Kernel checkedAs recorded L259–263

Theorem `amplitude_bound` Kernel checkedAs recorded L265–271

Theorem `only_two` Kernel checkedAs recorded L290–297

Theorem `laminar_is_equilibrium` Kernel checkedAs recorded L336–338

Theorem `ellipsoid_excludes_laminar` Kernel checkedAs recorded L340–343

Theorem `ellipsoid_below_twelve` Kernel checkedAs recorded L345–348

Theorem `tube_excludes_laminar` Kernel checkedAs recorded L365–368

Theorem `tube_below_nine` Kernel checkedAs recorded L370–373

Definition `forsetiTime` `: Gimle.Asgard.Dynamics.TimeDomain` L403–404

Definition `forsetiInitial` `: Gimle.Asgard.Point 3` L406–407

Definition `forsetiObservation` `: Fin 6` L409–409

Definition `forsetiIdentities` `: Prop` L411–415

Example `example (line 423)` Kernel checkedAs recorded L423–423

Example `example (line 424)` Kernel checkedAs recorded L424–424

Example `example (line 425)` Kernel checkedAs recorded L425–425

Example `example (line 426)` Kernel checkedAs recorded L426–426

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L428–429

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L431–434

Definition `forsetiContract` `: Prop` L436–441

Definition `forsetiRoot` `: Prop` L443–443

Theorem `in_ball` Kernel checkedAs recorded L445–486

Example `example (line 504)` Kernel checkedAs recorded L504–504

Example `example (line 505)` Kernel checkedAs recorded L505–505

Example `example (line 506)` Kernel checkedAs recorded L506–506

Example `example (line 507)` Kernel checkedAs recorded L507–507

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L509–510

Definition `forsetiContract` `: Prop` L512–517

Definition `forsetiRoot` `: Prop` L519–519

Theorem `below_one` Contains sorryAs recorded L521–532

Example `example (line 550)` Kernel checkedAs recorded L550–550

Example `example (line 551)` Kernel checkedAs recorded L551–551

Example `example (line 552)` Kernel checkedAs recorded L552–552

Example `example (line 553)` Kernel checkedAs recorded L553–553

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L555–556

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L558–561

Definition `forsetiContract` `: Prop` L563–568

Definition `forsetiRoot` `: Prop` L570–570

Theorem `below_10` Kernel checkedAs recorded L572–613

Example `example (line 634)` Kernel checkedAs recorded L634–634

Example `example (line 635)` Kernel checkedAs recorded L635–635

Example `example (line 636)` Kernel checkedAs recorded L636–636

Example `example (line 637)` Kernel checkedAs recorded L637–637

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L639–640

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L642–645

Definition `forsetiContract` `: Prop` L647–652

Definition `forsetiRoot` `: Prop` L654–654

Theorem `below_12` Kernel checkedAs recorded L656–697

Definition `forsetiTime` `: Gimle.Asgard.Dynamics.TimeDomain` L714–715

Definition `forsetiInitial` `: Gimle.Asgard.Point 3` L717–718

Definition `forsetiObservation` `: Fin 6` L720–720

Definition `forsetiIdentities` `: Prop` L722–726

Example `example (line 734)` Kernel checkedAs recorded L734–734

Example `example (line 735)` Kernel checkedAs recorded L735–735

Example `example (line 736)` Kernel checkedAs recorded L736–736

Example `example (line 737)` Kernel checkedAs recorded L737–737

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L739–740

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L742–745

Definition `forsetiContract` `: Prop` L747–752

Definition `forsetiRoot` `: Prop` L754–754

Theorem `in_enstrophy_ball` Kernel checkedAs recorded L756–797