LowRankForests

Abstract

Priority-forest interval structure and counting.

Definition 1.1 (OneLongAt).

$$\forall (n:\mathrm{Nat})(P:\mathrm{IntervalForest}n)(v:\mathrm{Fin}(n+1)),\mathrm{OneLongAt}Pv⟺(\exists (p:\mathrm{Fin}(n+1)),P.parentv=\mathrm{some}p\wedge \mathrm{val}(p)+2=\mathrm{val}(v))\wedge (\forall (wp:\mathrm{Fin}(n+1)),w\ne v\to P.parentw=\mathrm{some}p\to \mathrm{val}(p)+1=\mathrm{val}(w))$$

Formalization. D5/S3/Combinatorics/PriorityLattice/LowRankForests.OneLongAt (✓ 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.

OneLongAt means that v has a parent two labels below it, and every other non-root has a parent one label below it.

Definition 1.2 (OneLong).

$$\forall (n:\mathrm{Nat})(P:\mathrm{IntervalForest}n),\mathrm{OneLong}P⟺\exists (v:\mathrm{Fin}(n+1)),\mathrm{OneLongAt}Pv$$

Formalization. D5/S3/Combinatorics/PriorityLattice/LowRankForests.OneLong (✓ 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 ∃ v, OneLongAt P v.

Definition 1.3 (CodeOneStep).

$$\forall (k:\mathrm{Nat})(t:((v:\mathrm{Fin}k)\to \mathrm{Fin}(\mathrm{val}(v)+1))),\mathrm{CodeOneStep}t⟺\exists ij:\mathrm{Fin}k,\mathrm{val}(i)+1=\mathrm{val}(j)\wedge \mathrm{val}((tj))=\mathrm{val}(i)\wedge (\forall (z:\mathrm{Fin}k),z\ne j\to \mathrm{val}((tz))=\mathrm{val}(z))$$

Formalization. D5/S3/Combinatorics/PriorityLattice/LowRankForests.CodeOneStep (✓ 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.

CodeOneStep has one pair of adjacent indices i and j with val(t j) = val(i); every other index z has val(t z) = val(z).

Theorem 1.4 (IntervalForest / one_long_iff_code_one_step).

$$\forall \{nk:\mathbb{N}\}(P:IntervalForestBasic.IntervalForestn)(h:ForestCovers.IntervalForest.edgeCountP=k),LowRankForests.OneLongP⟺LowRankForests.CodeOneStep(IdealCompression.IntervalForest.compressCodePh)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/LowRankForests.one_long_iff_code_one_step (✓ 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.5 (SmallIdealCodes / oneStep_two_iff).

$$\forall (t:(v:\mathrm{Fin}2)\to \mathrm{Fin}(\mathrm{val}(v)+1)),LowRankForests.CodeOneStept⟺t=IdealCompression.SmallIdealCodes.t20$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/LowRankForests.oneStep_two_iff (✓ 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.6 (SmallIdealCodes / oneStep_three_iff).

$$\forall (t:(v:\mathrm{Fin}3)\to \mathrm{Fin}(\mathrm{val}(v)+1)),LowRankForests.CodeOneStept⟺t=IdealCompression.SmallIdealCodes.t302\vee t=IdealCompression.SmallIdealCodes.t311$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/LowRankForests.oneStep_three_iff (✓ 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 (long_two_card).

$$\forall (n:\mathbb{N}),Nat.card\{P:IntervalForestBasic.IntervalForestn\mid ForestCovers.IntervalForest.edgeCountP=2\wedge LowRankForests.OneLongP\}=n-1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/LowRankForests.long_two_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.

Theorem 1.8 (long_three_card).

$$\forall (n:\mathbb{N}),Nat.card\{P:IntervalForestBasic.IntervalForestn\mid ForestCovers.IntervalForest.edgeCountP=3\wedge LowRankForests.OneLongP\}=(n-1)\cdot (n-2)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/LowRankForests.long_three_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.

Theorem 1.9 (single_edges_card).

$$\forall (n:\mathbb{N}),Nat.card\{P:IntervalForestBasic.IntervalForestn\mid ForestCovers.IntervalForest.edgeCountP=1\}=n$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/LowRankForests.single_edges_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/LowRankForests.CodeOneStep
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/LowRankForests.OneLong
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/LowRankForests.OneLongAt
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/LowRankForests.long_three_card
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/LowRankForests.long_two_card
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/LowRankForests.oneStep_three_iff
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/LowRankForests.oneStep_two_iff
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/LowRankForests.one_long_iff_code_one_step
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/LowRankForests.single_edges_card
• Dependency: D5/S3/Combinatorics/PriorityLattice/IdealCompression