Does a damped scalar stay in its band?

Static snapshot of ScalarDecay.lean · source revision dated 2026-10-19T10:47:08.000Z · source SHA-256 cf86781b0596d24df074f03c1b8f54bb1e2de33e048bef973eb5b77f9190843c. 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

One state xx, damped at a constant rate:

x′=−kxx' = -k x

with k=12k = \tfrac12, started from x=1x = 1 at time t=0t = 0. We watch the energy V=x2V = x^2, which starts at 11.

There is no coupling here and nothing driving the system, so the damping is the only thing that moves VV. Because kk is positive, the energy should never grow. This notebook turns that intuition into claims Lean checks, and marks where it is left open.

The same question for three coupled states, where the coupling makes the argument less direct, is taken up in ThreeState.

What is modelled, and what is not

The questions are about the exact real solution for t≥0t \ge 0, for this one rate and this one initial state. The claims below are facts about every state xx; carrying them over to the solution is an argument made in the prose, not a claim. They say nothing about other starts, other rates, or a discretized implementation. No simulation enters any claim's status.

namespace Notebook.ScalarDecay
L31–31

Definition k : ℝ L33–34The damping rate.

Namespace Notebook.ScalarDecay

12\frac{1}{2}
Lean source · 2 lines
/-- The damping rate. -/
noncomputable def k : ℝ := 1 / 2
Details
Declaration context
noncomputable\text{noncomputable}

Theorem k_pos Kernel checkedAs recorded L36–39

Namespace Notebook.ScalarDecay

The rate is positive, which is what makes the system a damped one.

Statement
0  <  k0\;<\;\text{k}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines
/-- The rate is positive, which is what makes the system a damped one. -/
theorem k_pos : 0 < k := by
  unfold k
  norm_num

The energy never grows

The energy is V=x2V = x^2, so along a solution its rate is V′=2xx′=2x(−kx)V' = 2xx' = 2x(-kx). Write that out and it is −2kx2-2kx^2, which is a negative multiple of a square. This is the whole decay argument, stated for every state the system could be in rather than for the particular trajectory.

Theorem energy_rate_nonpositive Kernel checkedAs recorded L50–53

Namespace Notebook.ScalarDecay

The energy rate is never positive, at any state.

Statement
(x  :  R)  :  2  ⋅  x  ⋅  (−k  ⋅  x)  ≤  0(\text{x}\;:\;\mathbb{R} )\;:\;2\;\cdot \;\text{x}\;\cdot \;(-\text{k}\;\cdot \;\text{x})\;\le \;0
uses k_pos

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines
/-- The energy rate is never positive, at any state. -/
theorem energy_rate_nonpositive (x : ℝ) : 2 * x * (-k * x) ≤ 0 := by
  have hk : 0 < k := k_pos
  nlinarith [sq_nonneg x]

The energy stays in its band

The band has two sides, and only one of them needs the dynamics. The upper side follows from the claim above: the energy starts at 11 and its rate is never positive, so it never climbs past 11. That last step integrates the rate along the solution; it is ours, not Lean's. The lower side needs nothing at all about this system, because an energy is a square.

That asymmetry is worth stating rather than hiding: a reader should be able to see which half of [0,1][0, 1] is earned by the damping argument and which half is free.

Theorem energy_nonneg Kernel checkedAs recorded L69–71

Namespace Notebook.ScalarDecay

The energy is never negative, whatever the state.

Statement
(x  :  R)  :  0  ≤  x  ^  2(\text{x}\;:\;\mathbb{R} )\;:\;0\;\le \;\text{x}\;\text{\textasciicircum{}}\;2

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 3 lines
/-- The energy is never negative, whatever the state. -/
theorem energy_nonneg (x : ℝ) : 0 ≤ x ^ 2 := by
  exact sq_nonneg x

Does the energy stay above a floor?

The intuition says no: the damping drives xx towards zero, so the energy falls below any positive floor eventually. The claim below asserts the opposite, over every state rather than just the start, which makes it plainly false — x=0x = 0 refutes it. It is left unproved on purpose, so the notebook shows an open status beside the checked ones.

Note what the status does *not* say. open means no proof has been checked, not that the claim is false; Forseti would only report it refuted once a proof of its negation had itself been checked.

Theorem energy_above_floor Contains sorryAs recorded L87–89

Namespace Notebook.ScalarDecay

The energy never falls below a quarter. Unproved, and in fact false.

Statement
(x  :  R)  :  (1  :  R)  /  4  ≤  x  ^  2(\text{x}\;:\;\mathbb{R} )\;:\;(1\;:\;\mathbb{R} )\;/\;4\;\le \;\text{x}\;\text{\textasciicircum{}}\;2

Unfinished: the statement’s proof contains a placeholder.

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

Lean source & proof · 3 lines
/-- The energy never falls below a quarter. Unproved, and in fact false. -/
theorem energy_above_floor (x : ℝ) : (1 : ℝ) / 4 ≤ x ^ 2 := by
  sorry
end Notebook.ScalarDecay
L91–91