Does the energy of a damped three-state system stay bounded?

Static snapshot of ThreeState.lean · source revision dated 2026-10-19T10:47:08.000Z · source SHA-256 db1be4a181e76e3be25f0f8bdc36391571d0399b2f2879993a3712484eded499. 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.ThreeStateContract
L3–3

Three coupled states xx, yy, zz push each other around and are each damped:

x′=−ax+y−zx' = -a x + y - z
y′=−x−by+zy' = -x - b y + z
z′=x−y−czz' = x - y - c z

with damping (a,b,c)=(13,12,2)(a, b, c) = (\tfrac13, \tfrac12, 2), started from (x,y,z)=(1,2,−1)(x, y, z) = (1, 2, -1) at time t=2t = 2. We watch its energy V=x2+y2+z2V = x^2 + y^2 + z^2, which starts at 66.

The coupling terms are skew-symmetric, so they only move energy between the states; the damping is the only thing that changes VV. Because every damping coefficient is positive, that suggests the energy can never grow. This notebook turns that intuition into checked claims, and shows where the intuition is not enough.

From equations to a circuit

The system is written once, as Asgard equations, in Gimle.Asgard.Examples.ThreeState.body:

  • dx := -a * x + y - z
  • dy := -x - b * y + z
  • dz := x - y - c * z
  • V := sqx + sqy + sqz, with sqx := x ^ 2 and likewise for y, z
  • dissipation := -2 * (a * sqx + b * sqy + c * sqz)

asgard-lean compiles that declaration into a circuit, model, and proves the compilation faithful: Gimle.Asgard.Examples.ThreeState.solves_iff_realizes says a signal solves the declared equations and initial condition exactly when it is a trajectory of the compiled circuit. Every trajectory claim below is about that compiled circuit, so it is about the equations as written, not about a re-typed copy of them.

What is modelled, and what is not

The claims are about the exact real solutions for t≥2t \ge 2, for this one parameter triple and this one initial state, with no inputs driving the system. They say nothing about other starts, other damping values, or robustness to either, and the bound 66 below is simply the initial energy. Nothing here says anything about a discretized or rounded implementation, and no simulation enters any claim's status.

namespace Notebook.ThreeState
L50–50
open Gimle.Asgard Gimle.Asgard.Examples.ThreeState
L51–51

model diagram Gimle.Asgard.Examples.ThreeState.model L53–53

Continuous modelt · start 2Vector fieldIntegrate · tdx/dt = ((((-1/3) × x) + y) + (-z))∫ → xx(2) = 1xxdy/dt = (((-x) + (-(1/2 × y))) + z)∫ → yy(2) = 2yydz/dt = ((x + (-y)) + (-(2 × z)))∫ → zz(2) = -1zz
Observations z x y V
Evidence · not proofsimulate Gimle.Asgard.Examples.ThreeState.model · forsetiNever runL54–54

Not run yet.

What a simulation shows

The run above is a floating-point simulation of the compiled field, kept beside the claims as evidence. Lean emits the field exactly, with the damping as the rationals 1/3, 1/2 and 2. The run rounds to float64 only to integrate, and the snapshot lists what it rounded: 1/3 and the step 1/100; 1/2 and 2 are exact in float64. It integrates with RK4 from t=2t = 2 to t=14t = 14.

The run shows the damping at work: all three states decay towards zero, and the energy with them; it is below one by about t=3.6t = 3.6, well inside the bound the decay argument under "Does the energy stay above one?" gives. That is evidence, not proof. No claim's status reads it: a trajectory that agreed with a false claim would prove nothing, and one that disagreed with a true claim would refute nothing.

The energy stays in its band

The first claim is the one the intuition predicts: for every t≥2t \ge 2 the energy lies in [0,6][0, 6], and the system has exactly one solution for t≥2t \ge 2 from this start.

The band itself is a forseti-lean theorem, Gimle.Forseti.Examples.ThreeStateContract.energy_contract, proved by hand once for this model. The decider's job is to recognise that the goal as written is an instance of that theorem about this compiled circuit: it checks the names, time, initial state and observation, and bridges the two postconditions with an entailment certificate that Lean re-checks. Here that bridge is trivial; it does real work when the bound asked for is weaker than the contract's.

The claim reads as the property, about ThreeStateContract.observed: the compiled loop followed by its compiled observations [z, x, y, V]. For every input whose initial wires start at (1,2,−1)(1, 2, -1), that circuit has an output, all its outputs agree for t≥2t \ge 2, and on every output VV (output 3, the port obs-v) stays in [0,6][0, 6] for t≥2t \ge 2. Its proof first proves the decider's own root theorem, forsetiRoot, over the generated definitions folded away below, then shows that this statement is equivalent to the root's contract; Lean checks both.

Decisionenergy_band · trajectory · forsetiNever runL98–100
trajectory three-state interpretation continuous-real obligation contract start time = 2 initial initial-x = 1, initial-y = 2, initial-z = -1 observe obs-v as V always : V >= 0 and V <= 6

Not run yet.

namespace DecidedShared_e390e59d2288
L102–102

Definition forsetiTime : Gimle.Asgard.Dynamics.TimeDomain L104–105

Namespace Notebook.ThreeState.DecidedShared_e390e59d2288

⟨"time",  (((mkRat  (2)  1)  :  Q)  :  R)⟩\langle \texttt{"time"},\;(((\text{mkRat}\;(2)\;1)\;:\;\mathbb{Q} )\;:\;\mathbb{R} )\rangle
Lean source · 2 lines
def forsetiTime : Gimle.Asgard.Dynamics.TimeDomain :=
  ⟨"time", (((mkRat (2) 1) : ℚ) : ℝ)⟩

Definition forsetiInitial : Gimle.Asgard.Point 3 L107–108

Namespace Notebook.ThreeState.DecidedShared_e390e59d2288

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

Definition forsetiObservation : Fin 4 L110–110

Namespace Notebook.ThreeState.DecidedShared_e390e59d2288

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

Definition forsetiIdentities : Prop L112–116

Namespace Notebook.ThreeState.DecidedShared_e390e59d2288

Gimle.Asgard.Examples.ThreeState.evolution.states.map  (⋅.initialId)  =  ["initial-x",  "initial-y",  "initial-z"]  ∧\text{Gimle}.\text{Asgard}.\text{Examples}.\text{ThreeState}.\text{evolution}.\text{states}.\text{map}\;(\text{·}.\text{initialId})\;=\;\text{[}\texttt{"initial-x"},\;\texttt{"initial-y"},\;\texttt{"initial-z"}\text{]}\;\land   ((Gimle.Asgard.Examples.ThreeState.body  (1  /  3)  (1  /  2)  2).observations.get  forsetiObservation).port.id  =\;((\text{Gimle}.\text{Asgard}.\text{Examples}.\text{ThreeState}.\text{body}\;(1\;/\;3)\;(1\;/\;2)\;2).\text{observations}.\text{get}\;\text{forsetiObservation}).\text{port}.\text{id}\;=  "obs-v"  ∧\;\texttt{"obs-v"}\;\land   Gimle.Asgard.Examples.ThreeState.evolution.axis.id  =  "time"\;\text{Gimle}.\text{Asgard}.\text{Examples}.\text{ThreeState}.\text{evolution}.\text{axis}.\text{id}\;=\;\texttt{"time"}
Lean source · 5 lines
def forsetiIdentities : Prop :=
  Gimle.Asgard.Examples.ThreeState.evolution.states.map (·.initialId) = ["initial-x", "initial-y", "initial-z"] ∧
  ((Gimle.Asgard.Examples.ThreeState.body (1 / 3) (1 / 2) 2).observations.get forsetiObservation).port.id =
    "obs-v" ∧
  Gimle.Asgard.Examples.ThreeState.evolution.axis.id = "time"
end DecidedShared_e390e59d2288
L118–118
namespace Decided_energy_band
L120–120
open DecidedShared_e390e59d2288
L122–122

Example example (line 124) Kernel checkedAs recorded L124–124

Namespace Notebook.ThreeState.Decided_energy_band

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

Assumptions: propext, Classical.choice, Quot.sound

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

Example example (line 125) Kernel checkedAs recorded L125–125

Namespace Notebook.ThreeState.Decided_energy_band

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

Assumptions: propext, Classical.choice, Quot.sound

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

Example example (line 126) Kernel checkedAs recorded L126–126

Namespace Notebook.ThreeState.Decided_energy_band

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

Assumptions: none

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

Example example (line 127) Kernel checkedAs recorded L127–127

Namespace Notebook.ThreeState.Decided_energy_band

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

Assumptions: propext, Classical.choice, Quot.sound

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

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L129–130

Namespace Notebook.ThreeState.Decided_energy_band

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

Definition forsetiLeaf : Gimle.Forseti.Syntax.Goal L132–135

Namespace Notebook.ThreeState.Decided_energy_band

⟨⟨["V"],  by  decide,  by  decide,  by  decide⟩,\langle \langle \text{[}\texttt{"V"}\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)  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}\;(6)\;1)))))),  forsetiPost⟩\;\text{forsetiPost}\rangle
Lean source · 4 lines
def forsetiLeaf : Gimle.Forseti.Syntax.Goal :=
  ⟨⟨["V"], 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) 1)))))),
    forsetiPost⟩

Definition forsetiContract : Prop L137–142

Namespace Notebook.ThreeState.Decided_energy_band

Gimle.Forseti.Trajectory.Contract  Gimle.Forseti.Examples.ThreeStateContract.observed  forsetiTime\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{ThreeStateContract}.\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.ThreeStateContract.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 L144–144

Namespace Notebook.ThreeState.Decided_energy_band

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

Theorem energy_band Kernel checkedAs recorded L146–188

Namespace Notebook.ThreeState.Decided_energy_band

V is output 3 of the compiled circuit, the port obs-v; the input's initial wires (initial-x, initial-y, initial-z) start at (1, 2, -1) at time = 2. The trajectory decider proved it. Goal (trajectory): trajectory three-state interpretation continuous-real obligation contract start time = 2 initial initial-x = 1, initial-y = 2, initial-z = -1 observe obs-v as V always : V >= 0 and V <= 6

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

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 43 lines
/-- V is output 3 of the compiled circuit, the port obs-v; the input's initial wires (initial-x, initial-y, initial-z) start at (1, 2, -1) at time = 2. The trajectory decider proved it. Goal (trajectory): trajectory three-state interpretation continuous-real obligation contract start time = 2 initial initial-x = 1, initial-y = 2, initial-z = -1 observe obs-v as V always : V >= 0 and V <= 6 -/
theorem energy_band :
    have circuit := Gimle.Forseti.Examples.ThreeStateContract.observed
    have time : Gimle.Asgard.Dynamics.TimeDomain := ⟨"time", 2⟩
    ∀ u : Gimle.Asgard.Dynamics.Signal (0 + 3),
      Gimle.Asgard.Dynamics.signalRight u 2 = ![1, 2, -1] →
      (∃ y : Gimle.Asgard.Dynamics.Signal 4, circuit.Rel time u y) ∧
      (∀ y y' : Gimle.Asgard.Dynamics.Signal 4, circuit.Rel time u y → circuit.Rel time u y' →
        ∀ t ≥ 2, y t = y' t) ∧
      (∀ y : Gimle.Asgard.Dynamics.Signal 4, circuit.Rel time u y →
        ∀ t ≥ 2, have V := y t 3; V ≥ 0 ∧ V ≤ 6) := by
  have root : forsetiRoot := by
    unfold forsetiRoot forsetiIdentities forsetiContract
    refine ⟨⟨by decide, by decide, by decide⟩, ?_⟩
    have time : forsetiTime = Gimle.Asgard.Examples.ThreeState.evolution.time := by simp [forsetiTime, Gimle.Asgard.Model.Evolution.time, Gimle.Asgard.Examples.ThreeState.evolution] <;> norm_num [Rat.mkRat_eq_div]
    have init : forsetiInitial = Gimle.Asgard.Examples.ThreeState.model.initial := by rw [Gimle.Asgard.Examples.ThreeState.initial_eq]; funext i; fin_cases i <;> norm_num [forsetiInitial, Rat.mkRat_eq_div]
    have obs : forsetiObservation = Gimle.Asgard.Examples.ThreeState.energyIndex := rfl
    rw [time, init, obs]
    refine Gimle.Forseti.Trajectory.Contract.consequence Gimle.Forseti.Examples.ThreeStateContract.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 (6) 1) : ℚ) : ℝ) = 6 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast1 : (((mkRat (2) 1) : ℚ) : ℝ) = 2 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast2 : (((mkRat (1) 1) : ℚ) : ℝ) = 1 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast3 : (((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, forsetiCast3, ← 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, forsetiCast3, ← 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, forsetiCast3, ← 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_energy_band
L190–190

Five is not a bound

It is tempting to tighten the bound because the energy decays. But a bound for all t≥2t \ge 2 must hold at t=2t = 2 too, and the trajectory starts at V=6V = 6, so "the energy is at most five for all t≥2t \ge 2" is false. The decider does not merely fail to prove it; it refutes it with the initial state as a checked witness.

Below, the claim is stated in the same form as the band, with sorry in place of a proof: it is false, so it has none. What Lean checked is its negation, recorded beside the notebook, which is why the claim shows as refuted. A later claim that used it would be marked as depending on a refuted claim.

Decisionenergy_below_five · trajectory · forsetiNever runL209–211
trajectory three-state interpretation continuous-real obligation contract start time = 2 initial initial-x = 1, initial-y = 2, initial-z = -1 observe obs-v as V always : V <= 5

Not run yet.

namespace Decided_energy_below_five
L213–213
open DecidedShared_e390e59d2288
L215–215

Example example (line 217) Kernel checkedAs recorded L217–217

Namespace Notebook.ThreeState.Decided_energy_below_five

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

Assumptions: propext, Classical.choice, Quot.sound

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

Example example (line 218) Kernel checkedAs recorded L218–218

Namespace Notebook.ThreeState.Decided_energy_below_five

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

Assumptions: propext, Classical.choice, Quot.sound

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

Example example (line 219) Kernel checkedAs recorded L219–219

Namespace Notebook.ThreeState.Decided_energy_below_five

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

Assumptions: none

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

Example example (line 220) Kernel checkedAs recorded L220–220

Namespace Notebook.ThreeState.Decided_energy_below_five

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

Assumptions: propext, Classical.choice, Quot.sound

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

Definition forsetiPost : Gimle.Forseti.Syntax.Formula 1 L222–223

Namespace Notebook.ThreeState.Decided_energy_below_five

(.atom  .le  (.add  (.var  ⟨0,  by  decide⟩)  (.neg  (.constant  (mkRat  (5)  1)))))(.\text{atom}\;.\text{le}\;(.\text{add}\;(.\text{var}\;\langle 0,\;\text{by}\;\text{decide}\rangle )\;(.\text{neg}\;(.\text{constant}\;(\text{mkRat}\;(5)\;1)))))
Lean source · 2 lines
def forsetiPost : Gimle.Forseti.Syntax.Formula 1 :=
  (.atom .le (.add (.var ⟨0, by decide⟩) (.neg (.constant (mkRat (5) 1)))))

Definition forsetiContract : Prop L225–230

Namespace Notebook.ThreeState.Decided_energy_below_five

Gimle.Forseti.Trajectory.Contract  Gimle.Forseti.Examples.ThreeStateContract.observed  forsetiTime\text{Gimle}.\text{Forseti}.\text{Trajectory}.\text{Contract}\;\text{Gimle}.\text{Forseti}.\text{Examples}.\text{ThreeStateContract}.\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.ThreeStateContract.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 L232–232

Namespace Notebook.ThreeState.Decided_energy_below_five

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

Theorem energy_below_five Contains sorryAs recorded L234–245

Namespace Notebook.ThreeState.Decided_energy_below_five

V is output 3 of the compiled circuit, the port obs-v; the input's initial wires (initial-x, initial-y, initial-z) start at (1, 2, -1) at time = 2. The trajectory decider refuted it. Goal (trajectory): trajectory three-state interpretation continuous-real obligation contract start time = 2 initial initial-x = 1, initial-y = 2, initial-z = -1 observe obs-v as V always : V <= 5

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
/-- V is output 3 of the compiled circuit, the port obs-v; the input's initial wires (initial-x, initial-y, initial-z) start at (1, 2, -1) at time = 2. The trajectory decider refuted it. Goal (trajectory): trajectory three-state interpretation continuous-real obligation contract start time = 2 initial initial-x = 1, initial-y = 2, initial-z = -1 observe obs-v as V always : V <= 5 -/
theorem energy_below_five :
    have circuit := Gimle.Forseti.Examples.ThreeStateContract.observed
    have time : Gimle.Asgard.Dynamics.TimeDomain := ⟨"time", 2⟩
    ∀ u : Gimle.Asgard.Dynamics.Signal (0 + 3),
      Gimle.Asgard.Dynamics.signalRight u 2 = ![1, 2, -1] →
      (∃ y : Gimle.Asgard.Dynamics.Signal 4, circuit.Rel time u y) ∧
      (∀ y y' : Gimle.Asgard.Dynamics.Signal 4, circuit.Rel time u y → circuit.Rel time u y' →
        ∀ t ≥ 2, y t = y' t) ∧
      (∀ y : Gimle.Asgard.Dynamics.Signal 4, circuit.Rel time u y →
        ∀ t ≥ 2, have V := y t 3; V ≤ 5) := by
  sorry
end Decided_energy_below_five
L247–247

Does the energy stay above one?

It does not, though nothing here checks that. The weakest damping is a=13a = \tfrac13, so V′≤−23VV' \le -\tfrac23 V, and V(t)≤6e−2(t−2)/3V(t) \le 6 e^{-2(t-2)/3} drops below one for every t>2+32ln⁡6≈4.7t > 2 + \tfrac32 \ln 6 \approx 4.7. That argument is ours, not Lean's.

The decider cannot settle it either way. A refutation needs a checked witness, a time and state where V<1V < 1, and it only tries the start, where V=6V = 6. Nor can it prove the claim: the only contract it has, 0≤V≤60 \le V \le 6, does not imply V≥1V \ge 1. Its answer is unknown, the correct answer for a checker: unknown means "not decided here", never "true" and never "false". Because there is nothing to check, it adds no claim to the notebook; the answer stays with the directive below. Refuting it in Forseti would take that decay bound as a Lean theorem about the model; it is not one yet.

Decisionenergy_at_least_one · trajectory · forsetiNever runL267–269
trajectory three-state interpretation continuous-real obligation contract start time = 2 initial initial-x = 1, initial-y = 2, initial-z = -1 observe obs-v as V always : V >= 1

Not run yet.

Why the energy cannot grow

Along a trajectory V′=2⟨x,f(x)⟩V' = 2\langle x, f(x)\rangle, where ff is the compiled field. The last claim checks that this pairing is never positive, at any state, for the field the compiler produced. energy_pairing in asgard-lean rewrites it as the model's declared dissipation := -2 * (a*sqx + b*sqy + c*sqz), and energyRate_value gives that expression with the damping substituted; with positive damping it is a negatively weighted sum of squares.

The prover agent proved it with ordinary Lean tactics, given one hint naming the two lemmas. The band above was proved independently in forseti-lean, from the same fact stated about the model's matrix; it does not use this claim.

Theorem energy_rate_nonpositive Kernel checkedAs recorded L286–291

Namespace Notebook.ThreeState

2⟨x,f(x)⟩≤02\langle x, f(x)\rangle \le 0 for the compiled field ff: the energy rate is never positive.

Statement
(x  :  Gimle.Asgard.Point  3)  :(\text{x}\;:\;\text{Gimle}.\text{Asgard}.\text{Point}\;3)\;:  2  ⋅  ∑  i,  x  i  ⋅  model.rates.circuit.run  x  i  ≤  0\;2\;\cdot \;\sum \;\text{i},\;\text{x}\;\text{i}\;\cdot \;\text{model}.\text{rates}.\text{circuit}.\text{run}\;\text{x}\;\text{i}\;\le \;0

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- $2\langle x, f(x)\rangle \le 0$ for the compiled field $f$: the energy rate is never positive. -/
theorem energy_rate_nonpositive (x : Gimle.Asgard.Point 3) :
    2 * ∑ i, x i * model.rates.circuit.run x i ≤ 0 := by
  rw [Gimle.Asgard.Examples.ThreeState.energy_pairing]
  rw [Gimle.Asgard.Examples.ThreeState.energyRate_value]
  nlinarith [sq_nonneg (x 0), sq_nonneg (x 1), sq_nonneg (x 2)]
end Notebook.ThreeState
L293–293