A 3-mode truncation of Navier–Stokes at small forcing: the laminar line attracts

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

import Mathlib
L1–1
import Gimle.Forseti.Syntax.Certificate
L2–2
import Gimle.Forseti.Examples.GalerkinNS.T3S
L3–3

The same three cosine modes as NS_T3.lean, (1,0)(1, 0), (1,1)(1, 1), (2,1)(2, 1), with the same force f=1f = 1 on (1,1)(1, 1), but five times the viscosity: ν=12\nu = \tfrac12 instead of 110\tfrac{1}{10}. The Grashof-type number f/ν2f/\nu^2 drops from 100100 to 44, and the flow changes character: at ν=110\nu = \tfrac{1}{10} the laminar state is linearly unstable (numerically) and the simulated trajectory settles elsewhere, so the energy bounds below the laminar level stay undecided; here the laminar state attracts, and that is a theorem — for every member of the family below a threshold, proved once, restated and checked for this member, whose balls the decider settles against its compiled circuit.

The equations

Writing aka_k for the amplitude of cos⁡(k⋅x)\cos(k \cdot x) and λk=∣k∣2\lambda_k = |k|^2:

a10′=−12a10−320a11a21a11′=1−a11+25a10a21a21′=−52a21−14a10a11\begin{aligned} a_{10}' &= - \tfrac12 a_{10} - \tfrac{3}{20} a_{11} a_{21} \\ a_{11}' &= 1 - a_{11} + \tfrac{2}{5} a_{10} a_{21} \\ a_{21}' &= - \tfrac52 a_{21} - \tfrac14 a_{10} a_{11} \end{aligned}

The laminar state has only the forced mode excited, a11=f/(2ν)=1a_{11} = f/(2\nu) = 1, with energy E=f2/(8ν2)=12E = f^2/(8\nu^2) = \tfrac12 and enstrophy Z=f2/(4ν2)=1Z = f^2/(4\nu^2) = 1. Numerically its Jacobian has eigenvalues −0.48-0.48, −1-1, −2.52-2.52 — stable — but nothing below reads that; the theorem is global and needs no linearisation.

Proved. From the start where every amplitude is 11, a solution exists for all t≥0t \ge 0 and is unique; its energy stays in [0,1710][0, \tfrac{17}{10}], its enstrophy in [0,4][0, 4], and its unforced energy R=a102/λ10+a212/λ21R = a_{10}^2/\lambda_{10} + a_{21}^2/\lambda_{21} never exceeds its start value 65\tfrac65 — all three decided by the trajectory decider from named Lean contracts. And RR decays: R(t)≤65e−t/5R(t) \le \tfrac65 e^{-t/5} for all t≥0t \ge 0, a Lean theorem on this page, restated from the member's.

Refuted. R≤1R \le 1 for all t≥0t \ge 0: false at the start, where R=65R = \tfrac65. The decay says it is true soon after, but the claim is about every time, and the decider refutes it at t=0t = 0.

Not claimed. Anything about the Navier–Stokes *equations*; anything about where a11a_{11} ends up (the theorem bounds the unforced modes, and the forced one only through the enstrophy ball); any rate better than 15\tfrac15, which the crude coupling bound gives, where the linearisation (slowest eigenvalue −0.48-0.48, so R∼e−0.96tR \sim e^{-0.96 t}) suggests about 11. "Attracts" here is an invariant family and a rate, not a status at a finite time: the deciders state what holds for all t≥0t \ge 0.

The system, compiled

namespace Notebook.NSLaminar
L53–53
open Gimle.Asgard Gimle.Asgard.Dynamics Gimle.Forseti Gimle.Forseti.Trajectory
L54–54

model diagram Gimle.Forseti.Examples.GalerkinNS.T3S.compiled L56–56

Continuous modelt · start 0Vector fieldIntegrate · tda10/dt = (((-1/2) × a10) + (((-3/20) × a11) × a21))∫ → a10a10(0) = 1a10a10da11/dt = ((1 + ((-1) × a11)) + ((2/5 × a10) × a21))∫ → a11a11(0) = 1a11a11da21/dt = (((-5/2) × a21) + (((-1/4) × a10) × a11))∫ → a21a21(0) = 1a21a21
Observations a10 a11 a21 E Z R
Evidence · not proofsimulate Gimle.Forseti.Examples.GalerkinNS.T3S.compiled · forsetiNever runL57–57

Not run yet.

What a simulation shows

Drawn as evidence, never a status: the unforced amplitudes a10a_{10} and a21a_{21} fall into the origin of their plane along one direction, without circling, while a11a_{11} settles at 11. The theorems below say why, and say it for all time.

Why only the forced mode feeds the rest

Each mode stores ak2/λka_k^2/\lambda_k and each triad routes energy losslessly, as in NS_T3.lean. Sum the storage identities over the two unforced modes only: the triad's two flows into them do not cancel on their own — they cancel against the flow into a11a_{11}, which the sum leaves out — so what remains is exactly the forced mode's own cubic term, with the opposite sign:

R′=−2ν (a102+a212)−a11⋅25 a10a21.R' = -2\nu\,(a_{10}^2 + a_{21}^2) - a_{11} \cdot \tfrac25\, a_{10} a_{21}.

That is the whole coupling between the forced mode and the rest, and it is bounded: ∣25a10a21∣≤15(a102+a212)|\tfrac25 a_{10} a_{21}| \le \tfrac15 (a_{10}^2 + a_{21}^2), and ∣a11∣≤2|a_{11}| \le 2 on the enstrophy ball Z≤4Z \le 4 the start lies in. So R′≤−(2ν−25⋅2) (a102+a212)=−15(a102+a212)≤−15RR' \le -(2\nu - \tfrac25 \cdot 2)\,(a_{10}^2 + a_{21}^2) = -\tfrac15 (a_{10}^2 + a_{21}^2) \le -\tfrac15 R, and RR decays at rate at least 15\tfrac15. The threshold is Kr<2νK r < 2\nu with K=25K = \tfrac25 the forced mode's coupling sum and rr the enstrophy ball's radius; at ν=110\nu = \tfrac{1}{10} the ball must lie above the laminar enstrophy f2/(4ν2)=25f^2/(4\nu^2) = 25, so r>5r > 5 and Kr>2>15=2νK r > 2 > \tfrac15 = 2\nu; the generated member takes r=6r = 6, where Kr=125K r = \tfrac{12}{5}: above the threshold, and nothing of this kind is claimed there.

Theorem rest_rate Kernel checkedAs recorded L89–96

Namespace Notebook.NSLaminar

The unforced energy identity for the compiled field.

Statement
(x  :  Point  3)  :(\text{x}\;:\;\text{Point}\;3)\;:  (∑  i,  2  ⋅  (![(1  /  1  :  R),  0,  (1  /  5  :  R)]  :  Fin  3  →  R)  i  ⋅  x  i  ⋅\;(\sum \;\text{i},\;2\;\cdot \;(!\text{[}(1\;/\;1\;:\;\mathbb{R} ),\;0,\;(1\;/\;5\;:\;\mathbb{R} )\text{]}\;:\;\text{Fin}\;3\;\to \;\mathbb{R} )\;\text{i}\;\cdot \;\text{x}\;\text{i}\;\cdot   Gimle.Forseti.Nonlinear.field  Gimle.Forseti.Examples.GalerkinNS.T3S.compiled  x  i)  =\;\text{Gimle}.\text{Forseti}.\text{Nonlinear}.\text{field}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{compiled}\;\text{x}\;\text{i})\;=  −2  ⋅  (1  /  2  :  R)  ⋅  (x  0  ⋅  x  0  +  x  2  ⋅  x  2)  −  x  1  ⋅  ((2  /  5  :  R)  ⋅  x  0  ⋅  x  2)\;-2\;\cdot \;(1\;/\;2\;:\;\mathbb{R} )\;\cdot \;(\text{x}\;0\;\cdot \;\text{x}\;0\;+\;\text{x}\;2\;\cdot \;\text{x}\;2)\;-\;\text{x}\;1\;\cdot \;((2\;/\;5\;:\;\mathbb{R} )\;\cdot \;\text{x}\;0\;\cdot \;\text{x}\;2)

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 8 lines
/-- The unforced energy identity for the compiled field. -/
theorem rest_rate (x : Point 3) :
    (∑ i, 2 * (![(1 / 1 : ℝ), 0, (1 / 5 : ℝ)] : Fin 3 → ℝ) i * x i *
        Gimle.Forseti.Nonlinear.field Gimle.Forseti.Examples.GalerkinNS.T3S.compiled x i) =
      -2 * (1 / 2 : ℝ) * (x 0 * x 0 + x 2 * x 2) - x 1 * ((2 / 5 : ℝ) * x 0 * x 2) := by
  rw [Gimle.Forseti.Examples.GalerkinNS.T3S.field_eq]
  simp [Gimle.Forseti.Examples.GalerkinNS.T3S.field, Fin.sum_univ_succ]
  ring

Theorem coupling_sum Kernel checkedAs recorded L98–102

Namespace Notebook.NSLaminar

The forced mode's coupling sum, K = 2/5.

Statement
Gimle.Forseti.GalerkinNS.Family.couplingSum  Gimle.Forseti.Examples.GalerkinNS.T3S.modes\text{Gimle}.\text{Forseti}.\text{GalerkinNS}.\text{Family}.\text{couplingSum}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{modes}  Gimle.Forseti.Examples.GalerkinNS.T3S.forcedIndex  =  2  /  5\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{forcedIndex}\;=\;2\;/\;5

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 5 lines
/-- The forced mode's coupling sum, `K = 2/5`. -/
theorem coupling_sum :
    Gimle.Forseti.GalerkinNS.Family.couplingSum Gimle.Forseti.Examples.GalerkinNS.T3S.modes
      Gimle.Forseti.Examples.GalerkinNS.T3S.forcedIndex = 2 / 5 := by
  exact Gimle.Forseti.Examples.GalerkinNS.T3S.couplingSum_eq

Theorem below_threshold Kernel checkedAs recorded L104–106

Namespace Notebook.NSLaminar

Below the threshold: 2ν − K r = 1 − (2/5)·2 = 1/5 > 0.

Statement
(0  :  R)  <  2  ⋅  (1  /  2)  −  2  /  5  ⋅  2(0\;:\;\mathbb{R} )\;<\;2\;\cdot \;(1\;/\;2)\;-\;2\;/\;5\;\cdot \;2

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 3 lines
/-- Below the threshold: `2ν − K r = 1 − (2/5)·2 = 1/5 > 0`. -/
theorem below_threshold : (0 : ℝ) < 2 * (1 / 2) - 2 / 5 * 2 := by
  norm_num

Theorem above_threshold_at_small_viscosity Kernel checkedAs recorded L108–111

Namespace Notebook.NSLaminar

The same modes at ν = 1/10 are above it: any ball above the laminar enstrophy 25 has r > 5; with the member's r = 6, 2ν − K r = 1/5 − 12/5 < 0.

Statement
(2  ⋅  (1  /  10  :  R)  −  2  /  5  ⋅  6)  <  0(2\;\cdot \;(1\;/\;10\;:\;\mathbb{R} )\;-\;2\;/\;5\;\cdot \;6)\;<\;0

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines
/-- The same modes at `ν = 1/10` are above it: any ball above the laminar
enstrophy `25` has `r > 5`; with the member's `r = 6`, `2ν − K r = 1/5 − 12/5 < 0`. -/
theorem above_threshold_at_small_viscosity : (2 * (1 / 10 : ℝ) - 2 / 5 * 6) < 0 := by
  norm_num

Theorem rest_decays Kernel checkedAs recorded L113–132

Namespace Notebook.NSLaminar

The unforced energy decays: along every realization of the compiled model, R(t) ≤ R(0) e^{−t/5}, with R(0) = 6/5.

Statement
(state  :  Signal  3)(\text{state}\;:\;\text{Signal}\;3)  (realized  :  Gimle.Forseti.Examples.GalerkinNS.T3S.compiled.Realizes  state)  :\;(\text{realized}\;:\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{compiled}.\text{Realizes}\;\text{state})\;:  ∀  t  ∈  Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.time.domain,\;\forall \;\text{t}\;\in \;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{evolution}.\text{time}.\text{domain},  Gimle.Forseti.Examples.GalerkinNS.T3S.rest  (state  t)  ≤\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{rest}\;(\text{state}\;\text{t})\;\le   6  /  5  ⋅  Real.exp  (−(1  /  5  :  R)  ⋅  t)\;6\;/\;5\;\cdot \;\text{Real}.\text{exp}\;(-(1\;/\;5\;:\;\mathbb{R} )\;\cdot \;\text{t})

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 20 lines
/-- **The unforced energy decays**: along every realization of the compiled
model, `R(t) ≤ R(0) e^{−t/5}`, with `R(0) = 6/5`. -/
theorem rest_decays (state : Signal 3)
    (realized : Gimle.Forseti.Examples.GalerkinNS.T3S.compiled.Realizes state) :
    ∀ t ∈ Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.time.domain,
      Gimle.Forseti.Examples.GalerkinNS.T3S.rest (state t) ≤
        6 / 5 * Real.exp (-(1 / 5 : ℝ) * t) := by
  intro t ht
  have h := Gimle.Forseti.Examples.GalerkinNS.T3S.rest_decays state realized t ht
  rw [Gimle.Forseti.Examples.GalerkinNS.T3S.couplingSum_eq] at h
  have start : Gimle.Forseti.Examples.GalerkinNS.T3S.rest
      Gimle.Forseti.Examples.GalerkinNS.T3S.compiled.initial = 6 / 5 := by
    rw [Gimle.Forseti.Examples.GalerkinNS.T3S.initial_eq]
    simp [Gimle.Forseti.Examples.GalerkinNS.T3S.rest, Matrix.cons_val]
    norm_num
  have zero : Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.time.start = 0 := by
    simp [Model.Evolution.time, Gimle.Forseti.Examples.GalerkinNS.T3S.evolution]
  rw [start, zero] at h
  convert h using 2
  norm_num

For every member

The theorem is the family's: for any nonzero modes containing (1,1)(1,1), any ν>0\nu > 0 and any r≥0r \ge 0 with r2r^2 above the laminar enstrophy f2/(4ν2)f^2/(4\nu^2) and Kr<2νK r < 2\nu, from any start with Z≤r2Z \le r^2 a solution exists for all t≥t \ge the start, is unique, keeps Z≤r2Z \le r^2 and has R(t)≤R(start) e−(2ν−Kr)(t−start)R(t) \le R(\text{start})\, e^{-(2\nu - K r)(t - \text{start})}. The member above is an instance.

Theorem every_member Kernel checkedAs recorded L145–158

Namespace Notebook.NSLaminar

Every member below the threshold.

Statement
{n  :  N}  (k  :  Fin  n  →  Gimle.Forseti.GalerkinNS.Family.Wave)\text{\{}\text{n}\;:\;\mathbb{N} \text{\}}\;(\text{k}\;:\;\text{Fin}\;\text{n}\;\to \;\text{Gimle}.\text{Forseti}.\text{GalerkinNS}.\text{Family}.\text{Wave})  (hk  :  ∀  i,  k  i  ≠  0)  (forced  :  Fin  n)  (hf  :  k  forced  =  (1,  1))  (ν  f  r  :  R)  (hν  :  0  <  ν)\;(\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))\;(\nu \;\text{f}\;\text{r}\;:\;\mathbb{R} )\;(\text{h}\nu \;:\;0\;<\;\nu )  (hr  :  0  ≤  r)  (hC  :  f  ^  2  /  (4  ⋅  ν  ^  2)  <  r  ^  2)\;(\text{hr}\;:\;0\;\le \;\text{r})\;(\text{hC}\;:\;\text{f}\;\text{\textasciicircum{}}\;2\;/\;(4\;\cdot \;\nu \;\text{\textasciicircum{}}\;2)\;<\;\text{r}\;\text{\textasciicircum{}}\;2)  (hγ  :  0  <  2  ⋅  ν  −  Gimle.Forseti.GalerkinNS.Family.couplingSum  k  forced  ⋅  r)\;(\text{h}\gamma \;:\;0\;<\;2\;\cdot \;\nu \;-\;\text{Gimle}.\text{Forseti}.\text{GalerkinNS}.\text{Family}.\text{couplingSum}\;\text{k}\;\text{forced}\;\cdot \;\text{r})  (time  :  TimeDomain)  (x0  :  Point  n)  (initial  :  Gimle.Forseti.GalerkinNS.Family.enstrophy  x0  ≤  r  ^  2)  :\;(\text{time}\;:\;\text{TimeDomain})\;(\text{x}_{0}\;:\;\text{Point}\;\text{n})\;(\text{initial}\;:\;\text{Gimle}.\text{Forseti}.\text{GalerkinNS}.\text{Family}.\text{enstrophy}\;\text{x}_{0}\;\le \;\text{r}\;\text{\textasciicircum{}}\;2)\;:  ∀  state,  Gimle.Forseti.Nonlinear.Solves  (Gimle.Forseti.GalerkinNS.Family.field  ν  f  k  forced)  time  x0  state  →\;\forall \;\text{state},\;\text{Gimle}.\text{Forseti}.\text{Nonlinear}.\text{Solves}\;(\text{Gimle}.\text{Forseti}.\text{GalerkinNS}.\text{Family}.\text{field}\;\nu \;\text{f}\;\text{k}\;\text{forced})\;\text{time}\;\text{x}_{0}\;\text{state}\;\to   ∀  t  ∈  time.domain,\;\forall \;\text{t}\;\in \;\text{time}.\text{domain},  Gimle.Forseti.GalerkinNS.Family.restEnergy  k  forced  (state  t)  ≤\;\text{Gimle}.\text{Forseti}.\text{GalerkinNS}.\text{Family}.\text{restEnergy}\;\text{k}\;\text{forced}\;(\text{state}\;\text{t})\;\le   Gimle.Forseti.GalerkinNS.Family.restEnergy  k  forced  x0  ⋅\;\text{Gimle}.\text{Forseti}.\text{GalerkinNS}.\text{Family}.\text{restEnergy}\;\text{k}\;\text{forced}\;\text{x}_{0}\;\cdot   Real.exp  (−(2  ⋅  ν  −  Gimle.Forseti.GalerkinNS.Family.couplingSum  k  forced  ⋅  r)  ⋅  (t  −  time.start))\;\text{Real}.\text{exp}\;(-(2\;\cdot \;\nu \;-\;\text{Gimle}.\text{Forseti}.\text{GalerkinNS}.\text{Family}.\text{couplingSum}\;\text{k}\;\text{forced}\;\cdot \;\text{r})\;\cdot \;(\text{t}\;-\;\text{time}.\text{start}))

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 14 lines
/-- **Every member below the threshold.** -/
theorem every_member {n : ℕ} (k : Fin n → Gimle.Forseti.GalerkinNS.Family.Wave)
    (hk : ∀ i, k i ≠ 0) (forced : Fin n) (hf : k forced = (1, 1)) (ν f r : ℝ) (hν : 0 < ν)
    (hr : 0 ≤ r) (hC : f ^ 2 / (4 * ν ^ 2) < r ^ 2)
    (hγ : 0 < 2 * ν - Gimle.Forseti.GalerkinNS.Family.couplingSum k forced * r)
    (time : TimeDomain) (x₀ : Point n) (initial : Gimle.Forseti.GalerkinNS.Family.enstrophy x₀ ≤ r ^ 2) :
    ∀ state, Gimle.Forseti.Nonlinear.Solves (Gimle.Forseti.GalerkinNS.Family.field ν f k forced) time x₀ state →
      ∀ t ∈ time.domain,
        Gimle.Forseti.GalerkinNS.Family.restEnergy k forced (state t) ≤
          Gimle.Forseti.GalerkinNS.Family.restEnergy k forced x₀ *
            Real.exp (-(2 * ν - Gimle.Forseti.GalerkinNS.Family.couplingSum k forced * r) * (t - time.start)) := by
  intro state h t ht
  exact ((Gimle.Forseti.GalerkinNS.Family.laminar_attracts ν f hν k hk forced hf r hr hC hγ
    time x₀ initial).2.2 state h t ht).2

The claims, decided

Every claim below is decided against the compiled circuit from a one-line goal: the enstrophy ball the decay is proved on, the energy ball at the start level, the unforced energy never above its start, and a bound below the start refuted at the start.

Decisionin_enstrophy_ball · trajectory · forsetiNever runL169–169
trajectory ns-t3s from (1, 1, 1) at 0 observe Z always : Z >= 0 and Z <= 4

Not run yet.

namespace DecidedShared_9a6160343b19
L171–171

Definition forsetiTime : Gimle.Asgard.Dynamics.TimeDomain L173–174

Namespace Notebook.NSLaminar.DecidedShared_9a6160343b19

⟨"time",  (((mkRat  (0)  1)  :  Q)  :  R)⟩\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 L176–177

Namespace Notebook.NSLaminar.DecidedShared_9a6160343b19

![(((mkRat  (1)  1)  :  Q)  :  R),  (((mkRat  (1)  1)  :  Q)  :  R),  (((mkRat  (1)  1)  :  Q)  :  R)]!\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 L179–179

Namespace Notebook.NSLaminar.DecidedShared_9a6160343b19

⟨4,  by  decide⟩\langle 4,\;\text{by}\;\text{decide}\rangle
Lean source · 1 line
def forsetiObservation : Fin 6 := ⟨4, by decide⟩

Definition forsetiIdentities : Prop L181–185

Namespace Notebook.NSLaminar.DecidedShared_9a6160343b19

Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.states.map  (⋅.initialId)  =  ["initial-a10",  "initial-a11",  "initial-a21"]  ∧\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{evolution}.\text{states}.\text{map}\;(\text{·}.\text{initialId})\;=\;\text{[}\texttt{"initial-a10"},\;\texttt{"initial-a11"},\;\texttt{"initial-a21"}\text{]}\;\land   (Gimle.Forseti.Examples.GalerkinNS.T3S.body.observations.get  forsetiObservation).port.id  =\;(\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{body}.\text{observations}.\text{get}\;\text{forsetiObservation}).\text{port}.\text{id}\;=  "obs-z"  ∧\;\texttt{"obs-z"}\;\land   Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.axis.id  =  "time"\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{evolution}.\text{axis}.\text{id}\;=\;\texttt{"time"}
Lean source · 5 lines
def forsetiIdentities : Prop :=
  Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.states.map (·.initialId) = ["initial-a10", "initial-a11", "initial-a21"] ∧
  (Gimle.Forseti.Examples.GalerkinNS.T3S.body.observations.get forsetiObservation).port.id =
    "obs-z" ∧
  Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.axis.id = "time"
end DecidedShared_9a6160343b19
L187–187
namespace Decided_in_enstrophy_ball
L189–189
open DecidedShared_9a6160343b19
L191–191

Example example (line 193) Kernel checkedAs recorded L193–193

Namespace Notebook.NSLaminar.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it
forsetiTime  =  forsetiTime\text{forsetiTime}\;=\;\text{forsetiTime}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_9a6160343b19.forsetiTime Notebook.NSLaminar.DecidedShared_9a6160343b19.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiTime = @DecidedShared_9a6160343b19.forsetiTime := rfl

Example example (line 194) Kernel checkedAs recorded L194–194

Namespace Notebook.NSLaminar.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it
forsetiInitial  =  forsetiInitial\text{forsetiInitial}\;=\;\text{forsetiInitial}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_9a6160343b19.forsetiInitial
  Notebook.NSLaminar.DecidedShared_9a6160343b19.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiInitial = @DecidedShared_9a6160343b19.forsetiInitial := rfl

Example example (line 195) Kernel checkedAs recorded L195–195

Namespace Notebook.NSLaminar.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it
forsetiObservation  =  forsetiObservation\text{forsetiObservation}\;=\;\text{forsetiObservation}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_9a6160343b19.forsetiObservation
  Notebook.NSLaminar.DecidedShared_9a6160343b19.forsetiObservation

Assumptions: none

Lean source & proof · 1 line
example : @forsetiObservation = @DecidedShared_9a6160343b19.forsetiObservation := rfl

Example example (line 196) Kernel checkedAs recorded L196–196

Namespace Notebook.NSLaminar.Decided_in_enstrophy_ball

Checked statement, as this project’s notation prints it
forsetiIdentities  =  forsetiIdentities\text{forsetiIdentities}\;=\;\text{forsetiIdentities}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_9a6160343b19.forsetiIdentities
  Notebook.NSLaminar.DecidedShared_9a6160343b19.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiIdentities = @DecidedShared_9a6160343b19.forsetiIdentities := rfl

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L198–199

Namespace Notebook.NSLaminar.Decided_in_enstrophy_ball

(.and  (.atom  .ge  (.var  ⟨0,  by  decide⟩))  (.atom  .le  (.add  (.var  ⟨0,  by  decide⟩)  (.neg  (.constant  (mkRat  (4)  1))))))(.\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}\;(4)\;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 (4) 1))))))

Definition forsetiLeaf : Gimle.Forseti.Syntax.Goal L201–204

Namespace Notebook.NSLaminar.Decided_in_enstrophy_ball

⟨⟨["Z"],  by  decide,  by  decide,  by  decide⟩,\langle \langle \text{[}\texttt{"Z"}\text{]},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide}\rangle ,  (.and  (.atom  .le  (.neg  (.var  ⟨0,  by  decide⟩)))  (.atom  .le  (.add  (.var  ⟨0,  by  decide⟩)  (.neg  (.constant  (mkRat  (4)  1)))))),\;(.\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}\;(4)\;1)))))),  forsetiPost⟩\;\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 (4) 1)))))),
    forsetiPost⟩

Definition forsetiContract : Prop L206–211

Namespace Notebook.NSLaminar.Decided_in_enstrophy_ball

Gimle.Forseti.Trajectory.Contract  Gimle.Forseti.Examples.GalerkinNS.T3S.observed  forsetiTime\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{observed}\;\text{forsetiTime}  (Gimle.Forseti.Trajectory.Initialized  forsetiTime  (fun  _  =>  True)\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Initialized}\;\text{forsetiTime}\;(\text{fun}\;\text{\_}\;=>\;\text{True})  (⋅  =  forsetiInitial))\;(\text{·}\;=\;\text{forsetiInitial}))  (Gimle.Forseti.Trajectory.Always  forsetiTime\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Always}\;\text{forsetiTime}  fun  o  =>  forsetiPost.holds  (fun  _  =>  o  forsetiObservation))\;\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.T3S.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 L213–213

Namespace Notebook.NSLaminar.Decided_in_enstrophy_ball

forsetiIdentities  ∧  forsetiContract\text{forsetiIdentities}\;\land \;\text{forsetiContract}
Lean source · 1 line
def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem in_enstrophy_ball Kernel checkedAs recorded L215–256

Namespace Notebook.NSLaminar.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-t3s 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 <= 4

Statement
have  circuit\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-t3s 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 <= 4 -/
theorem in_enstrophy_ball :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.T3S.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 ≤ 4) := by
  have root : forsetiRoot := by
    unfold forsetiRoot forsetiIdentities forsetiContract
    refine ⟨⟨by decide, by decide, by decide⟩, ?_⟩
    have time : forsetiTime = Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.time := by simp [forsetiTime, Gimle.Asgard.Model.Evolution.time, Gimle.Forseti.Examples.GalerkinNS.T3S.evolution] <;> norm_num [Rat.mkRat_eq_div]
    have init : forsetiInitial = Gimle.Forseti.Examples.GalerkinNS.T3S.compiled.initial := by rw [Gimle.Forseti.Examples.GalerkinNS.T3S.initial_eq]; funext i; fin_cases i <;> norm_num [forsetiInitial, Rat.mkRat_eq_div]
    have obs : forsetiObservation = Gimle.Forseti.Examples.GalerkinNS.T3S.enstrophyIndex := rfl
    rw [time, init, obs]
    refine Gimle.Forseti.Trajectory.Contract.consequence Gimle.Forseti.Examples.GalerkinNS.T3S.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 (4) 1) : ℚ) : ℝ) = 4 := 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
L258–258
Decisionin_energy_ball · trajectory · forsetiNever runL261–261
trajectory ns-t3s from (1, 1, 1) at 0 observe E always : E >= 0 and E <= 17/10

Not run yet.

namespace DecidedShared_f551903755fb
L263–263

Definition forsetiTime : Gimle.Asgard.Dynamics.TimeDomain L265–266

Namespace Notebook.NSLaminar.DecidedShared_f551903755fb

⟨"time",  (((mkRat  (0)  1)  :  Q)  :  R)⟩\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 L268–269

Namespace Notebook.NSLaminar.DecidedShared_f551903755fb

![(((mkRat  (1)  1)  :  Q)  :  R),  (((mkRat  (1)  1)  :  Q)  :  R),  (((mkRat  (1)  1)  :  Q)  :  R)]!\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 L271–271

Namespace Notebook.NSLaminar.DecidedShared_f551903755fb

⟨3,  by  decide⟩\langle 3,\;\text{by}\;\text{decide}\rangle
Lean source · 1 line
def forsetiObservation : Fin 6 := ⟨3, by decide⟩

Definition forsetiIdentities : Prop L273–277

Namespace Notebook.NSLaminar.DecidedShared_f551903755fb

Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.states.map  (⋅.initialId)  =  ["initial-a10",  "initial-a11",  "initial-a21"]  ∧\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{evolution}.\text{states}.\text{map}\;(\text{·}.\text{initialId})\;=\;\text{[}\texttt{"initial-a10"},\;\texttt{"initial-a11"},\;\texttt{"initial-a21"}\text{]}\;\land   (Gimle.Forseti.Examples.GalerkinNS.T3S.body.observations.get  forsetiObservation).port.id  =\;(\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{body}.\text{observations}.\text{get}\;\text{forsetiObservation}).\text{port}.\text{id}\;=  "obs-e"  ∧\;\texttt{"obs-e"}\;\land   Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.axis.id  =  "time"\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{evolution}.\text{axis}.\text{id}\;=\;\texttt{"time"}
Lean source · 5 lines
def forsetiIdentities : Prop :=
  Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.states.map (·.initialId) = ["initial-a10", "initial-a11", "initial-a21"] ∧
  (Gimle.Forseti.Examples.GalerkinNS.T3S.body.observations.get forsetiObservation).port.id =
    "obs-e" ∧
  Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.axis.id = "time"
end DecidedShared_f551903755fb
L279–279
namespace Decided_in_energy_ball
L281–281
open DecidedShared_f551903755fb
L283–283

Example example (line 285) Kernel checkedAs recorded L285–285

Namespace Notebook.NSLaminar.Decided_in_energy_ball

Checked statement, as this project’s notation prints it
forsetiTime  =  forsetiTime\text{forsetiTime}\;=\;\text{forsetiTime}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_f551903755fb.forsetiTime Notebook.NSLaminar.DecidedShared_f551903755fb.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiTime = @DecidedShared_f551903755fb.forsetiTime := rfl

Example example (line 286) Kernel checkedAs recorded L286–286

Namespace Notebook.NSLaminar.Decided_in_energy_ball

Checked statement, as this project’s notation prints it
forsetiInitial  =  forsetiInitial\text{forsetiInitial}\;=\;\text{forsetiInitial}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_f551903755fb.forsetiInitial
  Notebook.NSLaminar.DecidedShared_f551903755fb.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiInitial = @DecidedShared_f551903755fb.forsetiInitial := rfl

Example example (line 287) Kernel checkedAs recorded L287–287

Namespace Notebook.NSLaminar.Decided_in_energy_ball

Checked statement, as this project’s notation prints it
forsetiObservation  =  forsetiObservation\text{forsetiObservation}\;=\;\text{forsetiObservation}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_f551903755fb.forsetiObservation
  Notebook.NSLaminar.DecidedShared_f551903755fb.forsetiObservation

Assumptions: none

Lean source & proof · 1 line
example : @forsetiObservation = @DecidedShared_f551903755fb.forsetiObservation := rfl

Example example (line 288) Kernel checkedAs recorded L288–288

Namespace Notebook.NSLaminar.Decided_in_energy_ball

Checked statement, as this project’s notation prints it
forsetiIdentities  =  forsetiIdentities\text{forsetiIdentities}\;=\;\text{forsetiIdentities}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_f551903755fb.forsetiIdentities
  Notebook.NSLaminar.DecidedShared_f551903755fb.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiIdentities = @DecidedShared_f551903755fb.forsetiIdentities := rfl

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L290–291

Namespace Notebook.NSLaminar.Decided_in_energy_ball

(.and  (.atom  .ge  (.var  ⟨0,  by  decide⟩))  (.atom  .le  (.add  (.var  ⟨0,  by  decide⟩)  (.neg  (.constant  (mkRat  (17)  10))))))(.\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}\;(17)\;10))))))
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 (17) 10))))))

Definition forsetiLeaf : Gimle.Forseti.Syntax.Goal L293–296

Namespace Notebook.NSLaminar.Decided_in_energy_ball

⟨⟨["E"],  by  decide,  by  decide,  by  decide⟩,\langle \langle \text{[}\texttt{"E"}\text{]},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide}\rangle ,  (.and  (.atom  .le  (.neg  (.var  ⟨0,  by  decide⟩)))  (.atom  .le  (.add  (.var  ⟨0,  by  decide⟩)  (.neg  (.constant  (mkRat  (17)  10)))))),\;(.\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}\;(17)\;10)))))),  forsetiPost⟩\;\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 (17) 10)))))),
    forsetiPost⟩

Definition forsetiContract : Prop L298–303

Namespace Notebook.NSLaminar.Decided_in_energy_ball

Gimle.Forseti.Trajectory.Contract  Gimle.Forseti.Examples.GalerkinNS.T3S.observed  forsetiTime\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{observed}\;\text{forsetiTime}  (Gimle.Forseti.Trajectory.Initialized  forsetiTime  (fun  _  =>  True)\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Initialized}\;\text{forsetiTime}\;(\text{fun}\;\text{\_}\;=>\;\text{True})  (⋅  =  forsetiInitial))\;(\text{·}\;=\;\text{forsetiInitial}))  (Gimle.Forseti.Trajectory.Always  forsetiTime\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Always}\;\text{forsetiTime}  fun  o  =>  forsetiPost.holds  (fun  _  =>  o  forsetiObservation))\;\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.T3S.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 L305–305

Namespace Notebook.NSLaminar.Decided_in_energy_ball

forsetiIdentities  ∧  forsetiContract\text{forsetiIdentities}\;\land \;\text{forsetiContract}
Lean source · 1 line
def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem in_energy_ball Kernel checkedAs recorded L307–348

Namespace Notebook.NSLaminar.Decided_in_energy_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-t3s 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 <= 17/10

Statement
have  circuit\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-t3s 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 <= 17/10 -/
theorem in_energy_ball :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.T3S.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 ≤ 17/10) := by
  have root : forsetiRoot := by
    unfold forsetiRoot forsetiIdentities forsetiContract
    refine ⟨⟨by decide, by decide, by decide⟩, ?_⟩
    have time : forsetiTime = Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.time := by simp [forsetiTime, Gimle.Asgard.Model.Evolution.time, Gimle.Forseti.Examples.GalerkinNS.T3S.evolution] <;> norm_num [Rat.mkRat_eq_div]
    have init : forsetiInitial = Gimle.Forseti.Examples.GalerkinNS.T3S.compiled.initial := by rw [Gimle.Forseti.Examples.GalerkinNS.T3S.initial_eq]; funext i; fin_cases i <;> norm_num [forsetiInitial, Rat.mkRat_eq_div]
    have obs : forsetiObservation = Gimle.Forseti.Examples.GalerkinNS.T3S.energyIndex := rfl
    rw [time, init, obs]
    refine Gimle.Forseti.Trajectory.Contract.consequence Gimle.Forseti.Examples.GalerkinNS.T3S.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 (17) 10) : ℚ) : ℝ) = (17/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⟩
end Decided_in_energy_ball
L350–350
Decisionrest_never_grows · trajectory · forsetiNever runL353–353
trajectory ns-t3s from (1, 1, 1) at 0 observe R always : R >= 0 and R <= 6/5

Not run yet.

namespace DecidedShared_e85b1539f483
L355–355

Definition forsetiTime : Gimle.Asgard.Dynamics.TimeDomain L357–358

Namespace Notebook.NSLaminar.DecidedShared_e85b1539f483

⟨"time",  (((mkRat  (0)  1)  :  Q)  :  R)⟩\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 L360–361

Namespace Notebook.NSLaminar.DecidedShared_e85b1539f483

![(((mkRat  (1)  1)  :  Q)  :  R),  (((mkRat  (1)  1)  :  Q)  :  R),  (((mkRat  (1)  1)  :  Q)  :  R)]!\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 L363–363

Namespace Notebook.NSLaminar.DecidedShared_e85b1539f483

⟨5,  by  decide⟩\langle 5,\;\text{by}\;\text{decide}\rangle
Lean source · 1 line
def forsetiObservation : Fin 6 := ⟨5, by decide⟩

Definition forsetiIdentities : Prop L365–369

Namespace Notebook.NSLaminar.DecidedShared_e85b1539f483

Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.states.map  (⋅.initialId)  =  ["initial-a10",  "initial-a11",  "initial-a21"]  ∧\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{evolution}.\text{states}.\text{map}\;(\text{·}.\text{initialId})\;=\;\text{[}\texttt{"initial-a10"},\;\texttt{"initial-a11"},\;\texttt{"initial-a21"}\text{]}\;\land   (Gimle.Forseti.Examples.GalerkinNS.T3S.body.observations.get  forsetiObservation).port.id  =\;(\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{body}.\text{observations}.\text{get}\;\text{forsetiObservation}).\text{port}.\text{id}\;=  "obs-r"  ∧\;\texttt{"obs-r"}\;\land   Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.axis.id  =  "time"\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{evolution}.\text{axis}.\text{id}\;=\;\texttt{"time"}
Lean source · 5 lines
def forsetiIdentities : Prop :=
  Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.states.map (·.initialId) = ["initial-a10", "initial-a11", "initial-a21"] ∧
  (Gimle.Forseti.Examples.GalerkinNS.T3S.body.observations.get forsetiObservation).port.id =
    "obs-r" ∧
  Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.axis.id = "time"
end DecidedShared_e85b1539f483
L371–371
namespace Decided_rest_never_grows
L373–373
open DecidedShared_e85b1539f483
L375–375

Example example (line 377) Kernel checkedAs recorded L377–377

Namespace Notebook.NSLaminar.Decided_rest_never_grows

Checked statement, as this project’s notation prints it
forsetiTime  =  forsetiTime\text{forsetiTime}\;=\;\text{forsetiTime}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiTime Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiTime = @DecidedShared_e85b1539f483.forsetiTime := rfl

Example example (line 378) Kernel checkedAs recorded L378–378

Namespace Notebook.NSLaminar.Decided_rest_never_grows

Checked statement, as this project’s notation prints it
forsetiInitial  =  forsetiInitial\text{forsetiInitial}\;=\;\text{forsetiInitial}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiInitial
  Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiInitial = @DecidedShared_e85b1539f483.forsetiInitial := rfl

Example example (line 379) Kernel checkedAs recorded L379–379

Namespace Notebook.NSLaminar.Decided_rest_never_grows

Checked statement, as this project’s notation prints it
forsetiObservation  =  forsetiObservation\text{forsetiObservation}\;=\;\text{forsetiObservation}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiObservation
  Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiObservation

Assumptions: none

Lean source & proof · 1 line
example : @forsetiObservation = @DecidedShared_e85b1539f483.forsetiObservation := rfl

Example example (line 380) Kernel checkedAs recorded L380–380

Namespace Notebook.NSLaminar.Decided_rest_never_grows

Checked statement, as this project’s notation prints it
forsetiIdentities  =  forsetiIdentities\text{forsetiIdentities}\;=\;\text{forsetiIdentities}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiIdentities
  Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiIdentities = @DecidedShared_e85b1539f483.forsetiIdentities := rfl

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L382–383

Namespace Notebook.NSLaminar.Decided_rest_never_grows

(.and  (.atom  .ge  (.var  ⟨0,  by  decide⟩))  (.atom  .le  (.add  (.var  ⟨0,  by  decide⟩)  (.neg  (.constant  (mkRat  (6)  5))))))(.\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}\;(6)\;5))))))
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 (6) 5))))))

Definition forsetiLeaf : Gimle.Forseti.Syntax.Goal L385–388

Namespace Notebook.NSLaminar.Decided_rest_never_grows

⟨⟨["R"],  by  decide,  by  decide,  by  decide⟩,\langle \langle \text{[}\texttt{"R"}\text{]},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide},\;\text{by}\;\text{decide}\rangle ,  (.and  (.atom  .le  (.neg  (.var  ⟨0,  by  decide⟩)))  (.atom  .le  (.add  (.var  ⟨0,  by  decide⟩)  (.neg  (.constant  (mkRat  (6)  5)))))),\;(.\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}\;(6)\;5)))))),  forsetiPost⟩\;\text{forsetiPost}\rangle
Lean source · 4 lines
def forsetiLeaf : Gimle.Forseti.Syntax.Goal :=
  ⟨⟨["R"], by decide, by decide, by decide⟩,
    (.and (.atom .le (.neg (.var ⟨0, by decide⟩))) (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (6) 5)))))),
    forsetiPost⟩

Definition forsetiContract : Prop L390–395

Namespace Notebook.NSLaminar.Decided_rest_never_grows

Gimle.Forseti.Trajectory.Contract  Gimle.Forseti.Examples.GalerkinNS.T3S.observed  forsetiTime\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{observed}\;\text{forsetiTime}  (Gimle.Forseti.Trajectory.Initialized  forsetiTime  (fun  _  =>  True)\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Initialized}\;\text{forsetiTime}\;(\text{fun}\;\text{\_}\;=>\;\text{True})  (⋅  =  forsetiInitial))\;(\text{·}\;=\;\text{forsetiInitial}))  (Gimle.Forseti.Trajectory.Always  forsetiTime\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Always}\;\text{forsetiTime}  fun  o  =>  forsetiPost.holds  (fun  _  =>  o  forsetiObservation))\;\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.T3S.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 L397–397

Namespace Notebook.NSLaminar.Decided_rest_never_grows

forsetiIdentities  ∧  forsetiContract\text{forsetiIdentities}\;\land \;\text{forsetiContract}
Lean source · 1 line
def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem rest_never_grows Kernel checkedAs recorded L399–440

Namespace Notebook.NSLaminar.Decided_rest_never_grows

R is output 5 of the compiled circuit, the port obs-r; 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-t3s interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-r as R always : R >= 0 and R <= 6/5

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

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 42 lines
/-- R is output 5 of the compiled circuit, the port obs-r; 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-t3s interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-r as R always : R >= 0 and R <= 6/5 -/
theorem rest_never_grows :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.T3S.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 R := y t 5; R ≥ 0 ∧ R ≤ 6/5) := by
  have root : forsetiRoot := by
    unfold forsetiRoot forsetiIdentities forsetiContract
    refine ⟨⟨by decide, by decide, by decide⟩, ?_⟩
    have time : forsetiTime = Gimle.Forseti.Examples.GalerkinNS.T3S.evolution.time := by simp [forsetiTime, Gimle.Asgard.Model.Evolution.time, Gimle.Forseti.Examples.GalerkinNS.T3S.evolution] <;> norm_num [Rat.mkRat_eq_div]
    have init : forsetiInitial = Gimle.Forseti.Examples.GalerkinNS.T3S.compiled.initial := by rw [Gimle.Forseti.Examples.GalerkinNS.T3S.initial_eq]; funext i; fin_cases i <;> norm_num [forsetiInitial, Rat.mkRat_eq_div]
    have obs : forsetiObservation = Gimle.Forseti.Examples.GalerkinNS.T3S.restIndex := rfl
    rw [time, init, obs]
    refine Gimle.Forseti.Trajectory.Contract.consequence Gimle.Forseti.Examples.GalerkinNS.T3S.rest_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 (6) 5) : ℚ) : ℝ) = (6/5) := 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_rest_never_grows
L442–442
Decisionrest_below_one · trajectory · forsetiNever runL445–445
trajectory ns-t3s from (1, 1, 1) at 0 observe R always : R <= 1

Not run yet.

namespace Decided_rest_below_one
L447–447
open DecidedShared_e85b1539f483
L449–449

Example example (line 451) Kernel checkedAs recorded L451–451

Namespace Notebook.NSLaminar.Decided_rest_below_one

Checked statement, as this project’s notation prints it
forsetiTime  =  forsetiTime\text{forsetiTime}\;=\;\text{forsetiTime}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiTime Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiTime

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiTime = @DecidedShared_e85b1539f483.forsetiTime := rfl

Example example (line 452) Kernel checkedAs recorded L452–452

Namespace Notebook.NSLaminar.Decided_rest_below_one

Checked statement, as this project’s notation prints it
forsetiInitial  =  forsetiInitial\text{forsetiInitial}\;=\;\text{forsetiInitial}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiInitial
  Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiInitial

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiInitial = @DecidedShared_e85b1539f483.forsetiInitial := rfl

Example example (line 453) Kernel checkedAs recorded L453–453

Namespace Notebook.NSLaminar.Decided_rest_below_one

Checked statement, as this project’s notation prints it
forsetiObservation  =  forsetiObservation\text{forsetiObservation}\;=\;\text{forsetiObservation}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiObservation
  Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiObservation

Assumptions: none

Lean source & proof · 1 line
example : @forsetiObservation = @DecidedShared_e85b1539f483.forsetiObservation := rfl

Example example (line 454) Kernel checkedAs recorded L454–454

Namespace Notebook.NSLaminar.Decided_rest_below_one

Checked statement, as this project’s notation prints it
forsetiIdentities  =  forsetiIdentities\text{forsetiIdentities}\;=\;\text{forsetiIdentities}
Kernel form, without notation
Eq Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiIdentities
  Notebook.NSLaminar.DecidedShared_e85b1539f483.forsetiIdentities

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 1 line
example : @forsetiIdentities = @DecidedShared_e85b1539f483.forsetiIdentities := rfl

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L456–457

Namespace Notebook.NSLaminar.Decided_rest_below_one

(.atom  .le  (.add  (.var  ⟨0,  by  decide⟩)  (.neg  (.constant  (mkRat  (1)  1)))))(.\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 L459–464

Namespace Notebook.NSLaminar.Decided_rest_below_one

Gimle.Forseti.Trajectory.Contract  Gimle.Forseti.Examples.GalerkinNS.T3S.observed  forsetiTime\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{GalerkinNS}.\text{T3S}.\text{observed}\;\text{forsetiTime}  (Gimle.Forseti.Trajectory.Initialized  forsetiTime  (fun  _  =>  True)\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Initialized}\;\text{forsetiTime}\;(\text{fun}\;\text{\_}\;=>\;\text{True})  (⋅  =  forsetiInitial))\;(\text{·}\;=\;\text{forsetiInitial}))  (Gimle.Forseti.Trajectory.Always  forsetiTime\;(\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Always}\;\text{forsetiTime}  fun  o  =>  forsetiPost.holds  (fun  _  =>  o  forsetiObservation))\;\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.T3S.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 L466–466

Namespace Notebook.NSLaminar.Decided_rest_below_one

forsetiIdentities  ∧  forsetiContract\text{forsetiIdentities}\;\land \;\text{forsetiContract}
Lean source · 1 line
def forsetiRoot : Prop := forsetiIdentities ∧ forsetiContract

Theorem rest_below_one Contains sorryAs recorded L468–479

Namespace Notebook.NSLaminar.Decided_rest_below_one

R is output 5 of the compiled circuit, the port obs-r; 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-t3s interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-r as R always : R <= 1

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

Unfinished: the statement’s proof contains a placeholder.

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

Lean source & proof · 12 lines
/-- R is output 5 of the compiled circuit, the port obs-r; 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-t3s interpretation continuous-real obligation contract start time = 0 initial initial-a10 = 1, initial-a11 = 1, initial-a21 = 1 observe obs-r as R always : R <= 1 -/
theorem rest_below_one :
    have circuit := Gimle.Forseti.Examples.GalerkinNS.T3S.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 R := y t 5; R ≤ 1) := by
  sorry
end Decided_rest_below_one
L481–481
#print axioms rest_rate
L484–484
#print axioms coupling_sum
L485–485
#print axioms below_threshold
L486–486
#print axioms above_threshold_at_small_viscosity
L487–487
#print axioms rest_decays
L488–488
#print axioms every_member
L489–489
end Notebook.NSLaminar
L491–491