IntervalForestBasic

Abstract

Priority-forest interval structure and counting.

Definition 1.1 (IntervalForest).

$$\forall (n:\mathrm{Nat})(\mathrm{parent}:\mathrm{Fin}(n+1)\to \mathrm{Option}(\mathrm{Fin}(n+1)))(\mathrm{increasing}:\forall (vp:\mathrm{Fin}(n+1)),\mathrm{parent}v=\mathrm{some}p\to p<v)(\mathrm{intervals}:\forall (uvw:\mathrm{Fin}(n+1)),u\le v\to v\le w\to Relation.EqvGen(\mathrm{fun}(ab:\mathrm{Fin}(n+1))\mapsto \mathrm{parent}b=\mathrm{some}a)uw\to Relation.EqvGen(\mathrm{fun}(ab:\mathrm{Fin}(n+1))\mapsto \mathrm{parent}b=\mathrm{some}a)uv),(IntervalForest.mk\mathrm{parent}\mathrm{increasing}\mathrm{intervals}).\mathrm{parent}=\mathrm{parent}$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.IntervalForest (✓ std3).

Citation. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

Section 2.1, pp. 3–4: a priority forest (labeled with [n]₀ and with m edges) is a rooted forest (T₀, T₁, …, Tₙ₋ₘ) with all component trees increasing and ordered according to the root’s labels, and where for all j<k, every label in Tⱼ is smaller than every label in Tₖ. Thus, the vertex set of each tree is an interval of integers. The parent-function fields use Fin (n + 1), a smaller parent for each non-root, and Relation.EqvGen for connected components.

Theorem 1.2 (IntervalForest / ext).

$$\forall \{n:\mathbb{N}\}\{PQ:IntervalForestBasic.IntervalForestn\},P.parent=Q.parent\to P=Q$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.ext (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The quantified statement holds for every parameter satisfying its displayed hypotheses.

Definition 1.3 (IntervalForest / edges).

$$\forall (n:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn),\mathrm{edges}P=\{e:\mathrm{Fin}(n+1)\times \mathrm{Fin}(n+1)\mid P.parente.2=\mathrm{some}e.1\}$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.edges (✓ std3).

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The defining expression is {e | P.parent e.2 = some e.1}.

Theorem 1.4 (IntervalForest / edges_injective).

$$\forall (n:\mathrm{Nat}),Function.Injective(\mathrm{fun}(P:IntervalForestBasic.IntervalForestn)\mapsto IntervalForestBasic.IntervalForest.edgesP)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.edges_injective (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The quantified statement holds for every parameter satisfying its displayed hypotheses.

Definition 1.5 (IntervalForest / forestPartialOrder).

$$\forall (n:\mathrm{Nat})(PQ:IntervalForestBasic.IntervalForestn),P\le Q⟺IntervalForestBasic.IntervalForest.edgesP\subseteq IntervalForestBasic.IntervalForest.edgesQ$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.forestPartialOrder (✓ std3).

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The defining expression is PartialOrder.lift edges edges_injective.

Definition 1.6 (filterCount).

$$\forall (n:\mathrm{Nat}),\mathrm{filterCount}n=Nat.card\{x:\mathrm{WithTop}(\mathrm{IntervalForest}n)\mid \exists (m:\mathrm{Nat}),m\le n\wedge \mathrm{Nonempty}(Set.Icix{\equiv }_o\mathrm{WithTop}(\mathrm{IntervalForest}m))\}$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.filterCount (✓ std3).

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The defining expression is Nat.card {x : (WithTop (IntervalForest n)) // ∃ m ≤ n, Nonempty (Set.Ici x ≃o (WithTop (IntervalForest m)))}.

Definition 1.7 (idealCount).

$$\forall (n:\mathrm{Nat}),\mathrm{idealCount}n=Nat.card\{x:\mathrm{WithTop}(\mathrm{IntervalForest}n)\mid \exists (m:\mathrm{Nat}),m\le n\wedge \mathrm{Nonempty}(Set.Iicx{\equiv }_o\mathrm{WithTop}(\mathrm{IntervalForest}m))\}$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.idealCount (✓ std3).

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The defining expression is Nat.card {x : (WithTop (IntervalForest n)) // ∃ m ≤ n, Nonempty (Set.Iic x ≃o (WithTop (IntervalForest m)))}.

Definition 1.8 (positiveIdealCount).

$$\forall (n:\mathrm{Nat}),\mathrm{positiveIdealCount}n=Nat.card\{x:\mathrm{WithTop}(\mathrm{IntervalForest}n)\mid \exists (m:\mathrm{Nat}),1\le m\wedge m\le n\wedge \mathrm{Nonempty}(Set.Iicx{\equiv }_o\mathrm{WithTop}(\mathrm{IntervalForest}m))\}$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.positiveIdealCount (✓ std3).

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The defining expression is Nat.card {x : (WithTop (IntervalForest n)) // exists m, 1 <= m ∧ m <= n ∧ Nonempty (Set.Iic x ≃o (WithTop (IntervalForest m)))}.

Definition 1.9 (IntervalForest / empty).

$$\forall (n:\mathrm{Nat})(v:\mathrm{Fin}(n+1)),(IntervalForest.emptyn).\mathrm{parent}v=\mathrm{none}$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.empty (✓ std3).

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The defining expression is parent := fun _ => none increasing := by simp intervals := by intro u v w huv hvw h have hempty : forall a b : Fin (n+1), Relation.EqvGen (fun a _ => (none : Option (Fin (n+1))) = some a) a b -> a = b := by intro a b hab induction hab with | rel x y h => cases h | refl x => rfl | symm x y _ ih => exact ih.symm | trans x y z _ _ ih1 ih2 => exact ih1.trans ih2 have huw : u = w := hempty u w h have huv’ : u = v := le_antisymm huv (huw ▸ hvw) subst v exact Relation.EqvGen.refl _.

Theorem 1.10 (IntervalForest / parent_zero).

$$\forall \{n:\mathbb{N}\}(P:IntervalForestBasic.IntervalForestn),P.parent0=\mathrm{none}$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.parent_zero (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The quantified statement holds for every parameter satisfying its displayed hypotheses.

Theorem 1.11 (IntervalForest / card_zero).

$$Nat.card(IntervalForestBasic.IntervalForest0)=1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.card_zero (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The quantified statement holds for every parameter satisfying its displayed hypotheses.

Theorem 1.12 (IntervalForest / no_skipped_root).

$$\forall \{n:\mathbb{N}\}(P:IntervalForestBasic.IntervalForestn)\{vpw:\mathrm{Fin}(n+1)\},P.parentv=\mathrm{some}p\to p<w\to w\le v\to P.parentw\ne \mathrm{none}$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.no_skipped_root (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The quantified statement holds for every parameter satisfying its displayed hypotheses.

Definition 1.13 (forestOfLocal).

$$\forall (n:\mathrm{Nat})(f:\mathrm{Fin}(n+1)\to \mathrm{Option}(\mathrm{Fin}(n+1)))(\mathrm{inc}:\forall (vp:\mathrm{Fin}(n+1)),fv=\mathrm{some}p\to p<v)(\mathrm{nskip}:\forall (vpw:\mathrm{Fin}(n+1)),fv=\mathrm{some}p\to p<w\to w\le v\to fw\ne \mathrm{none}),(\mathrm{forestOfLocal}f\mathrm{inc}\mathrm{nskip}).\mathrm{parent}=f$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.forestOfLocal (✓ std3).

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The literal parent function and increasing-parent proof, together with the no-skipped-root condition, construct the forest whose parent field is displayed.

Definition 1.14 (IsTree).

$$\forall (n:\mathrm{Nat})(P:\mathrm{IntervalForest}n),\mathrm{IsTree}P⟺\forall (v:\mathrm{Fin}(n+1)),P.parentv=\mathrm{none}\to v=0$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.IsTree (✓ std3).

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The defining expression is forall v, P.parent v = none -> v = 0.

Definition 1.15 (treeEquivCode).

$$\forall (n:\mathrm{Nat})(T:\{P:IntervalForestBasic.IntervalForestn\mid \mathrm{IsTree}P\})(i:\mathrm{Fin}n),Option.map(\mathrm{fun}p\mapsto \mathrm{val}(p))(\mathrm{parent}(\mathrm{val}(T))i.succ)=\mathrm{some}(\mathrm{val}((\mathrm{treeEquivCode}nTi)))$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.treeEquivCode (✓ std3).

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The equivalence sends each vertex i + 1 to its parent label, which is at most i. The inverse attaches each non-root vertex to its prescribed parent.

Theorem 1.16 (increasing_tree_card).

$$\forall (n:\mathbb{N}),Nat.card\{P:IntervalForestBasic.IntervalForestn\mid IntervalForestBasic.IsTreeP\}=n.factorial$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.increasing_tree_card (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Adrián Lillo and Mercedes Rosas (2026). The Priority Lattice. DOI: 10.48550/arXiv.2603.28905. URL: https://arxiv.org/abs/2603.28905v1.

Commentary.

The quantified statement holds for every parameter satisfying its displayed hypotheses.

References

• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.IntervalForest
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.IsTree
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.card_zero
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.edges
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.edges_injective
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.empty
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.ext
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.filterCount
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.forestOfLocal
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.forestPartialOrder
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.idealCount
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.increasing_tree_card
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.no_skipped_root
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.parent_zero
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.positiveIdealCount
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic.treeEquivCode