Equivalent damped Jordan chains

Static snapshot of LinearCircuitJordan.lean · source revision dated 2026-10-19T10:47:08.000Z · source SHA-256 a6684acf9ddce44023fefef188a25ef848359e0b95c7b1cc6779342093fd81f6. 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 Gimle.Forseti.LinearCircuitHoare
L1–1
import Mathlib.Tactic.FinCases
L2–2
import Mathlib.Tactic.NormNum
L3–3

Two linear systems can move through different states and still produce the same output stream. Damped Jordan chains show this in its simplest form: the two systems below differ in how strongly each coordinate feeds the next, yet a suitably scaled readout of the last coordinate is the same at every step.

Let SS be the nilpotent shift, which moves every coordinate one place down and inserts a zero; in dimension three it sends (x0,x1,x2)(x_0,x_1,x_2) to (0,x0,x1)(0,x_0,x_1). Compare the updates

A=12(I+S),B=12I+S.A = \tfrac12(I + S), \qquad B = \tfrac12 I + S.

Both start at the first basis vector e0e_0. Read the last coordinate of the first system and one quarter of the last coordinate of the second:

oA(n)=(Ane0)2,oB(n)=14 (Bne0)2.o_A(n) = (A^n e_0)_2, \qquad o_B(n) = \tfrac14\,(B^n e_0)_2.

After one step the middle coordinates already differ, 12\tfrac12 against 11, yet the two output streams agree. Expanding the binomials gives oA(n)=oB(n)=(n2) 2−no_A(n) = o_B(n) = \binom{n}{2}\,2^{-n}, so the outputs start 0,0,14,38,38,5160, 0, \tfrac14, \tfrac38, \tfrac38, \tfrac5{16}. That expansion is ours, not Lean's: the claims below check the equality for every nn, and the first six values of oAo_A exactly.

Six comparisons suffice because the sum of the dimensions is six. We also check the one- and two-dimensional versions, with output scalings 11 and 12\tfrac12. These are exact rational calculations embedded into real circuit semantics. The proved property is output equality; a decay-rate or stability estimate would require a separate theorem.

namespace Gimle.Forseti.Examples.LinearCircuitJordan
L37–37
open Gimle.Asgard Gimle.Forseti Gimle.Forseti.LinearCircuit
L39–39
open FiniteLinearEquivalence
L40–40
open scoped Matrix
L41–41

Definition jordanLeft1 : Program 1 L43–50A one-coordinate damped chain x+=12xx^+ = \tfrac12 x; both realizations coincide here.

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Fields
updates  :=  ![.mul  (.constant  (1  /  2))  (.var  0)]\text{updates}\;:=\;!\text{[}.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;0)\text{]}  readout  :=  .var  0\;\text{readout}\;:=\;.\text{var}\;0  matrix  :=  ![![1  /  2]]\;\text{matrix}\;:=\;!\text{[}!\text{[}1\;/\;2\text{]}\text{]}  weights  :=  ![1]\;\text{weights}\;:=\;!\text{[}1\text{]}  updates_ok  :=  by  intro  i;  fin_cases  i;  decide  +kernel\;\text{updates\_ok}\;:=\;\text{by}\;\text{intro}\;\text{i};\;\text{fin\_cases}\;\text{i};\;\text{decide}\;+\text{kernel}  readout_ok  :=  by  decide  +kernel\;\text{readout\_ok}\;:=\;\text{by}\;\text{decide}\;+\text{kernel}
Lean source · 8 lines
/-- A one-coordinate damped chain $x^+ = \tfrac12 x$; both realizations coincide here. -/
def jordanLeft1 : Program 1 where
  updates := ![.mul (.constant (1 / 2)) (.var 0)]
  readout := .var 0
  matrix := ![![1 / 2]]
  weights := ![1]
  updates_ok := by intro i; fin_cases i; decide +kernel
  readout_ok := by decide +kernel

Definition jordanRight1 : Program 1 L52–53In dimension one S=0S = 0, so 12(I+S)\tfrac12(I + S) and 12I+S\tfrac12 I + S are the same update.

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

jordanLeft1\text{jordanLeft1}
Lean source · 2 lines
/-- In dimension one $S = 0$, so $\tfrac12(I + S)$ and $\tfrac12 I + S$ are the same update. -/
def jordanRight1 : Program 1 := jordanLeft1

Definition jordanLeft2 : Program 2 L55–63Two coordinates with update A=12(I+S)A = \tfrac12(I + S), reading the last coordinate.

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Fields
updates  :=  ![.mul  (.constant  (1  /  2))  (.var  0),\text{updates}\;:=\;!\text{[}.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;0),  .add  (.mul  (.constant  (1  /  2))  (.var  0))  (.mul  (.constant  (1  /  2))  (.var  1))]\;.\text{add}\;(.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;0))\;(.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;1))\text{]}  readout  :=  .var  1\;\text{readout}\;:=\;.\text{var}\;1  matrix  :=  ![![1  /  2,  0],  ![1  /  2,  1  /  2]]\;\text{matrix}\;:=\;!\text{[}!\text{[}1\;/\;2,\;0\text{]},\;!\text{[}1\;/\;2,\;1\;/\;2\text{]}\text{]}  weights  :=  ![0,  1]\;\text{weights}\;:=\;!\text{[}0,\;1\text{]}  updates_ok  :=  by  intro  i;  fin_cases  i  <;>  decide  +kernel\;\text{updates\_ok}\;:=\;\text{by}\;\text{intro}\;\text{i};\;\text{fin\_cases}\;\text{i}\;<;>\;\text{decide}\;+\text{kernel}  readout_ok  :=  by  decide  +kernel\;\text{readout\_ok}\;:=\;\text{by}\;\text{decide}\;+\text{kernel}
Lean source · 9 lines
/-- Two coordinates with update $A = \tfrac12(I + S)$, reading the last coordinate. -/
def jordanLeft2 : Program 2 where
  updates := ![.mul (.constant (1 / 2)) (.var 0),
    .add (.mul (.constant (1 / 2)) (.var 0)) (.mul (.constant (1 / 2)) (.var 1))]
  readout := .var 1
  matrix := ![![1 / 2, 0], ![1 / 2, 1 / 2]]
  weights := ![0, 1]
  updates_ok := by intro i; fin_cases i <;> decide +kernel
  readout_ok := by decide +kernel

Definition jordanRight2 : Program 2 L65–73Two coordinates with update B=12I+SB = \tfrac12 I + S, reading half the last coordinate.

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Fields
updates  :=  ![.mul  (.constant  (1  /  2))  (.var  0),\text{updates}\;:=\;!\text{[}.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;0),  .add  (.var  0)  (.mul  (.constant  (1  /  2))  (.var  1))]\;.\text{add}\;(.\text{var}\;0)\;(.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;1))\text{]}  readout  :=  .mul  (.constant  (1  /  2))  (.var  1)\;\text{readout}\;:=\;.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;1)  matrix  :=  ![![1  /  2,  0],  ![1,  1  /  2]]\;\text{matrix}\;:=\;!\text{[}!\text{[}1\;/\;2,\;0\text{]},\;!\text{[}1,\;1\;/\;2\text{]}\text{]}  weights  :=  ![0,  1  /  2]\;\text{weights}\;:=\;!\text{[}0,\;1\;/\;2\text{]}  updates_ok  :=  by  intro  i;  fin_cases  i  <;>  decide  +kernel\;\text{updates\_ok}\;:=\;\text{by}\;\text{intro}\;\text{i};\;\text{fin\_cases}\;\text{i}\;<;>\;\text{decide}\;+\text{kernel}  readout_ok  :=  by  decide  +kernel\;\text{readout\_ok}\;:=\;\text{by}\;\text{decide}\;+\text{kernel}
Lean source · 9 lines
/-- Two coordinates with update $B = \tfrac12 I + S$, reading half the last coordinate. -/
def jordanRight2 : Program 2 where
  updates := ![.mul (.constant (1 / 2)) (.var 0),
    .add (.var 0) (.mul (.constant (1 / 2)) (.var 1))]
  readout := .mul (.constant (1 / 2)) (.var 1)
  matrix := ![![1 / 2, 0], ![1, 1 / 2]]
  weights := ![0, 1 / 2]
  updates_ok := by intro i; fin_cases i <;> decide +kernel
  readout_ok := by decide +kernel

Definition jordanLeft3 : Program 3 L75–84Three coordinates with update A=12(I+S)A = \tfrac12(I + S), reading the last coordinate.

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Fields
updates  :=  ![.mul  (.constant  (1  /  2))  (.var  0),\text{updates}\;:=\;!\text{[}.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;0),  .add  (.mul  (.constant  (1  /  2))  (.var  0))  (.mul  (.constant  (1  /  2))  (.var  1)),\;.\text{add}\;(.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;0))\;(.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;1)),  .add  (.mul  (.constant  (1  /  2))  (.var  1))  (.mul  (.constant  (1  /  2))  (.var  2))]\;.\text{add}\;(.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;1))\;(.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;2))\text{]}  readout  :=  .var  2\;\text{readout}\;:=\;.\text{var}\;2  matrix  :=  ![![1  /  2,  0,  0],  ![1  /  2,  1  /  2,  0],  ![0,  1  /  2,  1  /  2]]\;\text{matrix}\;:=\;!\text{[}!\text{[}1\;/\;2,\;0,\;0\text{]},\;!\text{[}1\;/\;2,\;1\;/\;2,\;0\text{]},\;!\text{[}0,\;1\;/\;2,\;1\;/\;2\text{]}\text{]}  weights  :=  ![0,  0,  1]\;\text{weights}\;:=\;!\text{[}0,\;0,\;1\text{]}  updates_ok  :=  by  intro  i;  fin_cases  i  <;>  decide  +kernel\;\text{updates\_ok}\;:=\;\text{by}\;\text{intro}\;\text{i};\;\text{fin\_cases}\;\text{i}\;<;>\;\text{decide}\;+\text{kernel}  readout_ok  :=  by  decide  +kernel\;\text{readout\_ok}\;:=\;\text{by}\;\text{decide}\;+\text{kernel}
Lean source · 10 lines
/-- Three coordinates with update $A = \tfrac12(I + S)$, reading the last coordinate. -/
def jordanLeft3 : Program 3 where
  updates := ![.mul (.constant (1 / 2)) (.var 0),
    .add (.mul (.constant (1 / 2)) (.var 0)) (.mul (.constant (1 / 2)) (.var 1)),
    .add (.mul (.constant (1 / 2)) (.var 1)) (.mul (.constant (1 / 2)) (.var 2))]
  readout := .var 2
  matrix := ![![1 / 2, 0, 0], ![1 / 2, 1 / 2, 0], ![0, 1 / 2, 1 / 2]]
  weights := ![0, 0, 1]
  updates_ok := by intro i; fin_cases i <;> decide +kernel
  readout_ok := by decide +kernel

Definition jordanRight3 : Program 3 L86–95Three coordinates with update B=12I+SB = \tfrac12 I + S, reading a quarter of the last coordinate.

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Fields
updates  :=  ![.mul  (.constant  (1  /  2))  (.var  0),\text{updates}\;:=\;!\text{[}.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;0),  .add  (.var  0)  (.mul  (.constant  (1  /  2))  (.var  1)),\;.\text{add}\;(.\text{var}\;0)\;(.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;1)),  .add  (.var  1)  (.mul  (.constant  (1  /  2))  (.var  2))]\;.\text{add}\;(.\text{var}\;1)\;(.\text{mul}\;(.\text{constant}\;(1\;/\;2))\;(.\text{var}\;2))\text{]}  readout  :=  .mul  (.constant  (1  /  4))  (.var  2)\;\text{readout}\;:=\;.\text{mul}\;(.\text{constant}\;(1\;/\;4))\;(.\text{var}\;2)  matrix  :=  ![![1  /  2,  0,  0],  ![1,  1  /  2,  0],  ![0,  1,  1  /  2]]\;\text{matrix}\;:=\;!\text{[}!\text{[}1\;/\;2,\;0,\;0\text{]},\;!\text{[}1,\;1\;/\;2,\;0\text{]},\;!\text{[}0,\;1,\;1\;/\;2\text{]}\text{]}  weights  :=  ![0,  0,  1  /  4]\;\text{weights}\;:=\;!\text{[}0,\;0,\;1\;/\;4\text{]}  updates_ok  :=  by  intro  i;  fin_cases  i  <;>  decide  +kernel\;\text{updates\_ok}\;:=\;\text{by}\;\text{intro}\;\text{i};\;\text{fin\_cases}\;\text{i}\;<;>\;\text{decide}\;+\text{kernel}  readout_ok  :=  by  decide  +kernel\;\text{readout\_ok}\;:=\;\text{by}\;\text{decide}\;+\text{kernel}
Lean source · 10 lines
/-- Three coordinates with update $B = \tfrac12 I + S$, reading a quarter of the last coordinate. -/
def jordanRight3 : Program 3 where
  updates := ![.mul (.constant (1 / 2)) (.var 0),
    .add (.var 0) (.mul (.constant (1 / 2)) (.var 1)),
    .add (.var 1) (.mul (.constant (1 / 2)) (.var 2))]
  readout := .mul (.constant (1 / 4)) (.var 2)
  matrix := ![![1 / 2, 0, 0], ![1, 1 / 2, 0], ![0, 1, 1 / 2]]
  weights := ![0, 0, 1 / 4]
  updates_ok := by intro i; fin_cases i <;> decide +kernel
  readout_ok := by decide +kernel

Initial states and the finite predicate

Every example starts at the first basis vector. embed casts rational coordinates exactly into the real state space. The helper below transports a finite rational matrix calculation to prefixFormula, an existing Forseti formula about the original compiled programs. The transport is justified by Program.observe_ratCast, rather than by an independently translated program.

Definition initial1 : Fin 1 → ℚ L107–108The initial state e0∈Q1e_0 \in \mathbb{Q}^1 as an explicit rational vector.

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

![1]!\text{[}1\text{]}
Lean source · 2 lines
/-- The initial state $e_0 \in \mathbb{Q}^1$ as an explicit rational vector. -/
def initial1 : Fin 1 → ℚ := ![1]

Definition initial2 : Fin 2 → ℚ L109–110The initial state e0∈Q2e_0 \in \mathbb{Q}^2.

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

![1,  0]!\text{[}1,\;0\text{]}
Lean source · 2 lines
/-- The initial state $e_0 \in \mathbb{Q}^2$. -/
def initial2 : Fin 2 → ℚ := ![1, 0]

Definition initial3 : Fin 3 → ℚ L111–112The initial state e0∈Q3e_0 \in \mathbb{Q}^3.

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

![1,  0,  0]!\text{[}1,\;0,\;0\text{]}
Lean source · 2 lines
/-- The initial state $e_0 \in \mathbb{Q}^3$. -/
def initial3 : Fin 3 → ℚ := ![1, 0, 0]

Definition embed {d : Nat} (x : Fin d → ℚ) : Point d L114–115A rational vector in Qd\mathbb{Q}^d as a point of Rd\mathbb{R}^d, coordinates cast exactly.

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

fun  i  =>  (x  i  :  R)\text{fun}\;\text{i}\;=>\;(\text{x}\;\text{i}\;:\;\mathbb{R} )
Lean source · 2 lines
/-- A rational vector in $\mathbb{Q}^d$ as a point of $\mathbb{R}^d$, coordinates cast exactly. -/
def embed {d : Nat} (x : Fin d → ℚ) : Point d := fun i => (x i : ℝ)

Theorem prefix_of_rational_prefix Kernel checkedAs recorded L117–131

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Finite rational evidence constructs the existing formula, without changing core APIs.

Statement
{d1  d2  :  Nat}\text{\{}\text{d}_{1}\;\text{d}_{2}\;:\;\text{Nat}\text{\}}  (P  :  Program  d1)  (Q  :  Program  d2)  (x  :  Fin  d1  →  Q)  (y  :  Fin  d2  →  Q)\;(\text{P}\;:\;\text{Program}\;\text{d}_{1})\;(\text{Q}\;:\;\text{Program}\;\text{d}_{2})\;(\text{x}\;:\;\text{Fin}\;\text{d}_{1}\;\to \;\mathbb{Q} )\;(\text{y}\;:\;\text{Fin}\;\text{d}_{2}\;\to \;\mathbb{Q} )  (h  :  ∀  n  :  Fin  (d1  +  d2),\;(\text{h}\;:\;\forall \;\text{n}\;:\;\text{Fin}\;(\text{d}_{1}\;+\;\text{d}_{2}),  matrix_output  P.matrix  x  P.weights  n  =  matrix_output  Q.matrix  y  Q.weights  n)  :\;\text{matrix\_output}\;\text{P}.\text{matrix}\;\text{x}\;\text{P}.\text{weights}\;\text{n}\;=\;\text{matrix\_output}\;\text{Q}.\text{matrix}\;\text{y}\;\text{Q}.\text{weights}\;\text{n})\;:  (prefixFormula  P  Q).holds  (pointAppend  (embed  x)  (embed  y))\;(\text{prefixFormula}\;\text{P}\;\text{Q}).\text{holds}\;(\text{pointAppend}\;(\text{embed}\;\text{x})\;(\text{embed}\;\text{y}))

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 15 lines
/-- Finite rational evidence constructs the existing formula, without changing core APIs. -/
private theorem prefix_of_rational_prefix {d₁ d₂ : Nat}
    (P : Program d₁) (Q : Program d₂) (x : Fin d₁ → ℚ) (y : Fin d₂ → ℚ)
    (h : ∀ n : Fin (d₁ + d₂),
      matrix_output P.matrix x P.weights n = matrix_output Q.matrix y Q.weights n) :
    (prefixFormula P Q).holds (pointAppend (embed x) (embed y)) := by
  rw [prefixFormula_holds_iff]
  simp only [pointLeft_pointAppend, pointRight_pointAppend]
  intro n hn
  calc
    P.observe (embed x) n = (matrix_output P.matrix x P.weights n : ℝ) :=
      P.observe_ratCast x n
    _ = (matrix_output Q.matrix y Q.weights n : ℝ) :=
      congrArg (fun q : ℚ => (q : ℝ)) (h ⟨n, hn⟩)
    _ = Q.observe (embed y) n := (Q.observe_ratCast y n).symm

Three concrete applications of the same interface

For each dimension, decide +kernel checks the finite rational calculation. The resulting initialization claim supplies observations_eq_of_prefixFormula. That library endpoint consumes prefix_safety: the existing Discrete.certificate_sound rule instantiated with the preservation Hoare triple prefix_hoare and the predicate entailment prefix_entails_output. Consequently each infinite conclusion is about the original compiled circuits and their initialized executions, not only about their matrix representations.

Dimension one is a boundary check where the two realizations coincide. The following two dimensions exercise genuinely different transition circuits.

Theorem jordan1_prefix Kernel checkedAs recorded L148–153

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Dimension-one initialization satisfies the actual finite observation formula.

Statement
(prefixFormula  jordanLeft1  jordanRight1).holds(\text{prefixFormula}\;\text{jordanLeft1}\;\text{jordanRight1}).\text{holds}  (pointAppend  (embed  initial1)  (embed  initial1))\;(\text{pointAppend}\;(\text{embed}\;\text{initial1})\;(\text{embed}\;\text{initial1}))
uses prefix_of_rational_prefix

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- Dimension-one initialization satisfies the actual finite observation formula. -/
theorem jordan1_prefix :
    (prefixFormula jordanLeft1 jordanRight1).holds
      (pointAppend (embed initial1) (embed initial1)) := by
  apply prefix_of_rational_prefix
  decide +kernel

Theorem jordan1_equivalent Kernel checkedAs recorded L155–158

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Dimension-one output equality uses the existing Hoare/safety endpoint.

Statement
∀  n,\forall \;\text{n},  jordanLeft1.observe  (embed  initial1)  n  =  jordanRight1.observe  (embed  initial1)  n\;\text{jordanLeft1}.\text{observe}\;(\text{embed}\;\text{initial1})\;\text{n}\;=\;\text{jordanRight1}.\text{observe}\;(\text{embed}\;\text{initial1})\;\text{n}
uses jordan1_prefix

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines
/-- Dimension-one output equality uses the existing Hoare/safety endpoint. -/
theorem jordan1_equivalent : ∀ n,
    jordanLeft1.observe (embed initial1) n = jordanRight1.observe (embed initial1) n := by
  exact observations_eq_of_prefixFormula jordanLeft1 jordanRight1 _ _ jordan1_prefix

Theorem jordan2_prefix Kernel checkedAs recorded L160–165

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Dimension-two initialization satisfies the actual finite observation formula.

Statement
(prefixFormula  jordanLeft2  jordanRight2).holds(\text{prefixFormula}\;\text{jordanLeft2}\;\text{jordanRight2}).\text{holds}  (pointAppend  (embed  initial2)  (embed  initial2))\;(\text{pointAppend}\;(\text{embed}\;\text{initial2})\;(\text{embed}\;\text{initial2}))
uses prefix_of_rational_prefix

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- Dimension-two initialization satisfies the actual finite observation formula. -/
theorem jordan2_prefix :
    (prefixFormula jordanLeft2 jordanRight2).holds
      (pointAppend (embed initial2) (embed initial2)) := by
  apply prefix_of_rational_prefix
  decide +kernel

Theorem jordan2_equivalent Kernel checkedAs recorded L167–170

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Distinct dimension-two realizations agree through the existing Hoare/safety endpoint.

Statement
∀  n,\forall \;\text{n},  jordanLeft2.observe  (embed  initial2)  n  =  jordanRight2.observe  (embed  initial2)  n\;\text{jordanLeft2}.\text{observe}\;(\text{embed}\;\text{initial2})\;\text{n}\;=\;\text{jordanRight2}.\text{observe}\;(\text{embed}\;\text{initial2})\;\text{n}
uses jordan2_prefix

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines
/-- Distinct dimension-two realizations agree through the existing Hoare/safety endpoint. -/
theorem jordan2_equivalent : ∀ n,
    jordanLeft2.observe (embed initial2) n = jordanRight2.observe (embed initial2) n := by
  exact observations_eq_of_prefixFormula jordanLeft2 jordanRight2 _ _ jordan2_prefix

Theorem jordan3_prefix Kernel checkedAs recorded L172–177

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Dimension-three initialization satisfies the actual finite observation formula.

Statement
(prefixFormula  jordanLeft3  jordanRight3).holds(\text{prefixFormula}\;\text{jordanLeft3}\;\text{jordanRight3}).\text{holds}  (pointAppend  (embed  initial3)  (embed  initial3))\;(\text{pointAppend}\;(\text{embed}\;\text{initial3})\;(\text{embed}\;\text{initial3}))
uses prefix_of_rational_prefix

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 6 lines
/-- Dimension-three initialization satisfies the actual finite observation formula. -/
theorem jordan3_prefix :
    (prefixFormula jordanLeft3 jordanRight3).holds
      (pointAppend (embed initial3) (embed initial3)) := by
  apply prefix_of_rational_prefix
  decide +kernel

Theorem jordan3_equivalent Kernel checkedAs recorded L179–182

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Distinct dimension-three realizations agree through the existing Hoare/safety endpoint.

Statement
∀  n,\forall \;\text{n},  jordanLeft3.observe  (embed  initial3)  n  =  jordanRight3.observe  (embed  initial3)  n\;\text{jordanLeft3}.\text{observe}\;(\text{embed}\;\text{initial3})\;\text{n}\;=\;\text{jordanRight3}.\text{observe}\;(\text{embed}\;\text{initial3})\;\text{n}
uses jordan3_prefix

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines
/-- Distinct dimension-three realizations agree through the existing Hoare/safety endpoint. -/
theorem jordan3_equivalent : ∀ n,
    jordanLeft3.observe (embed initial3) n = jordanRight3.observe (embed initial3) n := by
  exact observations_eq_of_prefixFormula jordanLeft3 jordanRight3 _ _ jordan3_prefix

Independent numerical controls

Agreement between two implementations alone would not rule out the same mistake in both. The next claims compare the selected left outputs with prescribed exact values, independently of the equality proof. Observation zero is included. Finally, explicit unequal next-state coordinates confirm that the two nontrivial examples really have different transitions.

Theorem jordan2_expected Kernel checkedAs recorded L194–205

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Independent expected outputs prevent a merely coincident wrong-prefix check.

Statement
(n  :  Fin  4)  :(\text{n}\;:\;\text{Fin}\;4)\;:  jordanLeft2.observe  (embed  initial2)  n  =  (![0,  1  /  2,  1  /  2,  3  /  8]  :  Fin  4  →  R)  n\;\text{jordanLeft2}.\text{observe}\;(\text{embed}\;\text{initial2})\;\text{n}\;=\;(!\text{[}0,\;1\;/\;2,\;1\;/\;2,\;3\;/\;8\text{]}\;:\;\text{Fin}\;4\;\to \;\mathbb{R} )\;\text{n}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 12 lines
/-- Independent expected outputs prevent a merely coincident wrong-prefix check. -/
theorem jordan2_expected (n : Fin 4) :
    jordanLeft2.observe (embed initial2) n = (![0, 1 / 2, 1 / 2, 3 / 8] : Fin 4 → ℝ) n := by
  have h : ∀ k : Fin 4, matrix_output jordanLeft2.matrix initial2 jordanLeft2.weights k =
      (![0, 1 / 2, 1 / 2, 3 / 8] : Fin 4 → ℚ) k := by decide +kernel
  calc
    jordanLeft2.observe (embed initial2) n =
        (matrix_output jordanLeft2.matrix initial2 jordanLeft2.weights n : ℝ) :=
      jordanLeft2.observe_ratCast initial2 n
    _ = ((![0, 1 / 2, 1 / 2, 3 / 8] : Fin 4 → ℚ) n : ℝ) :=
      congrArg (fun q : ℚ => (q : ℝ)) (h n)
    _ = _ := by fin_cases n <;> norm_num

Theorem jordan3_expected Kernel checkedAs recorded L207–219

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

The six-observation dimension-three prefix has the prescribed binomial values.

Statement
(n  :  Fin  6)  :(\text{n}\;:\;\text{Fin}\;6)\;:  jordanLeft3.observe  (embed  initial3)  n  =\;\text{jordanLeft3}.\text{observe}\;(\text{embed}\;\text{initial3})\;\text{n}\;=  (![0,  0,  1  /  4,  3  /  8,  3  /  8,  5  /  16]  :  Fin  6  →  R)  n\;(!\text{[}0,\;0,\;1\;/\;4,\;3\;/\;8,\;3\;/\;8,\;5\;/\;16\text{]}\;:\;\text{Fin}\;6\;\to \;\mathbb{R} )\;\text{n}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 13 lines
/-- The six-observation dimension-three prefix has the prescribed binomial values. -/
theorem jordan3_expected (n : Fin 6) :
    jordanLeft3.observe (embed initial3) n =
      (![0, 0, 1 / 4, 3 / 8, 3 / 8, 5 / 16] : Fin 6 → ℝ) n := by
  have h : ∀ k : Fin 6, matrix_output jordanLeft3.matrix initial3 jordanLeft3.weights k =
      (![0, 0, 1 / 4, 3 / 8, 3 / 8, 5 / 16] : Fin 6 → ℚ) k := by decide +kernel
  calc
    jordanLeft3.observe (embed initial3) n =
        (matrix_output jordanLeft3.matrix initial3 jordanLeft3.weights n : ℝ) :=
      jordanLeft3.observe_ratCast initial3 n
    _ = ((![0, 0, 1 / 4, 3 / 8, 3 / 8, 5 / 16] : Fin 6 → ℚ) n : ℝ) :=
      congrArg (fun q : ℚ => (q : ℝ)) (h n)
    _ = _ := by fin_cases n <;> norm_num

Theorem jordan2_different_updates Kernel checkedAs recorded L221–224

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

The two nontrivial trials really use different next-state circuits.

Statement
jordanLeft2.update.run  (embed  initial2)  1  ≠  jordanRight2.update.run  (embed  initial2)  1\text{jordanLeft2}.\text{update}.\text{run}\;(\text{embed}\;\text{initial2})\;1\;\ne \;\text{jordanRight2}.\text{update}.\text{run}\;(\text{embed}\;\text{initial2})\;1

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines
/-- The two nontrivial trials really use different next-state circuits. -/
theorem jordan2_different_updates :
    jordanLeft2.update.run (embed initial2) 1 ≠ jordanRight2.update.run (embed initial2) 1 := by
  norm_num [Program.update_run, jordanLeft2, jordanRight2, embed, initial2, Fin.sum_univ_succ]

Theorem jordan3_different_updates Kernel checkedAs recorded L226–228

Namespace Gimle.Forseti.Examples.LinearCircuitJordan

Statement
jordanLeft3.update.run  (embed  initial3)  1  ≠  jordanRight3.update.run  (embed  initial3)  1\text{jordanLeft3}.\text{update}.\text{run}\;(\text{embed}\;\text{initial3})\;1\;\ne \;\text{jordanRight3}.\text{update}.\text{run}\;(\text{embed}\;\text{initial3})\;1

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 3 lines
theorem jordan3_different_updates :
    jordanLeft3.update.run (embed initial3) 1 ≠ jordanRight3.update.run (embed initial3) 1 := by
  norm_num [Program.update_run, jordanLeft3, jordanRight3, embed, initial3, Fin.sum_univ_succ]
#print axioms jordan1_prefix
L230–230
#print axioms jordan1_equivalent
L231–231
#print axioms jordan2_prefix
L232–232
#print axioms jordan2_equivalent
L233–233
#print axioms jordan3_prefix
L234–234
#print axioms jordan3_equivalent
L235–235
#print axioms jordan2_expected
L236–236
#print axioms jordan3_expected
L237–237
#print axioms jordan2_different_updates
L238–238
#print axioms jordan3_different_updates
L239–239
end Gimle.Forseti.Examples.LinearCircuitJordan
L241–241