Least fixed points by bottom-up iteration

[UPSTREAM] Kleene-style certificates for OrderHom.lfp without continuity hypotheses: the iterates f^[k] ⊥ of a monotone map sit below every prefixed point, so as soon as one is a fixed point it is the least fixed point (OrderHom.lfp_eq_iterate_bot). In a finite lattice some iterate is always fixed — a monotone chain can rise at most Fintype.card times (OrderHom.iterate_bot_fixed).

Together these give the computable face of Knaster–Tarski used by the recursive-scheme and modal-μ semantics (Core/Computability/Subregular/Logic/): compute f^[k] ⊥, check one more application, conclude lfp.

theorem WellFounded.iterate_eventually_constant {α : Type u_1} {lt : α → α → Prop} (wf : WellFounded lt) {f : α → α} (hmove : ∀ (x : α), f x ≠ x → lt (f x) x) (x : α) : ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → f^[m] x = f^[N] x

A well-founded descent has eventually-constant iterates: if f moves every non-fixed point strictly down a well-founded relation, then from any start the orbit reaches a fixed point — there is an N past which further iteration does nothing.

Absent from mathlib: the nearest neighbor is the chain condition (wellFoundedGT_iff_monotone_chain_condition), which is keyed to preorders and ℕ →o α sequences rather than a bare relation and a self-map; the lemma is also the deterministic case of strong normalization, a rewriting theory mathlib lacks.

theorem OrderHom.iterate_bot_le_lfp {L : Type u_1} [CompleteLattice L] (f : L →o L) (k : ℕ) : (⇑f)^[k] ⊥ ≤ lfp f

Bottom-up iterates never overtake the least fixed point.

theorem OrderHom.lfp_eq_iterate_bot {L : Type u_1} [CompleteLattice L] (f : L →o L) {k : ℕ} (h : f ((⇑f)^[k] ⊥) = (⇑f)^[k] ⊥) : lfp f = (⇑f)^[k] ⊥

Iteration certificate for lfp: an iterate of ⊥ that f fixes is the least fixed point. The computable face of Knaster–Tarski: no continuity needed.

theorem OrderHom.iterate_bot_mono {L : Type u_1} [CompleteLattice L] (f : L →o L) : Monotone fun (k : ℕ) => (⇑f)^[k] ⊥

The bottom-up chain is monotone in the iteration count.

theorem OrderHom.iterate_bot_fixed {L : Type u_1} [CompleteLattice L] [Fintype L] (f : L →o L) : f ((⇑f)^[Fintype.card L] ⊥) = (⇑f)^[Fintype.card L] ⊥

In a finite lattice the bottom-up chain reaches a fixed point within Fintype.card L steps: a monotone chain can rise at most card times.

theorem OrderHom.lfp_eq_iterate_bot_card {L : Type u_1} [CompleteLattice L] [Fintype L] (f : L →o L) : lfp f = (⇑f)^[Fintype.card L] ⊥

In a finite lattice, lfp is computed by Fintype.card-fold iteration from ⊥.