Does the safety proof survive the rewrite?

import Mathlib

L1–1

import Gimle.Forseti.Syntax.Certificate

L2–2

import Gimle.Forseti.Examples.EnergyOptimization

L3–3

Every change to a circuit breaks its proof. A cheaper implementation, a compiler pass, a rewrite: the circuit changes, and the safety argument written for the old one no longer applies to the new one, so someone proves it again, or nobody does. This notebook shows the argument coming along instead: a replacement circuit is proposed, Lean checks that it computes exactly the same function, and the safety contract re-attaches by one rule of the calculus, with no new proof about the new circuit. It also shows a wrong replacement being caught.

The circuit computes the energy of a two-dimensional signal,

E(x, y) = (x + y)^2 + (x - y)^2,

and comes with a contract: whenever both inputs lie in $[-1, 1]$ , the output lies in $[0, 4]$ . The proposed replacement is $2(x^2 + y^2)$ , with fewer arithmetic blocks. Here it was written by hand; a rewrite engine, a search or a model could have proposed it, and nothing below would change, because the proposer is never trusted. Lean proves the two circuits equivalent, and only that proof carries the contract across.

Proved. The original circuit meets its contract on $[-1, 1]^2$ , with the bound decided by the entailment decider and its certificate kept for replay. The replacement computes the same function on every real input, so it meets the same contract, by one rule. No bound below $4$ holds.

Refuted. A tighter bound of $3$ . A replacement that multiplies by $3$ instead of $2$ : not equivalent, and it breaks the contract at $(1, 1)$ .

Not claimed. Anything about floating-point evaluation, about inputs outside the square, or about rewrites in general: the rule is general, the example is one circuit.

Why this matters: certification is paid per artefact, and every optimisation produces a new artefact. Here the cost of re-certifying the cheaper circuit is one equivalence proof, machine-checked, and the rule that transfers the contract, exactCircuitSubstitution, is general within the calculus: any exact contract carries across any proved equivalence.

Both circuits were written in Python Asgard's combinator language and exported (Gimle.Forseti.EnergyDemoData and Gimle.Forseti.EnergyOptimizationData); the pinned library checks by rfl that the definitions used here are those exports, so every claim below is about the exported circuits. The library also proves each of these claims itself (equivalence, optimizedBound, wrongViolatesBound, upperBoundIsSharp); they are restated here so that this notebook's own check, not the library's build, is what carries them.

Establish the original contract

The original circuit computes

2x^2 + 2y^2

, which lies in

[0,4]

[-1,1]^2

. The polynomial certificate gives the circuit's safety contract; the tighter bound

3

is refuted.3 Kernel checked 4 As recorded 1 Contains sorry

The circuit duplicates its inputs, forms $x + y$ and $x - y$ , squares both and adds. Lean draws it from the definition:

namespace Notebook.EnergyOptimization

L63–63

open Gimle.Asgard Gimle.Forseti Gimle.Forseti.EnergyDemo Gimle.Forseti.EnergyOptimization

L64–64

circuit diagram `Gimle.Asgard.EnergyDemo.energy` L66–66

Identify the computed function

Expanding the squares, the cross terms cancel and

E(x, y) = 2x^2 + 2y^2

. Lean checks this by running the circuit symbolically, unfolding every block and normalising the polynomial.1 Kernel checked 1 As recorded

Theorem `energy_formula` Kernel checkedAs recorded L76–80

Namespace Notebook.EnergyOptimization

The exported circuit computes $2x^2 + 2y^2$ : the cross terms cancel.

Statement

(\text{input}\;:\;\text{Point}\;2)\;:

\;\text{energy}.\text{run}\;\text{input}\;0\;=\;2\;\cdot \;(\text{input}\;0)\text{\textasciicircum{}}2\;+\;2\;\cdot \;(\text{input}\;1)\text{\textasciicircum{}}2

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 5 lines

/-- The exported circuit computes $2x^2 + 2y^2$: the cross terms cancel. -/
theorem energy_formula (input : Point 2) :
    energy.run input 0 = 2 * (input 0)^2 + 2 * (input 1)^2 := by
  norm_num [energy, duplicate, interleave, sumAndDifference, difference, squareBoth, square]
  ring

Certify the polynomial bound

[-1,1]^2

, the output lies in

[0,4]

. Lean checks the exact polynomial certificate produced by the entailment decider.1 Kernel checked 1 As recorded

The contract is a polynomial entailment: from the input bounds $-1 \le x \le 1$ and $-1 \le y \le 1$ , the output bound $0 \le 2x^2 + 2y^2 \le 4$ follows. The entailment decider first searches for a counterexample and, finding none, for a certificate: an exact identity writing each gap as a sum of squares plus the hypotheses times sums of squares, which Lean re-checks by computation. The certificate is kept beside the notebook, and the checker replays it without Z3.

Decisionenergy_in_band · entailment · forsetiNever runL97–97

entailment x, y : x >= -1 and x <= 1 and y >= -1 and y <= 1 |- 2*x^2 + 2*y^2 >= 0 and 2*x^2 + 2*y^2 <= 4

Not run yet.

namespace Decided_energy_in_band

L99–99

Definition `forsetiContext` `: Gimle.Forseti.Syntax.Context` L101–102

Namespace Notebook.EnergyOptimization.Decided_energy_in_band

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

Lean source · 2 lines

def forsetiContext : Gimle.Forseti.Syntax.Context :=
  ⟨["x", "y"], by decide, by decide, by decide⟩

Definition `forsetiAntecedent` `: Gimle.Forseti.Syntax.Formula 2` L104–105

Namespace Notebook.EnergyOptimization.Decided_energy_in_band

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

Lean source · 2 lines

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

Definition `forsetiConsequent` `: Gimle.Forseti.Syntax.Formula 2` L107–108

Namespace Notebook.EnergyOptimization.Decided_energy_in_band

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

Lean source · 2 lines

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

Definition `forsetiGoal` `: Gimle.Forseti.Syntax.Goal` L110–110

Namespace Notebook.EnergyOptimization.Decided_energy_in_band

\langle \text{forsetiContext},\;\text{forsetiAntecedent},\;\text{forsetiConsequent}\rangle

Lean source · 1 line

def forsetiGoal : Gimle.Forseti.Syntax.Goal := ⟨forsetiContext, forsetiAntecedent, forsetiConsequent⟩

Theorem `energy_in_band` Kernel checkedAs recorded L112–130

Namespace Notebook.EnergyOptimization.Decided_energy_in_band

x, y are real numbers. The entailment decider proved it. Goal (entailment): entailment x, y : x >= -1 and x <= 1 and y >= -1 and y <= 1 |- 2*(x*x) + 2*(y*y) >= 0 and 2*(x*x) + 2*(y*y) <= 4

Statement

\forall \;\text{x}\;\text{y}\;:\;\mathbb{R} ,

\;\text{x}\;\ge \;-1\;\land \;\text{x}\;\le \;1\;\land \;\text{y}\;\ge \;-1\;\land \;\text{y}\;\le \;1\;\to

\;2\;\cdot \;(\text{x}\;\cdot \;\text{x})\;+\;2\;\cdot \;(\text{y}\;\cdot \;\text{y})\;\ge \;0\;\land \;2\;\cdot \;(\text{x}\;\cdot \;\text{x})\;+\;2\;\cdot \;(\text{y}\;\cdot \;\text{y})\;\le \;4

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 19 lines

/-- x, y are real numbers. The entailment decider proved it. Goal (entailment): entailment x, y : x >= -1 and x <= 1 and y >= -1 and y <= 1 |- 2*(x*x) + 2*(y*y) >= 0 and 2*(x*x) + 2*(y*y) <= 4 -/
theorem energy_in_band :
    ∀ x y : ℝ,
      x ≥ -1 ∧ x ≤ 1 ∧ y ≥ -1 ∧ y ≤ 1 →
      2 * (x * x) + 2 * (y * y) ≥ 0 ∧ 2 * (x * x) + 2 * (y * y) ≤ 4 := by
  have root : Gimle.Forseti.Syntax.FormulaEntailment forsetiAntecedent forsetiConsequent := by
    exact Gimle.Forseti.Syntax.EntailmentCertificate.sound forsetiGoal ⟨[⟨⟨[((mkRat (2) 1), (.var ⟨0, by decide⟩)), ((mkRat (2) 1), (.var ⟨1, by decide⟩))]⟩, [⟨[]⟩, ⟨[]⟩, ⟨[]⟩, ⟨[]⟩]⟩, ⟨⟨[]⟩, [⟨[((mkRat (1) 1), (.add (.constant (mkRat (1) 1)) (.neg (.var ⟨0, by decide⟩))))]⟩, ⟨[((mkRat (1) 1), (.add (.constant (mkRat (1) 1)) (.var ⟨0, by decide⟩)))]⟩, ⟨[((mkRat (1) 1), (.add (.constant (mkRat (1) 1)) (.neg (.var ⟨1, by decide⟩))))]⟩, ⟨[((mkRat (1) 1), (.add (.constant (mkRat (1) 1)) (.var ⟨1, by decide⟩)))]⟩]⟩]⟩ (by decide +kernel)
  have forsetiSucc : ∀ {n : Nat} (k : Nat) (h : k + 1 < n + 1), (⟨k + 1, h⟩ : Fin (n + 1)) = Fin.succ ⟨k, Nat.lt_of_succ_lt_succ h⟩ := fun _ _ => rfl
  have forsetiCast0 : (((mkRat (1) 1) : ℚ) : ℝ) = 1 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast1 : (((mkRat (2) 1) : ℚ) : ℝ) = 2 := by norm_num [Rat.mkRat_eq_div]
  have forsetiCast2 : (((mkRat (4) 1) : ℚ) : ℝ) = 4 := by norm_num [Rat.mkRat_eq_div]
  refine (fun (bridge : _ ↔ Gimle.Forseti.Syntax.FormulaEntailment forsetiAntecedent forsetiConsequent) => bridge.mpr root) ?_
  constructor
  · intro claim
    revert claim
    set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Syntax.FormulaEntailment, forsetiAntecedent, forsetiConsequent, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, forsetiSucc, Fin.cons_succ, Fin.zero_eta, Fin.cons_zero, 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, imp_self]
  · intro lane
    revert lane
    set_option linter.unusedSimpArgs false in simp only [Gimle.Forseti.Syntax.FormulaEntailment, forsetiAntecedent, forsetiConsequent, Gimle.Forseti.Syntax.Formula.holds, Gimle.Forseti.Syntax.Relation.holds, Gimle.Asgard.Polynomial.Expr.eval, Fin.forall_fin_succ_pi, Fin.forall_fin_zero_pi, forsetiSucc, Fin.cons_succ, Fin.zero_eta, Fin.cons_zero, 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, imp_self]

end Decided_energy_in_band

L132–132

Test the tighter bound of three

The bound

3

is false on the same square. The recorded result checks a counterexample; the positive claim below deliberately remains unproved.1 Contains sorry 1 As recorded

Could the bound be tighter? Asking for $2x^2 + 2y^2 \le 3$ on the same square is refuted: the decider produces a point where the claim fails, and Lean checks that the point satisfies the hypotheses and violates the conclusion, which proves the negation. The claim below is stated with sorry in place of a proof: it is false, so it has none. What Lean checked is its negation, recorded beside the notebook, and that is what its status reads.

Decisionenergy_below_three · entailment · forsetiNever runL149–149

entailment x, y : x >= -1 and x <= 1 and y >= -1 and y <= 1 |- 2*x^2 + 2*y^2 <= 3

Not run yet.

namespace Decided_energy_below_three

L151–151

Definition `forsetiContext` `: Gimle.Forseti.Syntax.Context` L153–154

Namespace Notebook.EnergyOptimization.Decided_energy_below_three

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

Lean source · 2 lines

def forsetiContext : Gimle.Forseti.Syntax.Context :=
  ⟨["x", "y"], by decide, by decide, by decide⟩

Definition `forsetiAntecedent` `: Gimle.Forseti.Syntax.Formula 2` L156–157

Namespace Notebook.EnergyOptimization.Decided_energy_below_three

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

Lean source · 2 lines

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

Definition `forsetiConsequent` `: Gimle.Forseti.Syntax.Formula 2` L159–160

Namespace Notebook.EnergyOptimization.Decided_energy_below_three

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

Lean source · 2 lines

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

Definition `forsetiGoal` `: Gimle.Forseti.Syntax.Goal` L162–162

Namespace Notebook.EnergyOptimization.Decided_energy_below_three

\langle \text{forsetiContext},\;\text{forsetiAntecedent},\;\text{forsetiConsequent}\rangle

Lean source · 1 line

def forsetiGoal : Gimle.Forseti.Syntax.Goal := ⟨forsetiContext, forsetiAntecedent, forsetiConsequent⟩

Theorem `energy_below_three` Contains sorryAs recorded L164–167

Namespace Notebook.EnergyOptimization.Decided_energy_below_three

x, y are real numbers. The entailment decider refuted it. Goal (entailment): entailment x, y : x >= -1 and x <= 1 and y >= -1 and y <= 1 |- 2*(x*x) + 2*(y*y) <= 3

Statement

\forall \;\text{x}\;\text{y}\;:\;\mathbb{R} ,\;\text{x}\;\ge \;-1\;\land \;\text{x}\;\le \;1\;\land \;\text{y}\;\ge \;-1\;\land \;\text{y}\;\le \;1\;\to \;2\;\cdot \;(\text{x}\;\cdot \;\text{x})\;+\;2\;\cdot \;(\text{y}\;\cdot \;\text{y})\;\le \;3

Unfinished: the statement’s proof contains a placeholder.

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

Lean source & proof · 4 lines

/-- x, y are real numbers. The entailment decider refuted it. Goal (entailment): entailment x, y : x >= -1 and x <= 1 and y >= -1 and y <= 1 |- 2*(x*x) + 2*(y*y) <= 3 -/
theorem energy_below_three :
    ∀ x y : ℝ, x ≥ -1 ∧ x ≤ 1 ∧ y ≥ -1 ∧ y ≤ 1 → 2 * (x * x) + 2 * (y * y) ≤ 3 := by
  sorry

end Decided_energy_below_three

L169–169

Attach the bound to the circuit

Combine the circuit's computed formula with the certified polynomial bound to obtain its Hoare contract on

[-1,1]^2

.1 Kernel checked 1 As recorded

The decided claims are about the polynomial. The contract is about the circuit: a precondition on its inputs and a postcondition on its output, what the calculus calls a Hoare triple. It follows from the formula above and the decided bound, so the decider's certificate is what carries it.

Theorem `original_contract` Kernel checkedAs recorded L184–192

Namespace Notebook.EnergyOptimization

The contract as a Hoare triple over the exported circuit: inputs in $[-1, 1]^2$ give an output in $[0, 4]$ .

Statement

\text{ExactHoare}\;\text{EnergyDemoData}.\text{precondition}\;\text{energy}\;\text{EnergyDemoData}.\text{postcondition}

uses energy_formula energy_in_band

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 9 lines

/-- The contract as a Hoare triple over the exported circuit: inputs in $[-1, 1]^2$ give an output in $[0, 4]$. -/
theorem original_contract :
    ExactHoare EnergyDemoData.precondition energy EnergyDemoData.postcondition := by
  intro input hypothesis
  have bounds : input 0 ≥ -1 ∧ input 0 ≤ 1 ∧ input 1 ≥ -1 ∧ input 1 ≤ 1 := by
    simpa [EnergyDemoData.precondition, and_assoc, and_left_comm, and_comm] using hypothesis
  have band := Decided_energy_in_band.energy_in_band (input 0) (input 1) bounds
  simp only [EnergyDemoData.postcondition, energy_formula, sq]
  constructor <;> linarith [band.1, band.2]

Transfer the contract to the replacement

The replacement computes the same function for every real input. Substituting that equivalence into the original contract gives the same safety guarantee on

[-1,1]^2

.2 Kernel checked 2 As recorded

Check the replacement's equivalence

The proposed replacement squares each input, adds, and doubles: six blocks where the original needs fourteen, four of them arithmetic where the original needs six.1 Kernel checked 1 As recorded

circuit diagram `Gimle.Asgard.EnergyOptimization.optimized` L208–208

Theorem `same_function` Kernel checkedAs recorded L210–217

Namespace Notebook.EnergyOptimization

The replacement computes the same function as the original on every real input.

Statement

\text{GlobalCircuitEquivalence}\;\text{energy}\;\text{optimized}

uses energy_formula

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 8 lines

/-- The replacement computes the same function as the original on every real input. -/
theorem same_function : GlobalCircuitEquivalence energy optimized := by
  intro input
  funext coordinate
  have zero : coordinate = 0 := Subsingleton.elim _ _
  subst zero
  rw [energy_formula, optimizedIdentity]
  ring

Transfer the contract by substitution

Equivalence is exactly what the calculus needs: an exact Hoare triple is a statement about a circuit's function, so it transfers to any circuit with the same function. The proof is one rule application, substituting the equivalent circuit into the contract.1 Kernel checked 1 As recorded

Theorem `optimised_contract` Kernel checkedAs recorded L228–231

Namespace Notebook.EnergyOptimization

The contract transfers to the replacement by substituting the equivalent circuit; nothing new is proved about it.

Statement

\text{ExactHoare}\;\text{EnergyDemoData}.\text{precondition}\;\text{optimized}\;\text{EnergyDemoData}.\text{postcondition}

uses same_function original_contract

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines

/-- The contract transfers to the replacement by substituting the equivalent circuit; nothing new is proved about it. -/
theorem optimised_contract :
    ExactHoare EnergyDemoData.precondition optimized EnergyDemoData.postcondition := by
  exact exactCircuitSubstitution original_contract same_function

Check failure cases and sharpness

Multiplying by

3

instead of

2

breaks both equivalence and the safety contract at

(1,1)

. The correct circuit attains

4

there, so its uniform upper bound on the square cannot be lowered.4 Kernel checked 4 As recorded

Reject the wrong replacement

(1,1)

the original gives

4

and the wrong replacement gives

6

. These differing outputs refute equivalence and violate the original contract.3 Kernel checked 3 As recorded

Suppose the replacement had multiplied by three. The circuit looks just as plausible, and a proposer that got the constant wrong would not know:

circuit diagram `Gimle.Asgard.EnergyOptimization.wrongMultiplier` L249–249

Theorem `wrong_differs` Kernel checkedAs recorded L251–254

Namespace Notebook.EnergyOptimization

At the corner $(1, 1)$ the original circuit gives $4$ and the wrong one gives $6$ .

Statement

\text{energy}.\text{run}\;!\text{[}1,\;1\text{]}\;0\;=\;4\;\land \;\text{wrongMultiplier}.\text{run}\;!\text{[}1,\;1\text{]}\;0\;=\;6

uses energy_formula

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines

/-- At the corner $(1, 1)$ the original circuit gives $4$ and the wrong one gives $6$. -/
theorem wrong_differs :
    energy.run ![1, 1] 0 = 4 ∧ wrongMultiplier.run ![1, 1] 0 = 6 := by
  norm_num [energy_formula, wrongMultiplier, squareBoth, square]

Theorem `wrong_not_equivalent` Kernel checkedAs recorded L256–261

Namespace Notebook.EnergyOptimization

One differing input is enough: the wrong replacement is not equivalent to the original.

Statement

\neg \;\text{GlobalCircuitEquivalence}\;\text{energy}\;\text{wrongMultiplier}

uses wrong_differs

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines

/-- One differing input is enough: the wrong replacement is not equivalent to the original. -/
theorem wrong_not_equivalent : ¬ GlobalCircuitEquivalence energy wrongMultiplier := by
  intro claim
  have equal := congrFun (claim ![1, 1]) 0
  rw [wrong_differs.1, wrong_differs.2] at equal
  norm_num at equal

Theorem `wrong_breaks_contract` Kernel checkedAs recorded L263–270

Namespace Notebook.EnergyOptimization

And it breaks the contract: $(1, 1)$ satisfies the precondition and $6 > 4$ .

Statement

\neg \;\text{ExactHoare}\;\text{EnergyDemoData}.\text{precondition}\;\text{wrongMultiplier}\;\text{EnergyDemoData}.\text{postcondition}

uses wrong_differs

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 8 lines

/-- And it breaks the contract: $(1, 1)$ satisfies the precondition and $6 > 4$. -/
theorem wrong_breaks_contract :
    ¬ ExactHoare EnergyDemoData.precondition wrongMultiplier EnergyDemoData.postcondition := by
  intro claim
  have corner : EnergyDemoData.precondition.holds ![1, 1] := by
    norm_num [EnergyDemoData.precondition]
  have bound := claim ![1, 1] corner
  norm_num [EnergyDemoData.postcondition, wrong_differs.2] at bound

Show that four is sharp

The refuted claim energy_below_three says

3

fails at some point. This says more: no bound below

4

works, because the corner attains

4

.1 Kernel checked 1 As recorded

Theorem `four_is_sharp` Kernel checkedAs recorded L279–287

Namespace Notebook.EnergyOptimization

No uniform bound below $4$ holds on the square: the corner $(1, 1)$ attains $4$ .

Statement

(\text{bound}\;:\;\mathbb{R} )

\;(\text{valid}\;:\;\forall \;\text{input},\;\text{EnergyDemoData}.\text{precondition}.\text{holds}\;\text{input}\;\to \;\text{energy}.\text{run}\;\text{input}\;0\;\le \;\text{bound})\;:

\;4\;\le \;\text{bound}

uses wrong_differs

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 9 lines

/-- No uniform bound below $4$ holds on the square: the corner $(1, 1)$ attains $4$. -/
theorem four_is_sharp (bound : ℝ)
    (valid : ∀ input, EnergyDemoData.precondition.holds input → energy.run input 0 ≤ bound) :
    4 ≤ bound := by
  have corner : EnergyDemoData.precondition.holds ![1, 1] := by
    norm_num [EnergyDemoData.precondition]
  have at_corner := valid ![1, 1] corner
  rw [wrong_differs.1] at at_corner
  exact at_corner

What is claimed, and what is not

Every claim is about the exported circuits over exact real arithmetic: the equivalence holds for every real input, and the contract for every input in the square. Nothing here says anything about floating-point evaluation of either circuit, or about inputs outside the square. The replacement was checked, not trusted; a replacement that is not an equivalence, like the one above, gets no contract. Its failing corner $(1, 1)$ was chosen by hand and checked by Lean; the decider was asked only about the polynomial bounds.

The axiom lists below are the standard three for every checked claim. energy_below_three shows sorryAx, as it must: it is the false claim, left unproved, whose refutation is what Lean checked.

#print axioms energy_formula

L305–305

#print axioms Decided_energy_in_band.energy_in_band

L306–306

#print axioms Decided_energy_below_three.energy_below_three

L307–307

#print axioms original_contract

L308–308

#print axioms same_function

L309–309

#print axioms optimised_contract

L310–310

#print axioms wrong_not_equivalent

L311–311

#print axioms wrong_breaks_contract

L312–312

#print axioms four_is_sharp

L313–313

end Notebook.EnergyOptimization

L315–315

Establish the original contract

circuit diagram Gimle.Asgard.EnergyDemo.energy L66–66

Identify the computed function

Theorem energy_formula Kernel checkedAs recorded L76–80

Certify the polynomial bound

Definition forsetiContext : Gimle.Forseti.Syntax.Context L101–102

Definition forsetiAntecedent : Gimle.Forseti.Syntax.Formula 2 L104–105

Definition forsetiConsequent : Gimle.Forseti.Syntax.Formula 2 L107–108

Definition forsetiGoal : Gimle.Forseti.Syntax.Goal L110–110

Theorem energy_in_band Kernel checkedAs recorded L112–130

Test the tighter bound of three

Definition forsetiContext : Gimle.Forseti.Syntax.Context L153–154

Definition forsetiAntecedent : Gimle.Forseti.Syntax.Formula 2 L156–157

Definition forsetiConsequent : Gimle.Forseti.Syntax.Formula 2 L159–160

Definition forsetiGoal : Gimle.Forseti.Syntax.Goal L162–162

Theorem energy_below_three Contains sorryAs recorded L164–167

Attach the bound to the circuit

Theorem original_contract Kernel checkedAs recorded L184–192

Transfer the contract to the replacement

Check the replacement's equivalence

circuit diagram Gimle.Asgard.EnergyOptimization.optimized L208–208

Theorem same_function Kernel checkedAs recorded L210–217

Transfer the contract by substitution

Theorem optimised_contract Kernel checkedAs recorded L228–231

Check failure cases and sharpness

Reject the wrong replacement

circuit diagram Gimle.Asgard.EnergyOptimization.wrongMultiplier L249–249

Theorem wrong_differs Kernel checkedAs recorded L251–254

Theorem wrong_not_equivalent Kernel checkedAs recorded L256–261

Theorem wrong_breaks_contract Kernel checkedAs recorded L263–270

Show that four is sharp

Theorem four_is_sharp Kernel checkedAs recorded L279–287

What is claimed, and what is not

circuit diagram `Gimle.Asgard.EnergyDemo.energy` L66–66

Theorem `energy_formula` Kernel checkedAs recorded L76–80

Definition `forsetiContext` `: Gimle.Forseti.Syntax.Context` L101–102

Definition `forsetiAntecedent` `: Gimle.Forseti.Syntax.Formula 2` L104–105

Definition `forsetiConsequent` `: Gimle.Forseti.Syntax.Formula 2` L107–108

Definition `forsetiGoal` `: Gimle.Forseti.Syntax.Goal` L110–110

Theorem `energy_in_band` Kernel checkedAs recorded L112–130

Definition `forsetiContext` `: Gimle.Forseti.Syntax.Context` L153–154

Definition `forsetiAntecedent` `: Gimle.Forseti.Syntax.Formula 2` L156–157

Definition `forsetiConsequent` `: Gimle.Forseti.Syntax.Formula 2` L159–160

Definition `forsetiGoal` `: Gimle.Forseti.Syntax.Goal` L162–162

Theorem `energy_below_three` Contains sorryAs recorded L164–167

Theorem `original_contract` Kernel checkedAs recorded L184–192

circuit diagram `Gimle.Asgard.EnergyOptimization.optimized` L208–208

Theorem `same_function` Kernel checkedAs recorded L210–217

Theorem `optimised_contract` Kernel checkedAs recorded L228–231

circuit diagram `Gimle.Asgard.EnergyOptimization.wrongMultiplier` L249–249

Theorem `wrong_differs` Kernel checkedAs recorded L251–254

Theorem `wrong_not_equivalent` Kernel checkedAs recorded L256–261

Theorem `wrong_breaks_contract` Kernel checkedAs recorded L263–270

Theorem `four_is_sharp` Kernel checkedAs recorded L279–287