FixedPoint

Difficulty: optional — 7 definitions, 0 abbreviations, 7 lemmas, 3 theorems.

definition lemma theorem
legend

Some rules can meaningfully be run on their own output, feeding what comes out straight back in as the next input. Doing this over and over settles down to a fixed value — one where running the rule again changes nothing at all — exactly when the rule never “changes its mind”: once a wire has turned on, feeding the rule more on-wires only ever keeps that wire on or turns more on, never back off. Every rule like this, run enough times starting from every wire off, reaches its own fixed value, and always the same way: by simply running it long enough.

One bit sequence lines up with another wherever it says a wire is on: every wire the first sequence turns on, the second does too (the second may turn on more).

def BitSequence.Dominates {n : Nat} (a b : BitSequence n) : Prop :=
  ∀ i, a i = true → b i = true

Outer dependencies: BitSequence

Inner dependencies: Bit

Lean core dependencies: Eq, Fin, Nat

Used by: BitSequence.Dominates.bot, BitSequence.trueCount_strict, Component.Func.Monotone, Component.Func.exists_settle, Component.Func.iterate_dominates_succ

The sequence with every wire off: it lines up with every other sequence, no matter what that other sequence says.

theorem BitSequence.Dominates.bot {n : Nat} (a : BitSequence n) :
    BitSequence.Dominates (fun _ => false) a :=

Dependencies: BitSequence, BitSequence.Dominates

Proof dependencies: Bit

Lean core dependencies: Bool, Eq, Eq.trans, False, False.elim, Fin, Nat, Not, True, absurd, congrArg, eq_false', noConfusion_of_Nat, not_false_eq_true, of_eq_true

Used by: Component.Func.iterate_dominates_succ

A rule never changes its mind: feeding it a sequence that lines up with another always produces an output that lines up the same way.

def Component.Func.Monotone {n : Nat} (f : BitFunction n n) : Prop :=
  ∀ a b, BitSequence.Dominates a b → BitSequence.Dominates (f a) (f b)

Outer dependencies: BitFunction

Inner dependencies: BitSequence, BitSequence.Dominates

Lean core dependencies: Nat

Used by: Component.Func.exists_settle, Component.Func.fixedPoint, Component.Func.fixedPoint_isFixed, Component.Func.iterate_dominates_succ, Component.Func.iterate_settles, Component.Spec.fixedPoint_realizable

How many wires are on in a bit sequence.

def BitSequence.trueCount {n : Nat} (x : BitSequence n) : Nat :=
  (Finset.univ.filter (fun i => x i = true)).card

Outer dependencies: BitSequence

Inner dependencies: Bit

Mathlib dependencies: Finset.card, Finset.filter, Finset.univ

Lean core dependencies: Eq, Fin, Nat

Used by: BitSequence.trueCount_le, BitSequence.trueCount_strict, Component.Func.exists_settle

No sequence has more than n wires on — there are only n wires to begin with.

theorem BitSequence.trueCount_le {n : Nat} (x : BitSequence n) : x.trueCount ≤ n := by

Dependencies: BitSequence, BitSequence.trueCount

Proof dependencies: Bit

Mathlib dependencies: Finset.card, Finset.card_filter_le, Finset.univ, Fintype.card_fin

Lean core dependencies: Eq, Eq.trans, Fin, Nat, True, congrArg, congrFun', eq_self, of_eq_true

Used by: Component.Func.exists_settle

If domination is genuine (the two sequences actually differ), strictly more wires are on afterwards: some wire had to turn on somewhere, and domination never turns one back off.

theorem BitSequence.trueCount_strict {n : Nat} {a b : BitSequence n}
    (h : BitSequence.Dominates a b) (hne : a ≠ b) : a.trueCount < b.trueCount := by

Dependencies: BitSequence, BitSequence.Dominates, BitSequence.trueCount

Proof dependencies: Bit

Mathlib dependencies: Finset, Finset.card_lt_card, Finset.ext_iff, Finset.filter, Finset.mem_filter, Finset.mem_univ, Finset.univ, Fintype

Lean core dependencies: And, Bool, DecidablePred, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, False.elim, Fin, Iff, Nat, Ne, Not, Or, True, congr, congrArg, congrFun', eq_false', eq_self, eq_true, funext, id, iff_false, iff_true, noConfusion_of_Nat, not_true_eq_false, of_eq_true, true_and

Used by: Component.Func.exists_settle

Run f on its own output, k times over, starting from every wire off.

def Component.Func.iterate {n : Nat} (f : BitFunction n n) (k : Nat) : BitSequence n :=
  f^[k] (fun _ => false)

Outer dependencies: BitFunction, BitSequence

Inner dependencies: Bit

Mathlib dependencies: Nat.iterate

Lean core dependencies: Fin, Nat

Used by: Component.Func.exists_settle, Component.Func.fixedPoint, Component.Func.fixedPoint_isFixed, Component.Func.iterate_dominates_succ, Component.Func.iterate_settles, Component.Func.iterate_stays

Iterating a monotone rule never turns a wire back off from one step to the next.

theorem Component.Func.iterate_dominates_succ {n : Nat} {f : BitFunction n n}
    (hf : Component.Func.Monotone f) (k : Nat) :
    BitSequence.Dominates (Component.Func.iterate f k) (Component.Func.iterate f (k + 1)) := by

Dependencies: BitFunction, BitSequence.Dominates, Component.Func.Monotone, Component.Func.iterate

Proof dependencies: Bit, BitSequence.Dominates.bot

Mathlib dependencies: Function.iterate_succ_apply', Nat.iterate

Lean core dependencies: Eq, Eq.mpr, Fin, Nat, Nat.recAux, congrArg, id

Used by: Component.Func.exists_settle

Once iterating a rule agrees with itself one step later, it agrees with that same value at every step after — running a rule on its own fixed value never leaves it.

theorem Component.Func.iterate_stays {n : Nat} (f : BitFunction n n) {k : Nat}
    (hk : Component.Func.iterate f (k + 1) = Component.Func.iterate f k) :
    ∀ j, k ≤ j → Component.Func.iterate f j = Component.Func.iterate f k := by

Dependencies: BitFunction, BitSequence, Component.Func.iterate

Proof dependencies: Bit

Mathlib dependencies: Function.iterate_succ_apply', Nat.iterate, Nat.le_induction

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.trans, Fin, Nat, True, congrArg, congrFun', eq_self, id, of_eq_true

Used by: Component.Func.iterate_settles

Among the first n + 1 steps of iterating a monotone rule, at least one already agrees with the step right after it: the number of on-wires only ever climbs (never falls) with each step, and there are only n wires to turn on, so it cannot climb strictly more than n times running.

theorem Component.Func.exists_settle {n : Nat} {f : BitFunction n n}
    (hf : Component.Func.Monotone f) :
    ∃ k ≤ n, Component.Func.iterate f (k + 1) = Component.Func.iterate f k := by

Dependencies: BitFunction, BitSequence, Component.Func.Monotone, Component.Func.iterate

Proof dependencies: Bit, BitSequence.Dominates, BitSequence.trueCount, BitSequence.trueCount_le, BitSequence.trueCount_strict, Component.Func.iterate_dominates_succ

Mathlib dependencies: Mathlib.Tactic.Push.not_and_eq, le_refl

Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mp, Eq.symm, Eq.trans, Exists, Fin, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.le_of_succ_le, Nat.lt_of_not_le, Nat.recAux, Nat.zero_le, Ne, Ne.symm, Not, binderNameHint, forall_congr, id, le_of_le_of_eq, of_decide_eq_true

Used by: Component.Func.iterate_settles

Running a monotone rule long enough (n + 1 times, where n is the number of wires) always settles down: it reaches a value it agrees with even one more step later. This is the whole point of requiring Component.Func.Monotone — the number of on-wires can only ever climb, never fall, so it cannot climb strictly for more than n steps in a row before running out of wires to turn on, at which point it has nowhere left to go but to repeat itself.

theorem Component.Func.iterate_settles {n : Nat} {f : BitFunction n n}
    (hf : Component.Func.Monotone f) :
    Component.Func.iterate f (n + 1) = Component.Func.iterate f n := by

Dependencies: BitFunction, BitSequence, Component.Func.Monotone, Component.Func.iterate

Proof dependencies: Component.Func.exists_settle, Component.Func.iterate_stays

Lean core dependencies: And, Eq, Eq.mpr, Exists, Nat, Nat.le_succ_of_le, congrArg, id

Used by: Component.Func.fixedPoint_isFixed

The fixed value a monotone rule settles into, run enough times from every wire off.

def Component.Func.fixedPoint {n : Nat} (f : BitFunction n n) (_ : Component.Func.Monotone f) :
    BitSequence n :=
  Component.Func.iterate f n

Outer dependencies: BitFunction, BitSequence, Component.Func.Monotone

Inner dependencies: Component.Func.iterate

Lean core dependencies: Nat

Used by: Component.Func.fixedPoint_isFixed, Component.Spec.fixedPoint_realizable

Running f on its own fixed value changes nothing at all: Component.Func.fixedPoint really is a fixed point, and f is enough on its own to hand it back — nothing further needs to be run to find it, just f applied to itself’s own eventual output, enough times over.

theorem Component.Func.fixedPoint_isFixed {n : Nat} {f : BitFunction n n}
    (hf : Component.Func.Monotone f) :
    f (Component.Func.fixedPoint f hf) = Component.Func.fixedPoint f hf := by

Dependencies: Bit, BitFunction, Component.Func.Monotone, Component.Func.fixedPoint

Proof dependencies: BitSequence, Component.Func.iterate, Component.Func.iterate_settles

Mathlib dependencies: Function.iterate_succ_apply', Nat.iterate

Lean core dependencies: Eq, Eq.mpr, Eq.trans, Fin, Nat, True, congrArg, eq_self, id, of_eq_true

Used by: Component.Spec.fixedPoint_realizable

The same equation, stated as a constraint instead of built

Component.Func.fixedPoint only exists for a monotone rule, and only because it’s actually built, by running f enough times over. A Component.Spec can state the very same equation — what a fixed point of f would have to satisfy — for any rule at all, monotone or not, with no promise that anything ever satisfies it. Whether it does is a separate question, answered by Component.Spec.Realizable, not baked into the statement itself.

The defining equation of a fixed point, as a bare constraint: an output counts exactly when running f on it gives that same output back. Nothing here says one exists.

def Component.Spec.fixedPoint {n : Nat} (f : BitFunction n n) : Component.Spec Bit Bit 0 n :=
  fun _ o => f o = o

Outer dependencies: Bit, BitFunction, Component.Spec

Lean core dependencies: Eq, Fin, Nat

Used by: Component.Spec.fixedPoint_realizable, notRule_fixedPoint_unrealizable

Whenever f is monotone, its Component.Spec.fixedPoint is realizable after all — witnessed by Component.Func.fixedPoint, the same value found by actually running f.

theorem Component.Spec.fixedPoint_realizable {n : Nat} {f : BitFunction n n}
    (hf : Component.Func.Monotone f) : (Component.Spec.fixedPoint f).Realizable :=

Dependencies: Bit, BitFunction, Component.Func.Monotone, Component.Spec.Realizable, Component.Spec.fixedPoint

Proof dependencies: Component.Func.fixedPoint, Component.Func.fixedPoint_isFixed

Lean core dependencies: Fin, Nat

Used by: (none)

Example.

The rule that flips a single bit has no fixed point at all: fed true it hands back false, fed false it hands back true, never agreeing with its own input either way.

def notRule : BitFunction 1 1 := fun iv _ => !(iv 0)

Outer dependencies: BitFunction

Inner dependencies: Bit

Lean core dependencies: Bool.not, Fin, Nat

Used by: notRule_fixedPoint_unrealizable

Example.

Unlike a monotone rule, notRule’s own Component.Spec.fixedPoint is genuinely unrealizable — a bare constraint, unlike an actually-built rule, is free to have nothing satisfy it at all.

theorem notRule_fixedPoint_unrealizable :
    ¬ (Component.Spec.fixedPoint notRule).Realizable := by

Dependencies: Bit, Component.Spec.Realizable, Component.Spec.fixedPoint, notRule

Lean core dependencies: Bool, Bool.not, Decidable.decide, Eq, Eq.symm, Exists, False, Fin, Fin.elim0, Nat, Not, congrFun, id, of_decide_eq_true

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll) to zoom, click a node to jump to it.

definitionlemmatheoremexampledeclared elsewheredependencyproof dependency
legend