ForestCovers

Abstract

Priority-forest interval structure and counting.

Definition 1.1 (IntervalForest / support).

$$\forall (n:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn),\mathrm{support}P=Finset.univ.filter(\mathrm{fun}(v:\mathrm{Fin}(n+1))\mapsto P.parentv\ne \mathrm{none})$$

Formalization. D5/S3/Combinatorics/PriorityLattice/ForestCovers.support (✓ 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 by classical exact Finset.univ.filter (fun v => P.parent v ≠ none).

Theorem 1.2 (IntervalForest / mem_support).

$$\forall \{n:\mathbb{N}\}(P:IntervalForestBasic.IntervalForestn)(v:\mathrm{Fin}(n+1)),v\in ForestCovers.IntervalForest.supportP⟺P.parentv\ne \mathrm{none}$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.mem_support (✓ 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.3 (IntervalForest / le_iff_parent).

$$\forall \{n:\mathbb{N}\}(PQ:IntervalForestBasic.IntervalForestn),P\le Q⟺\forall (vp:\mathrm{Fin}(n+1)),P.parentv=\mathrm{some}p\to Q.parentv=\mathrm{some}p$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.le_iff_parent (✓ 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.4 (IntervalForest / support_mono).

$$\forall \{n:\mathbb{N}\}\{PQ:IntervalForestBasic.IntervalForestn\},P\le Q\to ForestCovers.IntervalForest.supportP\subseteq ForestCovers.IntervalForest.supportQ$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.support_mono (✓ 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 / edgeCount).

$$\forall (n:\mathrm{Nat})(P:\mathrm{IntervalForest}n),\mathrm{edgeCount}P=(\mathrm{support}P).\mathrm{card}$$

Formalization. D5/S3/Combinatorics/PriorityLattice/ForestCovers.edgeCount (✓ 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 (support P).card.

Theorem 1.6 (IntervalForest / covBy_iff_edgeCount).

$$\forall \{n:\mathbb{N}\}\{PQ:IntervalForestBasic.IntervalForestn\},P\mathrm{CovBy}Q⟺P<Q\wedge ForestCovers.IntervalForest.edgeCountQ=ForestCovers.IntervalForest.edgeCountP+1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.covBy_iff_edgeCount (✓ 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.7 (IntervalForest / edgeCount_le).

$$\forall \{n:\mathbb{N}\}(P:IntervalForestBasic.IntervalForestn),ForestCovers.IntervalForest.edgeCountP\le n$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.edgeCount_le (✓ 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.8 (IntervalForest / edgeCount_eq_iff_tree).

$$\forall \{n:\mathbb{N}\}(P:IntervalForestBasic.IntervalForestn),ForestCovers.IntervalForest.edgeCountP=n⟺IntervalForestBasic.IsTreeP$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.edgeCount_eq_iff_tree (✓ 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.9 (rank).

$$\forall (n:\mathrm{Nat})(x:\mathrm{WithTop}(IntervalForestBasic.IntervalForestn)),\mathrm{rank}x=Option.elim(x:\mathrm{Option}(IntervalForestBasic.IntervalForestn))(n+1)ForestCovers.IntervalForest.edgeCount$$

Formalization. D5/S3/Combinatorics/PriorityLattice/ForestCovers.rank (✓ 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 (x : Option (IntervalForest n)).elim (n+1) IntervalForest.edgeCount.

Theorem 1.10 (coatom_iff_tree).

$$\forall (n:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn),\mathrm{IsCoatom}(P:\mathrm{WithTop}(IntervalForestBasic.IntervalForestn))⟺IntervalForestBasic.IsTreeP$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.coatom_iff_tree (✓ 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 (covBy_rank).

$$\forall \{n:\mathbb{N}\}\{xy:\mathrm{WithTop}(IntervalForestBasic.IntervalForestn)\},x\mathrm{CovBy}y\to ForestCovers.ranky=ForestCovers.rankx+1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.covBy_rank (✓ 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 (atom_card_orderIso).

$$\forall \{A:\mathrm{Type}\}\{B:\mathrm{Type}\}[\mathrm{PartialOrder}A][\mathrm{PartialOrder}B][\mathrm{OrderBot}A][\mathrm{OrderBot}B],(A{\equiv }_{o}B)\to Nat.card\{a:A\mid \mathrm{IsAtom}a\}=Nat.card\{b:B\mid \mathrm{IsAtom}b\}$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.atom_card_orderIso (✓ 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.13 (IntervalForest / eq_of_same_support_below).

$$\forall \{n:\mathbb{N}\}\{PQR:IntervalForestBasic.IntervalForestn\},Q\le P\to R\le P\to ForestCovers.IntervalForest.supportQ=ForestCovers.IntervalForest.supportR\to Q=R$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.eq_of_same_support_below (✓ 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.14 (IntervalForest / lower_covers_card_le).

$$\forall \{n:\mathbb{N}\}(P:IntervalForestBasic.IntervalForestn),Nat.card\{Q:IntervalForestBasic.IntervalForestn\mid Q\mathrm{CovBy}P\}\le ForestCovers.IntervalForest.edgeCountP$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.lower_covers_card_le (✓ 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.15 (ideal_iso_rank).

$$\forall \{nm:\mathbb{N}\}\{x:\mathrm{WithTop}(IntervalForestBasic.IntervalForestn)\},(CoeSort.coe\left(Set.Iicx\right){\equiv }_o\mathrm{WithTop}(IntervalForestBasic.IntervalForestm))\to ForestCovers.rankx=m+1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.ideal_iso_rank (✓ 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.16 (filter_iso_rank).

$$\forall \{nm:\mathbb{N}\}\{x:\mathrm{WithTop}(IntervalForestBasic.IntervalForestn)\},(CoeSort.coe\left(Set.Icix\right){\equiv }_o\mathrm{WithTop}(IntervalForestBasic.IntervalForestm))\to m+1=n+1-ForestCovers.rankx$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.filter_iso_rank (✓ 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.17 (top_filter_not_iso).

$$\forall (nm:\mathrm{Nat}),\neg \mathrm{Nonempty}(Set.Ici(Top.top:\mathrm{WithTop}(IntervalForestBasic.IntervalForestn)){\equiv }_o\mathrm{WithTop}(IntervalForestBasic.IntervalForestm))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.top_filter_not_iso (✓ 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.18 (forest_ideal_index_le_two).

$$\forall (nm:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn),(Set.Iic(P:\mathrm{WithTop}(IntervalForestBasic.IntervalForestn)){\equiv }_o\mathrm{WithTop}(IntervalForestBasic.IntervalForestm))\to m\le 2$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.forest_ideal_index_le_two (✓ 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.19 (IntervalForest / cover_adjacent_roots).

$$\forall \{n:\mathbb{N}\}\{PQ:IntervalForestBasic.IntervalForestn\},P\mathrm{CovBy}Q\to \exists (vp:\mathrm{Fin}(n+1)),P.parentv=\mathrm{none}\wedge Q.parentv=\mathrm{some}p\wedge p<v\wedge (\forall (w:\mathrm{Fin}(n+1)),p<w\to w<v\to P.parentw\ne \mathrm{none})\wedge (\forall (w:\mathrm{Fin}(n+1)),w\ne v\to Q.parentw=P.parentw)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/ForestCovers.cover_adjacent_roots (✓ 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/ForestCovers.atom_card_orderIso
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.coatom_iff_tree
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.covBy_iff_edgeCount
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.covBy_rank
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.cover_adjacent_roots
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.edgeCount
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.edgeCount_eq_iff_tree
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.edgeCount_le
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.eq_of_same_support_below
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.filter_iso_rank
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.forest_ideal_index_le_two
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.ideal_iso_rank
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.le_iff_parent
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.lower_covers_card_le
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.mem_support
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.rank
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.support
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.support_mono
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/ForestCovers.top_filter_not_iso
• Dependency: D5/S3/Combinatorics/PriorityLattice/IntervalForestBasic