Two programs producing the Fibonacci stream

import Gimle.Forseti.Examples.LinearCircuitModels

L1–1

import Mathlib.Tactic.FinCases

L2–2

import Mathlib.Tactic.IntervalCases

L3–3

import Mathlib.Tactic.NormNum

L4–4

import Mathlib.Tactic.Ring

L5–5

The Fibonacci stream $0, 1, 1, 2, 3, \dots$ is produced by more than one linear program. We compare a two-state and a three-state program, both compiled in Gimle.Forseti.Examples.LinearCircuitModels, and prove that they produce the same output at every step.

Consider the simultaneous recurrences

(x_0,x_1)^+ = (x_0+x_1,x_0), \qquad o_x=x_0,

(y_0,y_1,y_2)^+ = (y_1,y_0+y_1,2y_2), \qquad o_y=y_1.

At starts $(0,1)$ and $(1,0,1)$ , respectively, both output prefixes are $0, 1, 1, 2, 3$ . Observation zero reads the initial state, before any update. The extra coordinate doubles at each step and is unobserved. Output agreement does not imply bounded states or identical state representations.

The sum of the state dimensions is five. The reusable finite-dimensional criterion proves that equality of these five observations implies equality at every natural-number step. Below we first establish that prefix for the larger family $(0,r)$ and $(r,0,r)$ , for every real $r$ , then specialize to $r = 1$ . All semantics are exact over the reals with rational coefficients.

namespace Gimle.Forseti.Examples.LinearCircuitFibonacci

L32–32

open Gimle.Asgard Gimle.Forseti Gimle.Forseti.LinearCircuit

L34–34

open scoped Matrix

L35–35

open Gimle.Forseti.Examples.LinearCircuitModels

L36–36

Why five observations suffice

First check five observations for every real scale

r

. Then use the library's finite-dimensional preservation argument to obtain equality at every step, and specialize to the stated starts. This proves output agreement, not bounded states or equality of internal coordinates.5 Kernel checked 5 As recorded

Check the finite prefix

For starts

(0,r)

and

(r,0,r)

, the first five outputs agree for every real

r

. This is the initialization needed by the all-step result.1 Kernel checked 1 As recorded

prefixFormula is an existing Forseti Syntax.Formula, built from conjunctions of equality atoms. Each atom substitutes the original polynomial updates into the readout. prefixFormula_holds_iff identifies its denotation with the five compiled-output comparisons. The following proof checks those comparisons symbolically; it does not assume the desired infinite conclusion.

Theorem `fibonacci_scaled_prefix` Kernel checkedAs recorded L58–68

Namespace Gimle.Forseti.Examples.LinearCircuitFibonacci

Symbolic real scaling exercises all real states of this family.

Statement

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

\;(\text{prefixFormula}\;\text{fibonacci}\;\text{extendedFibonacci}).\text{holds}

\;(\text{pointAppend}\;!\text{[}0,\;\text{r}\text{]}\;!\text{[}\text{r},\;0,\;\text{r}\text{]})

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 11 lines

/-- Symbolic real scaling exercises all real states of this family. -/
theorem fibonacci_scaled_prefix (r : ℝ) :
    (prefixFormula fibonacci extendedFibonacci).holds
      (pointAppend ![0, r] ![r, 0, r]) := by
  rw [prefixFormula_holds_iff]
  simp only [pointLeft_pointAppend, pointRight_pointAppend]
  intro n hn
  interval_cases n <;>
    norm_num [Program.observe, Program.output, Program.state_succ, Program.state_zero,
      Program.update, fibonacci, extendedFibonacci, Polynomial.Expr.eval]
  ring

Extend agreement to every step

The checked prefix and the library's preservation theorem imply agreement for every natural-number step. Specializing to

r=1

gives the two Fibonacci executions stated at the start of the notebook.3 Kernel checked 3 As recorded

The library theorem prefix_hoare proves {K} pairedUpdate {K}, where K is the prefix formula. Cayley–Hamilton on the combined state space supplies the finite-dimensional step. prefix_entails_output gives the predicate entailment from K to equality of the current readouts. prefix_safety combines these premises with the existing Discrete.certificate_sound rule.

observations_eq_of_prefixFormula consumes that all-step safety contract and the proved initialization. It identifies the paired run with the two original Discrete.run executions and obtains equality of their selected outputs. Thus the endpoint below really uses the existing predicate and Hoare calculus.

Theorem `fibonacci_scaled_equivalent` Kernel checkedAs recorded L89–92

Namespace Gimle.Forseti.Examples.LinearCircuitFibonacci

Statement

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

\;\forall \;\text{n},\;\text{fibonacci}.\text{observe}\;!\text{[}0,\;\text{r}\text{]}\;\text{n}\;=\;\text{extendedFibonacci}.\text{observe}\;!\text{[}\text{r},\;0,\;\text{r}\text{]}\;\text{n}

uses fibonacci_scaled_prefix

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines

theorem fibonacci_scaled_equivalent (r : ℝ) :
    ∀ n, fibonacci.observe ![0, r] n = extendedFibonacci.observe ![r, 0, r] n := by
  exact observations_eq_of_prefixFormula fibonacci extendedFibonacci _ _
    (fibonacci_scaled_prefix r)

Theorem `fibonacci_prefix` Kernel checkedAs recorded L94–97

Namespace Gimle.Forseti.Examples.LinearCircuitFibonacci

Statement

(\text{prefixFormula}\;\text{fibonacci}\;\text{extendedFibonacci}).\text{holds}

\;(\text{pointAppend}\;!\text{[}0,\;1\text{]}\;!\text{[}1,\;0,\;1\text{]})

uses fibonacci_scaled_prefix

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 4 lines

theorem fibonacci_prefix :
    (prefixFormula fibonacci extendedFibonacci).holds
      (pointAppend ![0, 1] ![1, 0, 1]) := by
  exact fibonacci_scaled_prefix 1

Theorem `fibonacci_equivalent` Kernel checkedAs recorded L99–106

Namespace Gimle.Forseti.Examples.LinearCircuitFibonacci

Statement

\forall \;\text{n},\;\text{fibonacci}.\text{output}.\text{run}

\;(\text{Discrete}.\text{run}\;(\text{u}\;:=\;0)\;(\text{p}\;:=\;0)\;\text{fibonacci}.\text{update}

\;\text{empty}\;!\text{[}0,\;1\text{]}\;(\text{fun}\;(\text{\_step}\;:\;\text{Nat})\;=>\;\text{empty})\;\text{n})\;0\;=

\;\text{extendedFibonacci}.\text{output}.\text{run}

\;(\text{Discrete}.\text{run}\;(\text{u}\;:=\;0)\;(\text{p}\;:=\;0)\;\text{extendedFibonacci}.\text{update}

\;\text{empty}\;!\text{[}1,\;0,\;1\text{]}\;(\text{fun}\;(\text{\_step}\;:\;\text{Nat})\;=>\;\text{empty})\;\text{n})\;0

uses fibonacci_prefix

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 8 lines

theorem fibonacci_equivalent :
    ∀ n, fibonacci.output.run
        (Discrete.run (u := 0) (p := 0) fibonacci.update
          empty ![0, 1] (fun (_step : Nat) => empty) n) 0 =
      extendedFibonacci.output.run
        (Discrete.run (u := 0) (p := 0) extendedFibonacci.update
          empty ![1, 0, 1] (fun (_step : Nat) => empty) n) 0 := by
  exact observations_eq_of_prefixFormula fibonacci extendedFibonacci _ _ fibonacci_prefix

Inspect the preservation contract

The paired update preserves the prefix predicate. This is an explicit instance of the library contract used above, not an extra assumption or a new proof of the infinite conclusion.1 Kernel checked 1 As recorded

This specialization exposes the reusable preservation result as the existing ExactHoare judgment over the compiled paired circuit. The earlier infinite conclusions use this same generic preservation theorem through prefix_safety; they do not depend on this later specialized alias.

Theorem `fibonacci_hoare` Kernel checkedAs recorded L121–125

Namespace Gimle.Forseti.Examples.LinearCircuitFibonacci

Statement

\text{ExactHoare}\;(\text{prefixFormula}\;\text{fibonacci}\;\text{extendedFibonacci}).\text{toPredicate}

\;(\text{pairedUpdate}\;\text{fibonacci}\;\text{extendedFibonacci})

\;(\text{prefixFormula}\;\text{fibonacci}\;\text{extendedFibonacci}).\text{toPredicate}

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 5 lines

theorem fibonacci_hoare :
    ExactHoare (prefixFormula fibonacci extendedFibonacci).toPredicate
      (pairedUpdate fibonacci extendedFibonacci)
      (prefixFormula fibonacci extendedFibonacci).toPredicate := by
  exact prefix_hoare fibonacci extendedFibonacci

A second realization: permuting the coordinates

The same argument handles a coordinate permutation. Two states on each side reduce initialization to four comparisons, and the reusable theorem again extends agreement to every step.2 Kernel checked 2 As recorded

Swapping the two visible coordinates, while also swapping the update and readout consistently, gives a two-state realization. Now the total dimension is four, so the finite initialization proof has four comparisons. The same safety endpoint establishes the infinite conclusion without changing the reusable library.

Theorem `permutation_prefix` Kernel checkedAs recorded L141–149

Namespace Gimle.Forseti.Examples.LinearCircuitFibonacci

Statement

(\text{prefixFormula}\;\text{fibonacci}\;\text{permutedFibonacci}).\text{holds}

\;(\text{pointAppend}\;!\text{[}0,\;1\text{]}\;!\text{[}1,\;0\text{]})

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 9 lines

theorem permutation_prefix :
    (prefixFormula fibonacci permutedFibonacci).holds
      (pointAppend ![0, 1] ![1, 0]) := by
  rw [prefixFormula_holds_iff]
  simp only [pointLeft_pointAppend, pointRight_pointAppend]
  intro n hn
  interval_cases n <;>
    norm_num [Program.observe, Program.output, Program.state_succ, Program.state_zero,
      Program.update, fibonacci, permutedFibonacci, Polynomial.Expr.eval]

Theorem `permutation_equivalent` Kernel checkedAs recorded L151–153

Namespace Gimle.Forseti.Examples.LinearCircuitFibonacci

Statement

\forall \;\text{n},\;\text{fibonacci}.\text{observe}\;!\text{[}0,\;1\text{]}\;\text{n}\;=\;\text{permutedFibonacci}.\text{observe}\;!\text{[}1,\;0\text{]}\;\text{n}

uses permutation_prefix

Assumptions: propext, Classical.choice, Quot.sound

Lean source & proof · 3 lines

theorem permutation_equivalent :
    ∀ n, fibonacci.observe ![0, 1] n = permutedFibonacci.observe ![1, 0] n := by
  exact observations_eq_of_prefixFormula fibonacci permutedFibonacci _ _ permutation_prefix

What the result establishes

Both comparisons establish exact output equality for all natural-number steps at the stated starts. The scaled comparison also covers every real $r$ in its specified family. The doubling hidden coordinate in the three-state program shows why output agreement does not establish boundedness of all states. The finite-dimensional argument comes from the imported library; the notebook's prose explains its role but is not itself a checked proof.

#print axioms fibonacci_scaled_prefix

L166–166

#print axioms fibonacci_scaled_equivalent

L167–167

#print axioms fibonacci_equivalent

L168–168

#print axioms fibonacci_hoare

L169–169

#print axioms permutation_equivalent

L170–170

end Gimle.Forseti.Examples.LinearCircuitFibonacci

L172–172

Why five observations suffice

Check the finite prefix

Theorem fibonacci_scaled_prefix Kernel checkedAs recorded L58–68

Extend agreement to every step

Theorem fibonacci_scaled_equivalent Kernel checkedAs recorded L89–92

Theorem fibonacci_prefix Kernel checkedAs recorded L94–97

Theorem fibonacci_equivalent Kernel checkedAs recorded L99–106

Inspect the preservation contract

Theorem fibonacci_hoare Kernel checkedAs recorded L121–125

A second realization: permuting the coordinates

Theorem permutation_prefix Kernel checkedAs recorded L141–149

Theorem permutation_equivalent Kernel checkedAs recorded L151–153

What the result establishes

Theorem `fibonacci_scaled_prefix` Kernel checkedAs recorded L58–68

Theorem `fibonacci_scaled_equivalent` Kernel checkedAs recorded L89–92

Theorem `fibonacci_prefix` Kernel checkedAs recorded L94–97

Theorem `fibonacci_equivalent` Kernel checkedAs recorded L99–106

Theorem `fibonacci_hoare` Kernel checkedAs recorded L121–125

Theorem `permutation_prefix` Kernel checkedAs recorded L141–149

Theorem `permutation_equivalent` Kernel checkedAs recorded L151–153