A 12-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.B2

L3–3

Two-dimensional incompressible flow on the periodic square, kept to the twelve cosine modes of the vorticity with wavevectors in the block $|k_x|, |k_y| \le 2$ , forced in $(1, 1)$ and damped in all, at a viscosity ( $\nu = \tfrac{1}{50}$ ) where the simulated flow wanders irregularly for as long as it is run, and is still trapped. The energy bound is proved as for T3 (NS_T3.lean), from twenty-two triads instead of one; this page keeps the exposition short and links there for the derivation. The family theorem that covers every member is restated below.

Read the argument in three stages: the reusable energy bound, enstrophy and amplitude control, and the decided requests. Expand a stage for its explanation and individual claims.

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 313$ throughout. Decided by the trajectory decider from a named Lean contract; its artifact replays without the solver. Its enstrophy $Z = \sum_k a_k^2$ satisfies $0 \le Z \le 626$ throughout, by the same decider from a second named contract, so every amplitude satisfies $|a_k| \le 26$ (amplitude_bound).

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

Unknown. $E \le 150$ and $Z \le 600$ for all $t \ge 0$ . The retained requests have neither a proof nor a refutation. Numerical runs do not settle these bounds.

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 equations

Two-dimensional incompressible flow on the periodic square, in vorticity form, keeps only the cosine modes $(0, 1)$ , $(0, 2)$ , $(1, -2)$ , $(1, -1)$ , $(1, 0)$ , $(1, 1)$ , $(1, 2)$ , $(2, -2)$ , $(2, -1)$ , $(2, 0)$ , $(2, 1)$ , $(2, 2)$ of the vorticity, with viscosity $\nu = \tfrac{1}{50}$ 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 22 triads. Twelve equations with up to a dozen terms each; Lean draws them below rather than this page listing them.

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.NSB2

L65–65

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

L66–67

model diagram `Gimle.Forseti.Examples.GalerkinNS.B2.compiled` L69–69

Observations a01 a02 a1m2 a1m1 a10 a11 a12 a2m2 a2m1 a20 a21 a22 E Z R

Evidence · not proofsimulate Gimle.Forseti.Examples.GalerkinNS.B2.compiled · forsetiNever runL70–70

Not run yet.

What a simulation shows

The panel above integrates the compiled field with RK4 from the same start, $h = \tfrac{1}{50}$ over $t \le 200$ , and draws the twelve amplitudes and $a_{(1,1)}$ against $a_{(2,1)}$ . The energy, computed from that run, goes from $\tfrac{91}{20}$ to a peak near $98$ at $t \approx 99$ , falls back to about $75$ by $t \approx 140$ and stays within $74$ – $77$ to the end, the amplitudes oscillating with a period near $1.35$ . Runs we made of the same equations at other steps, outside the workbench and not kept here, tell other stories: at $h = \tfrac{1}{100}$ the energy wandered between about $19$ and $98$ and kept wandering to $t = 2000$ , peaking near $103$ ; at $h = \tfrac{1}{200}$ it settled on an orbit near $E = 71.5$ . That sensitivity to the integrator is why this page says *irregular in simulation* and no more. It is evidence about runs, not a status.

Derive the reusable energy bound

Triad cancellation gives an energy identity and a sum-of-squares certificate. Each energy ball with threshold above

625/2

is invariant; a start inside it has a unique global trajectory under the family hypotheses.6 Kernel checked 6 As recorded

Cancel the triad energy transfers

The weights

1/\lambda_k

cancel the cubic transfers within each triad. The resulting identity is checked against this member's compiled field.2 Kernel checked 2 As recorded

As in T3 (NS_T3.lean): each mode is a *storage element* and each triad a *lossless three-port*, so summing the storage identities with the weights $1/\lambda_k$ cancels every cubic term triad by triad. Here is one of this member's triads, checked as plain arithmetic:

Theorem `triad_lossless` Kernel checkedAs recorded L105–110

Namespace Notebook.NSB2

The triad $\{a_{(0,1)}, a_{(1,-2)}, a_{(1,-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/5\;:\;\mathbb{R} )\;\cdot \;(-1/4)\;+\;(1/2\;:\;\mathbb{R} )\;\cdot \;(2/5)\;=\;0\;\land

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

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines

/-- The triad $\{a_{(0,1)}, a_{(1,-2)}, a_{(1,-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/5 : ℝ) * (-1/4) + (1/2 : ℝ) * (2/5) = 0 ∧
    (-3/20 : ℝ) + (-1/4) + (2/5) = 0 := by
  constructor <;> norm_num

What remains after the cancellation 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 L120–125

Namespace Notebook.NSB2

The energy identity for the compiled field.

Statement

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

\;(\sum \;\text{i},\;2\;\cdot \;(!\text{[}(1\;/\;1\;:\;\mathbb{R} ),\;(1\;/\;4\;:\;\mathbb{R} ),\;(1\;/\;5\;:\;\mathbb{R} ),\;(1\;/\;2\;:\;\mathbb{R} ),\;(1\;/\;1\;:\;\mathbb{R} ),\;(1\;/\;2\;:\;\mathbb{R} ),\;(1\;/\;5\;:\;\mathbb{R} ),\;(1\;/\;8\;:\;\mathbb{R} ),\;(1\;/\;5\;:\;\mathbb{R} ),\;(1\;/\;4\;:\;\mathbb{R} ),\;(1\;/\;5\;:\;\mathbb{R} ),\;(1\;/\;8\;:\;\mathbb{R} )\text{]}\;:\;\text{Fin}\;12\;\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\;/\;50\;:\;\mathbb{R} )\;\cdot \;(\text{x}\;0\;\cdot \;\text{x}\;0\;+\;\text{x}\;1\;\cdot \;\text{x}\;1\;+\;\text{x}\;2\;\cdot \;\text{x}\;2\;+\;\text{x}\;3\;\cdot \;\text{x}\;3\;+\;\text{x}\;4\;\cdot \;\text{x}\;4\;+\;\text{x}\;5\;\cdot \;\text{x}\;5\;+\;\text{x}\;6\;\cdot \;\text{x}\;6\;+\;\text{x}\;7\;\cdot \;\text{x}\;7\;+\;\text{x}\;8\;\cdot \;\text{x}\;8\;+\;\text{x}\;9\;\cdot \;\text{x}\;9\;+\;\text{x}\;10\;\cdot \;\text{x}\;10\;+\;\text{x}\;11\;\cdot \;\text{x}\;11)\;+\;(1\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;5

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines

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

Turn the identity into a trapping ball

Energy decreases above

625/2

. The ball

E \le 313

therefore traps any trajectory starting inside it, including the all-ones start.2 Kernel checked 2 As recorded

As in T3 (NS_T3.lean), $Z \ge E$ and the forcing acts on one mode, so the energy identity gives $2\nu(f^2/(8\nu^2) - E) - E' \ge 0$ with an explicit sum-of-squares certificate, checked below for this member's field. So $E$ decreases whenever it exceeds $f^2/(8\nu^2) = \tfrac{625}{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 $313$ , a whisker above.

Theorem `laminar_energy` Kernel checkedAs recorded L147–149

Namespace Notebook.NSB2

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

Statement

(1\;:\;\mathbb{R} )\;\text{\textasciicircum{}}\;2\;/\;(8\;\cdot \;(1/50)\;\text{\textasciicircum{}}\;2)\;=\;625/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/50) ^ 2) = 625/2 := by
  norm_num

Theorem `certificate_here` Kernel checkedAs recorded L151–155

Namespace Notebook.NSB2

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

Statement

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

\;\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\;/\;50\;:\;\mathbb{R} )\;\cdot \;(\text{x}\;5\;-\;25\;/\;1)\;\text{\textasciicircum{}}\;2\;+\;(3\;/\;100\;:\;\mathbb{R} )\;\cdot \;\text{x}\;1\;\text{\textasciicircum{}}\;2\;+\;(4\;/\;125\;:\;\mathbb{R} )\;\cdot \;\text{x}\;2\;\text{\textasciicircum{}}\;2\;+\;(1\;/\;50\;:\;\mathbb{R} )\;\cdot \;\text{x}\;3\;\text{\textasciicircum{}}\;2\;+\;(4\;/\;125\;:\;\mathbb{R} )\;\cdot \;\text{x}\;6\;\text{\textasciicircum{}}\;2\;+\;(7\;/\;200\;:\;\mathbb{R} )\;\cdot \;\text{x}\;7\;\text{\textasciicircum{}}\;2\;+\;(4\;/\;125\;:\;\mathbb{R} )\;\cdot \;\text{x}\;8\;\text{\textasciicircum{}}\;2\;+\;(3\;/\;100\;:\;\mathbb{R} )\;\cdot \;\text{x}\;9\;\text{\textasciicircum{}}\;2\;+\;(4\;/\;125\;:\;\mathbb{R} )\;\cdot \;\text{x}\;10\;\text{\textasciicircum{}}\;2\;+\;(7\;/\;200\;:\;\mathbb{R} )\;\cdot \;\text{x}\;11\;\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 12) :
    trapping.alpha * (trapping.inner - trapping.energy x) - trapping.rate (Gimle.Forseti.Nonlinear.field compiled) x =
      (1 / 50 : ℝ) * (x 5 - 25 / 1) ^ 2 + (3 / 100 : ℝ) * x 1 ^ 2 + (4 / 125 : ℝ) * x 2 ^ 2 + (1 / 50 : ℝ) * x 3 ^ 2 + (4 / 125 : ℝ) * x 6 ^ 2 + (7 / 200 : ℝ) * x 7 ^ 2 + (4 / 125 : ℝ) * x 8 ^ 2 + (3 / 100 : ℝ) * x 9 ^ 2 + (4 / 125 : ℝ) * x 10 ^ 2 + (7 / 200 : ℝ) * x 11 ^ 2 := by
  exact certificate x

Connect this system to the finite family

The compiled field is an instance of the family field. The theorem applies to nonzero modes with forcing on

(1,1)

and an initial state inside

E \le C

, where

C>625/2

.2 Kernel checked 2 As recorded

The family theorem (GalerkinNS.Family; derivation and discussion in NS_T3.lean) is instantiated here: Lean restates the library's check that this member's compiled field is the family field at its modes, and the theorem at $\nu = \tfrac{1}{50}$ , $f = 1$ — existence for all $t \ge$ any start time, uniqueness and $E \le C$ for every list of nonzero modes forced on $(1,1)$ and every $C > f^2/(8\nu^2)$ , provided the initial energy is at most $C$ .

Theorem `is_family_member` Kernel checkedAs recorded L172–176

Namespace Notebook.NSB2

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\;/\;50\;:\;\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 / 50 : ℝ) (1 / 1 : ℝ) modes forcedIndex := by
  exact field_eq_family

Theorem `every_member` Kernel checkedAs recorded L178–191

Namespace Notebook.NSB2

Every member. At $\nu = \tfrac{1}{50}$ , $f = 1$ : for any nonzero modes containing $(1,1)$ and any $C > \tfrac{625}{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\;/\;50\;:\;\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\;/\;50\;:\;\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\;/\;50\;:\;\mathbb{R} )\;1\;\text{k}\;\text{forced})\;\text{time}\;\text{x}_{0}\;\text{x}\;\to

\;\text{Nonlinear}.\text{Solves}\;(\text{Family}.\text{field}\;(1\;/\;50\;:\;\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\;/\;50\;:\;\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}{50}$, $f = 1$: for any nonzero modes
containing $(1,1)$ and any $C > \tfrac{625}{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 / 50 : ℝ) ^ 2) < C)
    (time : TimeDomain) (x₀ : Point n) (initial : Family.energy k x₀ ≤ C) :
    (∃ state, Nonlinear.Solves (Family.field (1 / 50 : ℝ) 1 k forced) time x₀ state) ∧
    (∀ x y : Signal n, Nonlinear.Solves (Family.field (1 / 50 : ℝ) 1 k forced) time x₀ x →
      Nonlinear.Solves (Family.field (1 / 50 : ℝ) 1 k forced) time x₀ y →
        Set.EqOn x y time.domain) ∧
    (∀ state, Nonlinear.Solves (Family.field (1 / 50 : ℝ) 1 k forced) time x₀ state →
      ∀ t ∈ time.domain, Family.energy k (state t) ≤ C) := by
  exact Family.trapped (1 / 50 : ℝ) 1 (by norm_num) k hk forced hf C hC time x₀ initial

Bound enstrophy and individual amplitudes

The enstrophy certificate gives

Z \le 626

for the stated start, hence

|a_k| \le 26

for every amplitude. Energy and enstrophy span the diagonal quadratic forms conserved by the nonlinear triad transfers; forcing and damping still change them along the full flow.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 and a bound on 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) = 625$ 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{626} < 26$ for all time, as amplitude_bound says of any state in the ball the decider establishes below.

Theorem `enstrophy_rate` Kernel checkedAs recorded L222–227

Namespace Notebook.NSB2

The enstrophy identity for the compiled field.

Statement

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

\;(\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{B2}.\text{compiled}\;\text{x}\;\text{i})\;=

\;-2\;\cdot \;(1\;/\;50\;:\;\mathbb{R} )\;\cdot \;(\text{x}\;0\;\cdot \;\text{x}\;0\;+\;(4\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;1\;\cdot \;\text{x}\;1\;+\;(5\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;2\;\cdot \;\text{x}\;2\;+\;(2\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;3\;\cdot \;\text{x}\;3\;+\;\text{x}\;4\;\cdot \;\text{x}\;4\;+\;(2\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;5\;\cdot \;\text{x}\;5\;+\;(5\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;6\;\cdot \;\text{x}\;6\;+\;(8\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;7\;\cdot \;\text{x}\;7\;+\;(5\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;8\;\cdot \;\text{x}\;8\;+\;(4\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;9\;\cdot \;\text{x}\;9\;+\;(5\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;10\;\cdot \;\text{x}\;10\;+\;(8\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;11\;\cdot \;\text{x}\;11)\;+\;2\;\cdot \;(1\;/\;1\;:\;\mathbb{R} )\;\cdot \;\text{x}\;5

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines

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

Theorem `laminar_enstrophy` Kernel checkedAs recorded L229–231

Namespace Notebook.NSB2

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

Statement

(1\;/\;1\;:\;\mathbb{R} )\;\text{\textasciicircum{}}\;2\;/\;(4\;\cdot \;(1\;/\;50)\;\text{\textasciicircum{}}\;2)\;=\;625\;/\;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 / 50) ^ 2) = 625 / 1 := by
  norm_num

Theorem `enstrophy_certificate_here` Kernel checkedAs recorded L233–237

Namespace Notebook.NSB2

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

Statement

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

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

\;(2\;\cdot \;(1\;/\;50)\;:\;\mathbb{R} )\;\cdot \;(\text{x}\;5\;-\;25\;/\;1)\;\text{\textasciicircum{}}\;2\;+\;(3\;/\;25\;:\;\mathbb{R} )\;\cdot \;\text{x}\;1\;\text{\textasciicircum{}}\;2\;+\;(4\;/\;25\;:\;\mathbb{R} )\;\cdot \;\text{x}\;2\;\text{\textasciicircum{}}\;2\;+\;(1\;/\;25\;:\;\mathbb{R} )\;\cdot \;\text{x}\;3\;\text{\textasciicircum{}}\;2\;+\;(4\;/\;25\;:\;\mathbb{R} )\;\cdot \;\text{x}\;6\;\text{\textasciicircum{}}\;2\;+\;(7\;/\;25\;:\;\mathbb{R} )\;\cdot \;\text{x}\;7\;\text{\textasciicircum{}}\;2\;+\;(4\;/\;25\;:\;\mathbb{R} )\;\cdot \;\text{x}\;8\;\text{\textasciicircum{}}\;2\;+\;(3\;/\;25\;:\;\mathbb{R} )\;\cdot \;\text{x}\;9\;\text{\textasciicircum{}}\;2\;+\;(4\;/\;25\;:\;\mathbb{R} )\;\cdot \;\text{x}\;10\;\text{\textasciicircum{}}\;2\;+\;(7\;/\;25\;:\;\mathbb{R} )\;\cdot \;\text{x}\;11\;\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 12) :
    Gimle.Forseti.Examples.GalerkinNS.B2.trappingZ.alpha * (Gimle.Forseti.Examples.GalerkinNS.B2.trappingZ.inner - Gimle.Forseti.Examples.GalerkinNS.B2.trappingZ.energy x) - Gimle.Forseti.Examples.GalerkinNS.B2.trappingZ.rate (Gimle.Forseti.Nonlinear.field Gimle.Forseti.Examples.GalerkinNS.B2.compiled) x =
      (2 * (1 / 50) : ℝ) * (x 5 - 25 / 1) ^ 2 + (3 / 25 : ℝ) * x 1 ^ 2 + (4 / 25 : ℝ) * x 2 ^ 2 + (1 / 25 : ℝ) * x 3 ^ 2 + (4 / 25 : ℝ) * x 6 ^ 2 + (7 / 25 : ℝ) * x 7 ^ 2 + (4 / 25 : ℝ) * x 8 ^ 2 + (3 / 25 : ℝ) * x 9 ^ 2 + (4 / 25 : ℝ) * x 10 ^ 2 + (7 / 25 : ℝ) * x 11 ^ 2 := by
  exact Gimle.Forseti.Examples.GalerkinNS.B2.certificateZ x

Theorem `amplitude_bound` Kernel checkedAs recorded L239–245

Namespace Notebook.NSB2

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

Statement

(\text{x}\;:\;\text{Point}\;12)\;(\text{h}\;:\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{B2}.\text{enstrophy}\;\text{x}\;\le \;626)\;(\text{i}\;:\;\text{Fin}\;12)\;:

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 626$. -/
theorem amplitude_bound (x : Point 12) (h : Gimle.Forseti.Examples.GalerkinNS.B2.enstrophy x ≤ 626) (i : Fin 12) :
    |x i| ≤ 26 := by
  rw [Gimle.Forseti.Examples.GalerkinNS.B2.enstrophy_eq_trappingZ, Gimle.Forseti.Examples.GalerkinNS.B2.enstrophy_eq_family] at h
  have := Gimle.Forseti.GalerkinNS.Family.mode_sq_le_enstrophy x i
  rw [abs_le]
  constructor <;> nlinarith

Classify the diagonal transfer invariants

Every diagonal weighting for which the triads are lossless is a combination of

1/\lambda

and

1

. This classifies diagonal quadratic forms for the nonlinear transfers, not all invariants of the full forced, damped system.1 Kernel checked 1 As recorded

The two trapping balls can be intersected to give $\{E \le C_E\} \cap \{Z \le C_Z\}$ . A closed trapping set containing the origin also contains the laminar equilibrium approached from that origin, so it cannot establish the requested energy bound $150$ .

Theorem `only_two` Kernel checkedAs recorded L261–298

Namespace Notebook.NSB2

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}\;12\;\to \;\mathbb{R} )

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

\;(\text{h1}\;:\;\text{w}\;0\;\cdot \;(-1\;/\;4)\;+\;\text{w}\;4\;\cdot \;(1\;/\;4)\;=\;0)

\;(\text{h2}\;:\;\text{w}\;0\;\cdot \;(1\;/\;4)\;+\;\text{w}\;4\;\cdot \;(-1\;/\;4)\;=\;0)

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

\;(\text{h4}\;:\;\text{w}\;0\;\cdot \;(-3\;/\;40)\;+\;\text{w}\;7\;\cdot \;(-4\;/\;5)\;+\;\text{w}\;8\;\cdot \;(7\;/\;8)\;=\;0)

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

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

\;(\text{h7}\;:\;\text{w}\;0\;\cdot \;(3\;/\;40)\;+\;\text{w}\;10\;\cdot \;(-7\;/\;8)\;+\;\text{w}\;11\;\cdot \;(4\;/\;5)\;=\;0)

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

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

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

\;(\text{h11}\;:\;\text{w}\;1\;\cdot \;(-1\;/\;4)\;+\;\text{w}\;9\;\cdot \;(1\;/\;4)\;=\;0)

\;(\text{h12}\;:\;\text{w}\;8\;\cdot \;(-1\;/\;10)\;+\;\text{w}\;10\;\cdot \;(1\;/\;10)\;=\;0)

\;(\text{h13}\;:\;\text{w}\;1\;\cdot \;(1\;/\;4)\;+\;\text{w}\;9\;\cdot \;(-1\;/\;4)\;=\;0)

\;(\text{h14}\;:\;\text{w}\;2\;\cdot \;(-7\;/\;8)\;+\;\text{w}\;4\;\cdot \;(3\;/\;40)\;+\;\text{w}\;7\;\cdot \;(4\;/\;5)\;=\;0)

\;(\text{h15}\;:\;\text{w}\;2\;\cdot \;(-9\;/\;20)\;+\;\text{w}\;8\;\cdot \;(9\;/\;20)\;=\;0)

\;(\text{h16}\;:\;\text{w}\;2\;\cdot \;(1\;/\;10)\;+\;\text{w}\;6\;\cdot \;(-1\;/\;10)\;=\;0)

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

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

\;(\text{h19}\;:\;\text{w}\;6\;\cdot \;(9\;/\;20)\;+\;\text{w}\;10\;\cdot \;(-9\;/\;20)\;=\;0)

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

\;(\text{h21}\;:\;\text{w}\;4\;\cdot \;(-3\;/\;40)\;+\;\text{w}\;6\;\cdot \;(7\;/\;8)\;+\;\text{w}\;11\;\cdot \;(-4\;/\;5)\;=\;0)\;:

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

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

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

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

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

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

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

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

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

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

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

\;\text{w}\;11\;=\;\alpha \;\cdot \;(1\;/\;8)\;+\;\beta

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 38 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 12 → ℝ)
    (h0 : w 0 * (-3 / 20) + w 2 * (-1 / 4) + w 3 * (2 / 5) = 0)
    (h1 : w 0 * (-1 / 4) + w 4 * (1 / 4) = 0)
    (h2 : w 0 * (1 / 4) + w 4 * (-1 / 4) = 0)
    (h3 : w 0 * (3 / 20) + w 5 * (-2 / 5) + w 6 * (1 / 4) = 0)
    (h4 : w 0 * (-3 / 40) + w 7 * (-4 / 5) + w 8 * (7 / 8) = 0)
    (h5 : w 0 * (-1 / 20) + w 8 * (-3 / 4) + w 9 * (4 / 5) = 0)
    (h6 : w 0 * (1 / 20) + w 9 * (-4 / 5) + w 10 * (3 / 4) = 0)
    (h7 : w 0 * (3 / 40) + w 10 * (-7 / 8) + w 11 * (4 / 5) = 0)
    (h8 : w 1 * (-4 / 5) + w 2 * (3 / 4) + w 4 * (1 / 20) = 0)
    (h9 : w 3 * (1 / 4) + w 5 * (-1 / 4) = 0)
    (h10 : w 1 * (4 / 5) + w 4 * (-1 / 20) + w 6 * (-3 / 4) = 0)
    (h11 : w 1 * (-1 / 4) + w 9 * (1 / 4) = 0)
    (h12 : w 8 * (-1 / 10) + w 10 * (1 / 10) = 0)
    (h13 : w 1 * (1 / 4) + w 9 * (-1 / 4) = 0)
    (h14 : w 2 * (-7 / 8) + w 4 * (3 / 40) + w 7 * (4 / 5) = 0)
    (h15 : w 2 * (-9 / 20) + w 8 * (9 / 20) = 0)
    (h16 : w 2 * (1 / 10) + w 6 * (-1 / 10) = 0)
    (h17 : w 3 * (-2 / 5) + w 4 * (3 / 20) + w 8 * (1 / 4) = 0)
    (h18 : w 3 * (-1 / 4) + w 5 * (1 / 4) = 0)
    (h19 : w 6 * (9 / 20) + w 10 * (-9 / 20) = 0)
    (h20 : w 4 * (-3 / 20) + w 5 * (2 / 5) + w 10 * (-1 / 4) = 0)
    (h21 : w 4 * (-3 / 40) + w 6 * (7 / 8) + w 11 * (-4 / 5) = 0) :
    ∃ α β : ℝ, w 0 = α * (1 / 1) + β ∧
      w 1 = α * (1 / 4) + β ∧
      w 2 = α * (1 / 5) + β ∧
      w 3 = α * (1 / 2) + β ∧
      w 4 = α * (1 / 1) + β ∧
      w 5 = α * (1 / 2) + β ∧
      w 6 = α * (1 / 5) + β ∧
      w 7 = α * (1 / 8) + β ∧
      w 8 = α * (1 / 5) + β ∧
      w 9 = α * (1 / 4) + β ∧
      w 10 = α * (1 / 5) + β ∧
      w 11 = α * (1 / 8) + β := by
  exact Gimle.Forseti.Examples.GalerkinNS.B2.only_two_diagonal w h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21

Inspect the decided trajectory contracts

The queries certify energy bound

313

, and enstrophy bound

626

, from the all-ones start at time zero. Energy bound

1

is refuted;

E \le 150

and

Z \le 600

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

Existence for all time, uniqueness and the ball come from the library's general trapping theorem, the same one that traps the Lorenz system (Lorenz.lean): clamp the field to a box, solve on every $[0, n]$ , glue, and fence with the strict decrease at the ball's boundary. Every claim below is decided against the compiled circuit.

Inspect the energy bound of 313

The query certifies existence, uniqueness and

0 \le E \le 313

for all time from the all-ones start.5 Kernel checked 5 As recorded

Decisionin_ball · trajectory · forsetiNever runL324–324

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

Not run yet.

namespace DecidedShared_eb9ca2106187

L326–326

Definition `forsetiTime` `: Gimle.Asgard.Dynamics.TimeDomain` L328–329

Namespace Notebook.NSB2.DecidedShared_eb9ca2106187

\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 12` L331–332

Namespace Notebook.NSB2.DecidedShared_eb9ca2106187

!\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{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} ),\;(((\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{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} ),\;(((\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{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} )\text{]}

Lean source · 2 lines

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

Definition `forsetiObservation` `: Fin 15` L334–334

Namespace Notebook.NSB2.DecidedShared_eb9ca2106187

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

Lean source · 1 line

def forsetiObservation : Fin 15 := ⟨12, by decide⟩

Definition `forsetiIdentities` `: Prop` L336–340

Namespace Notebook.NSB2.DecidedShared_eb9ca2106187

\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{B2}.\text{evolution}.\text{states}.\text{map}\;(\text{·}.\text{initialId})\;=\;\text{[}\texttt{"initial-a01"},\;\texttt{"initial-a02"},\;\texttt{"initial-a1m2"},\;\texttt{"initial-a1m1"},\;\texttt{"initial-a10"},\;\texttt{"initial-a11"},\;\texttt{"initial-a12"},\;\texttt{"initial-a2m2"},\;\texttt{"initial-a2m1"},\;\texttt{"initial-a20"},\;\texttt{"initial-a21"},\;\texttt{"initial-a22"}\text{]}\;\land

\;(\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{B2}.\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{B2}.\text{evolution}.\text{axis}.\text{id}\;=\;\texttt{"time"}

Lean source · 5 lines

def forsetiIdentities : Prop :=
  Gimle.Forseti.Examples.GalerkinNS.B2.evolution.states.map (·.initialId) = ["initial-a01", "initial-a02", "initial-a1m2", "initial-a1m1", "initial-a10", "initial-a11", "initial-a12", "initial-a2m2", "initial-a2m1", "initial-a20", "initial-a21", "initial-a22"] ∧
  (Gimle.Forseti.Examples.GalerkinNS.B2.body.observations.get forsetiObservation).port.id =
    "obs-e" ∧
  Gimle.Forseti.Examples.GalerkinNS.B2.evolution.axis.id = "time"

end DecidedShared_eb9ca2106187

L342–342

namespace Decided_in_ball

L344–344

open DecidedShared_eb9ca2106187

L346–346

Example `example (line 348)` Kernel checkedAs recorded L348–348

Namespace Notebook.NSB2.Decided_in_ball

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiTime Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiTime = @DecidedShared_eb9ca2106187.forsetiTime := rfl

Example `example (line 349)` Kernel checkedAs recorded L349–349

Namespace Notebook.NSB2.Decided_in_ball

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiInitial Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiInitial = @DecidedShared_eb9ca2106187.forsetiInitial := rfl

Example `example (line 350)` Kernel checkedAs recorded L350–350

Namespace Notebook.NSB2.Decided_in_ball

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiObservation
  Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiObservation

Assumptions: none

Lean source & proof · 1 line

example : @forsetiObservation = @DecidedShared_eb9ca2106187.forsetiObservation := rfl

Example `example (line 351)` Kernel checkedAs recorded L351–351

Namespace Notebook.NSB2.Decided_in_ball

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiIdentities Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiIdentities = @DecidedShared_eb9ca2106187.forsetiIdentities := rfl

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L353–354

Namespace Notebook.NSB2.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}\;(313)\;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 (313) 1))))))

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L356–359

Namespace Notebook.NSB2.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}\;(313)\;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 (313) 1)))))),
    forsetiPost⟩

Definition `forsetiContract` `: Prop` L361–366

Namespace Notebook.NSB2.Decided_in_ball

\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{B2}.\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.B2.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` L368–368

Namespace Notebook.NSB2.Decided_in_ball

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

Lean source · 1 line

def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem `in_ball` Kernel checkedAs recorded L370–411

Namespace Notebook.NSB2.Decided_in_ball

E is output 12 of the compiled circuit, the port obs-e; the input's initial wires (initial-a01, initial-a02, initial-a1m2, initial-a1m1, initial-a10, initial-a11, initial-a12, initial-a2m2, initial-a2m1, initial-a20, initial-a21, initial-a22) start at (1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) at time = 0. The trajectory decider proved it. Goal (trajectory): trajectory ns-b2 interpretation continuous-real obligation contract start time = 0 initial initial-a01 = 1, initial-a02 = 1, initial-a10 = 1, initial-a11 = 1, initial-a12 = 1, initial-a1m1 = 1, initial-a1m2 = 1, initial-a20 = 1, initial-a21 = 1, initial-a22 = 1, initial-a2m1 = 1, initial-a2m2 = 1 observe obs-e as E always : E >= 0 and E <= 313

Statement

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

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 42 lines

/-- E is output 12 of the compiled circuit, the port obs-e; the input's initial wires (initial-a01, initial-a02, initial-a1m2, initial-a1m1, initial-a10, initial-a11, initial-a12, initial-a2m2, initial-a2m1, initial-a20, initial-a21, initial-a22) start at (1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) at time = 0. The trajectory decider proved it. Goal (trajectory): trajectory ns-b2 interpretation continuous-real obligation contract start time = 0 initial initial-a01 = 1, initial-a02 = 1, initial-a10 = 1, initial-a11 = 1, initial-a12 = 1, initial-a1m1 = 1, initial-a1m2 = 1, initial-a20 = 1, initial-a21 = 1, initial-a22 = 1, initial-a2m1 = 1, initial-a2m2 = 1 observe obs-e as E always : E >= 0 and E <= 313 -/
theorem in_ball :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.B2.observed
    have time : Gimle.Asgard.Dynamics.TimeDomain := ⟨"time", 0⟩
    ∀ u : Gimle.Asgard.Dynamics.Signal (0 + 12),
      Gimle.Asgard.Dynamics.signalRight u 0 = ![1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] →
      (∃ y : Gimle.Asgard.Dynamics.Signal 15, circuit.Rel time u y) ∧
      (∀ y y' : Gimle.Asgard.Dynamics.Signal 15, circuit.Rel time u y → circuit.Rel time u y' →
        ∀ t ≥ 0, y t = y' t) ∧
      (∀ y : Gimle.Asgard.Dynamics.Signal 15, circuit.Rel time u y →
        ∀ t ≥ 0, have E := y t 12; E ≥ 0 ∧ E ≤ 313) := by
  have root : forsetiRoot := by
    unfold forsetiRoot forsetiIdentities forsetiContract
    refine ⟨⟨by decide, by decide, by decide⟩, ?_⟩
    have time : forsetiTime = Gimle.Forseti.Examples.GalerkinNS.B2.evolution.time := by simp [forsetiTime, Gimle.Asgard.Model.Evolution.time, Gimle.Forseti.Examples.GalerkinNS.B2.evolution] <;> norm_num [Rat.mkRat_eq_div]
    have init : forsetiInitial = Gimle.Forseti.Examples.GalerkinNS.B2.compiled.initial := by rw [Gimle.Forseti.Examples.GalerkinNS.B2.initial_eq]; funext i; fin_cases i <;> norm_num [forsetiInitial, Rat.mkRat_eq_div]
    have obs : forsetiObservation = Gimle.Forseti.Examples.GalerkinNS.B2.energyIndex := rfl
    rw [time, init, obs]
    refine Gimle.Forseti.Trajectory.Contract.consequence Gimle.Forseti.Examples.GalerkinNS.B2.energy_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 (313) 1) : ℚ) : ℝ) = 313 := 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 initial energy is

91/20>1

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

end Decided_in_ball

L421–421

Decisionbelow_one · trajectory · forsetiNever runL424–424

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

Not run yet.

namespace Decided_below_one

L426–426

open DecidedShared_eb9ca2106187

L428–428

Example `example (line 430)` Kernel checkedAs recorded L430–430

Namespace Notebook.NSB2.Decided_below_one

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiTime Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiTime = @DecidedShared_eb9ca2106187.forsetiTime := rfl

Example `example (line 431)` Kernel checkedAs recorded L431–431

Namespace Notebook.NSB2.Decided_below_one

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiInitial Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiInitial = @DecidedShared_eb9ca2106187.forsetiInitial := rfl

Example `example (line 432)` Kernel checkedAs recorded L432–432

Namespace Notebook.NSB2.Decided_below_one

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiObservation
  Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiObservation

Assumptions: none

Lean source & proof · 1 line

example : @forsetiObservation = @DecidedShared_eb9ca2106187.forsetiObservation := rfl

Example `example (line 433)` Kernel checkedAs recorded L433–433

Namespace Notebook.NSB2.Decided_below_one

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiIdentities Notebook.NSB2.DecidedShared_eb9ca2106187.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiIdentities = @DecidedShared_eb9ca2106187.forsetiIdentities := rfl

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L435–436

Namespace Notebook.NSB2.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` L438–443

Namespace Notebook.NSB2.Decided_below_one

\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{B2}.\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.B2.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` L445–445

Namespace Notebook.NSB2.Decided_below_one

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

Lean source · 1 line

def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem `below_one` Contains sorryAs recorded L447–458

Namespace Notebook.NSB2.Decided_below_one

E is output 12 of the compiled circuit, the port obs-e; the input's initial wires (initial-a01, initial-a02, initial-a1m2, initial-a1m1, initial-a10, initial-a11, initial-a12, initial-a2m2, initial-a2m1, initial-a20, initial-a21, initial-a22) start at (1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) at time = 0. The trajectory decider refuted it. Goal (trajectory): trajectory ns-b2 interpretation continuous-real obligation contract start time = 0 initial initial-a01 = 1, initial-a02 = 1, initial-a10 = 1, initial-a11 = 1, initial-a12 = 1, initial-a1m1 = 1, initial-a1m2 = 1, initial-a20 = 1, initial-a21 = 1, initial-a22 = 1, initial-a2m1 = 1, initial-a2m2 = 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 12 of the compiled circuit, the port obs-e; the input's initial wires (initial-a01, initial-a02, initial-a1m2, initial-a1m1, initial-a10, initial-a11, initial-a12, initial-a2m2, initial-a2m1, initial-a20, initial-a21, initial-a22) start at (1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) at time = 0. The trajectory decider refuted it. Goal (trajectory): trajectory ns-b2 interpretation continuous-real obligation contract start time = 0 initial initial-a01 = 1, initial-a02 = 1, initial-a10 = 1, initial-a11 = 1, initial-a12 = 1, initial-a1m1 = 1, initial-a1m2 = 1, initial-a20 = 1, initial-a21 = 1, initial-a22 = 1, initial-a2m1 = 1, initial-a2m2 = 1 observe obs-e as E always : E <= 1 -/
theorem below_one :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.B2.observed
    have time : Gimle.Asgard.Dynamics.TimeDomain := ⟨"time", 0⟩
    ∀ u : Gimle.Asgard.Dynamics.Signal (0 + 12),
      Gimle.Asgard.Dynamics.signalRight u 0 = ![1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] →
      (∃ y : Gimle.Asgard.Dynamics.Signal 15, circuit.Rel time u y) ∧
      (∀ y y' : Gimle.Asgard.Dynamics.Signal 15, circuit.Rel time u y → circuit.Rel time u y' →
        ∀ t ≥ 0, y t = y' t) ∧
      (∀ y : Gimle.Asgard.Dynamics.Signal 15, circuit.Rel time u y →
        ∀ t ≥ 0, have E := y t 12; E ≤ 1) := by
  sorry

Compare unresolved energy with certified enstrophy

The request

E \le 150

remains unknown. The next request certifies existence, uniqueness and

0 \le Z \le 626

from the stated start, supporting the amplitude bound above. The later request

Z \le 600

also remains unknown.5 Kernel checked 5 As recorded

end Decided_below_one

L470–470

Decisionbelow_150 · trajectory · forsetiNever runL473–473

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

Not run yet.

Decisionin_enstrophy_ball · trajectory · forsetiNever runL475–475

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

Not run yet.

namespace DecidedShared_2983651b73e2

L477–477

Definition `forsetiTime` `: Gimle.Asgard.Dynamics.TimeDomain` L479–480

Namespace Notebook.NSB2.DecidedShared_2983651b73e2

\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 12` L482–483

Namespace Notebook.NSB2.DecidedShared_2983651b73e2

!\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{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} ),\;(((\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{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} ),\;(((\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{mkRat}\;(1)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} )\text{]}

Lean source · 2 lines

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

Definition `forsetiObservation` `: Fin 15` L485–485

Namespace Notebook.NSB2.DecidedShared_2983651b73e2

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

Lean source · 1 line

def forsetiObservation : Fin 15 := ⟨13, by decide⟩

Definition `forsetiIdentities` `: Prop` L487–491

Namespace Notebook.NSB2.DecidedShared_2983651b73e2

\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{B2}.\text{evolution}.\text{states}.\text{map}\;(\text{·}.\text{initialId})\;=\;\text{[}\texttt{"initial-a01"},\;\texttt{"initial-a02"},\;\texttt{"initial-a1m2"},\;\texttt{"initial-a1m1"},\;\texttt{"initial-a10"},\;\texttt{"initial-a11"},\;\texttt{"initial-a12"},\;\texttt{"initial-a2m2"},\;\texttt{"initial-a2m1"},\;\texttt{"initial-a20"},\;\texttt{"initial-a21"},\;\texttt{"initial-a22"}\text{]}\;\land

\;(\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{B2}.\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{B2}.\text{evolution}.\text{axis}.\text{id}\;=\;\texttt{"time"}

Lean source · 5 lines

def forsetiIdentities : Prop :=
  Gimle.Forseti.Examples.GalerkinNS.B2.evolution.states.map (·.initialId) = ["initial-a01", "initial-a02", "initial-a1m2", "initial-a1m1", "initial-a10", "initial-a11", "initial-a12", "initial-a2m2", "initial-a2m1", "initial-a20", "initial-a21", "initial-a22"] ∧
  (Gimle.Forseti.Examples.GalerkinNS.B2.body.observations.get forsetiObservation).port.id =
    "obs-z" ∧
  Gimle.Forseti.Examples.GalerkinNS.B2.evolution.axis.id = "time"

end DecidedShared_2983651b73e2

L493–493

namespace Decided_in_enstrophy_ball

L495–495

open DecidedShared_2983651b73e2

L497–497

Example `example (line 499)` Kernel checkedAs recorded L499–499

Namespace Notebook.NSB2.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_2983651b73e2.forsetiTime Notebook.NSB2.DecidedShared_2983651b73e2.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiTime = @DecidedShared_2983651b73e2.forsetiTime := rfl

Example `example (line 500)` Kernel checkedAs recorded L500–500

Namespace Notebook.NSB2.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_2983651b73e2.forsetiInitial Notebook.NSB2.DecidedShared_2983651b73e2.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiInitial = @DecidedShared_2983651b73e2.forsetiInitial := rfl

Example `example (line 501)` Kernel checkedAs recorded L501–501

Namespace Notebook.NSB2.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_2983651b73e2.forsetiObservation
  Notebook.NSB2.DecidedShared_2983651b73e2.forsetiObservation

Assumptions: none

Lean source & proof · 1 line

example : @forsetiObservation = @DecidedShared_2983651b73e2.forsetiObservation := rfl

Example `example (line 502)` Kernel checkedAs recorded L502–502

Namespace Notebook.NSB2.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it

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

Kernel form, without notation

Eq Notebook.NSB2.DecidedShared_2983651b73e2.forsetiIdentities Notebook.NSB2.DecidedShared_2983651b73e2.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line

example : @forsetiIdentities = @DecidedShared_2983651b73e2.forsetiIdentities := rfl

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L504–505

Namespace Notebook.NSB2.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}\;(626)\;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 (626) 1))))))

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L507–510

Namespace Notebook.NSB2.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}\;(626)\;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 (626) 1)))))),
    forsetiPost⟩

Definition `forsetiContract` `: Prop` L512–517

Namespace Notebook.NSB2.Decided_in_enstrophy_ball

\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{B2}.\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.B2.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.NSB2.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 L521–562

Namespace Notebook.NSB2.Decided_in_enstrophy_ball

Z is output 13 of the compiled circuit, the port obs-z; the input's initial wires (initial-a01, initial-a02, initial-a1m2, initial-a1m1, initial-a10, initial-a11, initial-a12, initial-a2m2, initial-a2m1, initial-a20, initial-a21, initial-a22) start at (1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) at time = 0. The trajectory decider proved it. Goal (trajectory): trajectory ns-b2 interpretation continuous-real obligation contract start time = 0 initial initial-a01 = 1, initial-a02 = 1, initial-a10 = 1, initial-a11 = 1, initial-a12 = 1, initial-a1m1 = 1, initial-a1m2 = 1, initial-a20 = 1, initial-a21 = 1, initial-a22 = 1, initial-a2m1 = 1, initial-a2m2 = 1 observe obs-z as Z always : Z >= 0 and Z <= 626

Statement

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

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 42 lines

/-- Z is output 13 of the compiled circuit, the port obs-z; the input's initial wires (initial-a01, initial-a02, initial-a1m2, initial-a1m1, initial-a10, initial-a11, initial-a12, initial-a2m2, initial-a2m1, initial-a20, initial-a21, initial-a22) start at (1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) at time = 0. The trajectory decider proved it. Goal (trajectory): trajectory ns-b2 interpretation continuous-real obligation contract start time = 0 initial initial-a01 = 1, initial-a02 = 1, initial-a10 = 1, initial-a11 = 1, initial-a12 = 1, initial-a1m1 = 1, initial-a1m2 = 1, initial-a20 = 1, initial-a21 = 1, initial-a22 = 1, initial-a2m1 = 1, initial-a2m2 = 1 observe obs-z as Z always : Z >= 0 and Z <= 626 -/
theorem in_enstrophy_ball :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.B2.observed
    have time : Gimle.Asgard.Dynamics.TimeDomain := ⟨"time", 0⟩
    ∀ u : Gimle.Asgard.Dynamics.Signal (0 + 12),
      Gimle.Asgard.Dynamics.signalRight u 0 = ![1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] →
      (∃ y : Gimle.Asgard.Dynamics.Signal 15, circuit.Rel time u y) ∧
      (∀ y y' : Gimle.Asgard.Dynamics.Signal 15, circuit.Rel time u y → circuit.Rel time u y' →
        ∀ t ≥ 0, y t = y' t) ∧
      (∀ y : Gimle.Asgard.Dynamics.Signal 15, circuit.Rel time u y →
        ∀ t ≥ 0, have Z := y t 13; Z ≥ 0 ∧ Z ≤ 626) := by
  have root : forsetiRoot := by
    unfold forsetiRoot forsetiIdentities forsetiContract
    refine ⟨⟨by decide, by decide, by decide⟩, ?_⟩
    have time : forsetiTime = Gimle.Forseti.Examples.GalerkinNS.B2.evolution.time := by simp [forsetiTime, Gimle.Asgard.Model.Evolution.time, Gimle.Forseti.Examples.GalerkinNS.B2.evolution] <;> norm_num [Rat.mkRat_eq_div]
    have init : forsetiInitial = Gimle.Forseti.Examples.GalerkinNS.B2.compiled.initial := by rw [Gimle.Forseti.Examples.GalerkinNS.B2.initial_eq]; funext i; fin_cases i <;> norm_num [forsetiInitial, Rat.mkRat_eq_div]
    have obs : forsetiObservation = Gimle.Forseti.Examples.GalerkinNS.B2.enstrophyIndex := rfl
    rw [time, init, obs]
    refine Gimle.Forseti.Trajectory.Contract.consequence Gimle.Forseti.Examples.GalerkinNS.B2.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 (626) 1) : ℚ) : ℝ) = 626 := 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⟩

Scope and unresolved bounds

These are statements about the compiled finite ODE at the stated viscosity, forcing and initial state. They establish no approximation or limiting theorem for the Navier–Stokes PDE. Simulations guide the questions but are not proofs. The requests $E \le 150$ and $Z \le 600$ remain unknown; their absence from claim counts does not make them settled.

end Decided_in_enstrophy_ball

L575–575

Decisionenstrophy_below_600 · trajectory · forsetiNever runL578–578

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

Not run yet.

#print axioms triad_lossless

L580–580

#print axioms energy_rate

L581–581

#print axioms laminar_energy

L582–582

#print axioms certificate_here

L583–583

#print axioms is_family_member

L584–584

#print axioms every_member

L585–585

#print axioms enstrophy_rate

L586–586

#print axioms laminar_enstrophy

L587–587

#print axioms enstrophy_certificate_here

L588–588

#print axioms amplitude_bound

L589–589

#print axioms only_two

L590–590

end Notebook.NSB2

L592–592

The equations

The system, compiled

model diagram Gimle.Forseti.Examples.GalerkinNS.B2.compiled L69–69

What a simulation shows

Derive the reusable energy bound

Cancel the triad energy transfers

Theorem triad_lossless Kernel checkedAs recorded L105–110

Theorem energy_rate Kernel checkedAs recorded L120–125

Turn the identity into a trapping ball

Theorem laminar_energy Kernel checkedAs recorded L147–149

Theorem certificate_here Kernel checkedAs recorded L151–155

Connect this system to the finite family

Theorem is_family_member Kernel checkedAs recorded L172–176

Theorem every_member Kernel checkedAs recorded L178–191

Bound enstrophy and individual amplitudes

Derive the enstrophy certificate

Theorem enstrophy_rate Kernel checkedAs recorded L222–227

Theorem laminar_enstrophy Kernel checkedAs recorded L229–231

Theorem enstrophy_certificate_here Kernel checkedAs recorded L233–237

Theorem amplitude_bound Kernel checkedAs recorded L239–245

Classify the diagonal transfer invariants

Theorem only_two Kernel checkedAs recorded L261–298

Inspect the decided trajectory contracts

Inspect the energy bound of 313

Definition forsetiTime : Gimle.Asgard.Dynamics.TimeDomain L328–329

Definition forsetiInitial : Gimle.Asgard.Point 12 L331–332

Definition forsetiObservation : Fin 15 L334–334

Definition forsetiIdentities : Prop L336–340

Example example (line 348) Kernel checkedAs recorded L348–348

Example example (line 349) Kernel checkedAs recorded L349–349

Example example (line 350) Kernel checkedAs recorded L350–350

Example example (line 351) Kernel checkedAs recorded L351–351

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L353–354

Definition forsetiLeaf : Gimle.Forseti.Syntax.Goal L356–359

Definition forsetiContract : Prop L361–366

Definition forsetiRoot : Prop L368–368

Theorem in_ball Kernel checkedAs recorded L370–411

Inspect the refuted energy bound of one

Example example (line 430) Kernel checkedAs recorded L430–430

Example example (line 431) Kernel checkedAs recorded L431–431

Example example (line 432) Kernel checkedAs recorded L432–432

Example example (line 433) Kernel checkedAs recorded L433–433

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L435–436

Definition forsetiContract : Prop L438–443

Definition forsetiRoot : Prop L445–445

Theorem below_one Contains sorryAs recorded L447–458

Compare unresolved energy with certified enstrophy

Definition forsetiTime : Gimle.Asgard.Dynamics.TimeDomain L479–480

Definition forsetiInitial : Gimle.Asgard.Point 12 L482–483

Definition forsetiObservation : Fin 15 L485–485

Definition forsetiIdentities : Prop L487–491

Example example (line 499) Kernel checkedAs recorded L499–499

Example example (line 500) Kernel checkedAs recorded L500–500

Example example (line 501) Kernel checkedAs recorded L501–501

Example example (line 502) Kernel checkedAs recorded L502–502

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L504–505

Definition forsetiLeaf : Gimle.Forseti.Syntax.Goal L507–510

Definition forsetiContract : Prop L512–517

Definition forsetiRoot : Prop L519–519

Theorem in_enstrophy_ball Kernel checkedAs recorded L521–562

Scope and unresolved bounds

model diagram `Gimle.Forseti.Examples.GalerkinNS.B2.compiled` L69–69

Theorem `triad_lossless` Kernel checkedAs recorded L105–110

Theorem `energy_rate` Kernel checkedAs recorded L120–125

Theorem `laminar_energy` Kernel checkedAs recorded L147–149

Theorem `certificate_here` Kernel checkedAs recorded L151–155

Theorem `is_family_member` Kernel checkedAs recorded L172–176

Theorem `every_member` Kernel checkedAs recorded L178–191

Theorem `enstrophy_rate` Kernel checkedAs recorded L222–227

Theorem `laminar_enstrophy` Kernel checkedAs recorded L229–231

Theorem `enstrophy_certificate_here` Kernel checkedAs recorded L233–237

Theorem `amplitude_bound` Kernel checkedAs recorded L239–245

Theorem `only_two` Kernel checkedAs recorded L261–298

Definition `forsetiTime` `: Gimle.Asgard.Dynamics.TimeDomain` L328–329

Definition `forsetiInitial` `: Gimle.Asgard.Point 12` L331–332

Definition `forsetiObservation` `: Fin 15` L334–334

Definition `forsetiIdentities` `: Prop` L336–340

Example `example (line 348)` Kernel checkedAs recorded L348–348

Example `example (line 349)` Kernel checkedAs recorded L349–349

Example `example (line 350)` Kernel checkedAs recorded L350–350

Example `example (line 351)` Kernel checkedAs recorded L351–351

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L353–354

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L356–359

Definition `forsetiContract` `: Prop` L361–366

Definition `forsetiRoot` `: Prop` L368–368

Theorem `in_ball` Kernel checkedAs recorded L370–411

Example `example (line 430)` Kernel checkedAs recorded L430–430

Example `example (line 431)` Kernel checkedAs recorded L431–431

Example `example (line 432)` Kernel checkedAs recorded L432–432

Example `example (line 433)` Kernel checkedAs recorded L433–433

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L435–436

Definition `forsetiContract` `: Prop` L438–443

Definition `forsetiRoot` `: Prop` L445–445

Theorem `below_one` Contains sorryAs recorded L447–458

Definition `forsetiTime` `: Gimle.Asgard.Dynamics.TimeDomain` L479–480

Definition `forsetiInitial` `: Gimle.Asgard.Point 12` L482–483

Definition `forsetiObservation` `: Fin 15` L485–485

Definition `forsetiIdentities` `: Prop` L487–491

Example `example (line 499)` Kernel checkedAs recorded L499–499

Example `example (line 500)` Kernel checkedAs recorded L500–500

Example `example (line 501)` Kernel checkedAs recorded L501–501

Example `example (line 502)` Kernel checkedAs recorded L502–502

Definition `forsetiPost` `: Gimle.Forseti.Syntax.Formula 1` L504–505

Definition `forsetiLeaf` `: Gimle.Forseti.Syntax.Goal` L507–510

Definition `forsetiContract` `: Prop` L512–517

Definition `forsetiRoot` `: Prop` L519–519

Theorem `in_enstrophy_ball` Kernel checkedAs recorded L521–562