IdealCompression

Abstract

Priority-forest interval structure and counting.

Definition 1.1 (CodeClosed).

$$\forall (k:\mathrm{Nat})(t:((v:\mathrm{Fin}k)\to \mathrm{Fin}(\mathrm{val}(v)+1)))(s:\mathrm{Finset}(\mathrm{Fin}k)),\mathrm{CodeClosed}ts⟺\forall (v:\mathrm{Fin}k),v\in s\to \forall (w:\mathrm{Fin}k),\mathrm{val}((tv))\le \mathrm{val}(w)\to w\le v\to w\in s$$

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

A subset is CodeClosed when it contains every index between the parent code val(t v) and each of its members v.

Definition 1.2 (IntervalForest / supportParent).

$$\forall (n:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn)(v:CoeSort.coe\left(ForestCovers.IntervalForest.supportP\right)),\mathrm{supportParent}Pv=Exists.choose({Option.{\left({\left(\mathrm{n}{\mathrm{e}}_{\mathrm{none}}\right)}_{\mathrm{iff}}\right)}_{\mathrm{exists}}}^{\prime }.\mathrm{mp}((ForestCovers.IntervalForest.me{\mathrm{m}}_{\mathrm{support}}P\mathrm{val}(v)).\mathrm{mp}v.property))$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IdealCompression.supportParent (✓ 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 chosen parent is extracted from the existence of a parent for each support member; the displayed value projection passes that member to the forest parent function.

Theorem 1.3 (IntervalForest / supportParent_spec).

$$\forall \{n:\mathbb{N}\}(P:IntervalForestBasic.IntervalForestn)(v:CoeSort.coe\left(ForestCovers.IntervalForest.supportP\right)),P.parent\mathrm{val}(v)=\mathrm{some}(IdealCompression.IntervalForest.supportParentPv)$$

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

$$\forall (n:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn)(v:CoeSort.coe\left(ForestCovers.IntervalForest.supportP\right)),\mathrm{val}((\mathrm{firstNeeded}Pv))=\mathrm{val}((\mathrm{supportParent}Pv))+1$$

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

firstNeeded has value val(supportParent P v) + 1; increasing parents place this label within Fin (n + 1).

Definition 1.5 (IntervalForest / firstIndex).

$$\forall (nk:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn)(h:ForestCovers.IntervalForest.edgeCountP=k)(i:\mathrm{Fin}k),\mathrm{val}((Finset.orderIsoOfFin(ForestCovers.IntervalForest.supportP)h(\mathrm{firstIndex}Phi)))=\mathrm{firstNeeded}P(Finset.orderIsoOfFin(ForestCovers.IntervalForest.supportP)hi)$$

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

firstIndex sends i to the index, under Finset.orderIsoOfFin, of firstNeeded P applied to the support label at index i.

Definition 1.6 (IntervalForest / compressCode).

$$\forall (nk:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn)(h:ForestCovers.IntervalForest.edgeCountP=k)(i:\mathrm{Fin}k),\mathrm{val}((\mathrm{compressCode}Phi))=\mathrm{val}((\mathrm{firstIndex}Phi))$$

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

compressCode sends i to the finite code with value val(firstIndex P h i). The bound on firstIndex makes this value an element of Fin (val(i) + 1).

Definition 1.7 (IntervalForest / idealCodeOrderIso).

$$\forall (nk:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn)(h:ForestCovers.IntervalForest.edgeCountP=k)(Q:IntervalForestBasic.IntervalForestn)(\mathrm{hQ}:Q\le P),\mathrm{val}((\mathrm{idealCodeOrderIso}Ph(Subtype.mk(Q:\mathrm{WithTop}(IntervalForestBasic.IntervalForestn))(WithTop.{\left(\mathrm{co}{\mathrm{e}}_{\mathrm{le}}\right)}_{\mathrm{coe}}.mpr\mathrm{hQ}))))=Finset.univ.filter(\mathrm{fun}(i:\mathrm{Fin}k)\mapsto \mathrm{val}((Finset.orderIsoOfFin(ForestCovers.IntervalForest.supportP)hi))\in ForestCovers.IntervalForest.supportQ)$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IdealCompression.idealCodeOrderIso (✓ 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 isomorphism sends a subforest to the occupied child indices in the increasing enumeration of the host support. Closed subsets preserve the interval-component condition.

Theorem 1.8 (pi_one_card).

$$Nat.card(\mathrm{WithTop}(IntervalForestBasic.IntervalForest1))=3$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IdealCompression.pi_one_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 (pi_two_card).

$$Nat.card(\mathrm{WithTop}(IntervalForestBasic.IntervalForest2))=6$$

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

Definition 1.10 (SmallIdealCodes / t1).

$$\forall (i:\mathrm{Fin}1),SmallIdealCodes.t1i=0$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IdealCompression.t1 (✓ 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 fun _ => 0.

Definition 1.11 (SmallIdealCodes / t20).

$$\forall (i:\mathrm{Fin}2),SmallIdealCodes.t20i=0$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IdealCompression.t20 (✓ 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 fun _ => 0.

Definition 1.12 (SmallIdealCodes / t21).

$$\forall (i:\mathrm{Fin}2),\mathrm{val}((SmallIdealCodes.t21i))=\mathrm{val}(i)$$

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

t21 is the dependent identity code: val(t21 i) = val(i).

Definition 1.13 (SmallIdealCodes / t3).

$$\forall (a:\mathrm{Fin}2)(b:\mathrm{Fin}3)(i:\mathrm{Fin}3),\mathrm{val}((SmallIdealCodes.t3abi))=(\mathrm{if}\mathrm{val}(i)=0\mathrm{then}0\mathrm{else}\mathrm{if}\mathrm{val}(i)=1\mathrm{then}\mathrm{val}(a)\mathrm{else}\mathrm{val}(b))$$

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

t3 has value 0 at index 0, value val(a) at index 1, and value val(b) at index 2.

Theorem 1.14 (SmallIdealCodes / code_one).

$$\forall (t:(v:\mathrm{Fin}1)\to \mathrm{Fin}(\mathrm{val}(v)+1)),t=IdealCompression.SmallIdealCodes.t1$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IdealCompression.code_one (✓ 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 (SmallIdealCodes / code_two).

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

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IdealCompression.code_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.16 (SmallIdealCodes / code_three).

$$\forall (t:(v:\mathrm{Fin}3)\to \mathrm{Fin}(\mathrm{val}(v)+1)),\exists (a:\mathrm{Fin}2)(b:\mathrm{Fin}3),t=IdealCompression.SmallIdealCodes.t3ab$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IdealCompression.code_three (✓ 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 (SmallIdealCodes / card_two_iff).

$$\forall (t:(v:\mathrm{Fin}2)\to \mathrm{Fin}(\mathrm{val}(v)+1)),Nat.card\{s:\mathrm{Finset}(\mathrm{Fin}2)\mid IdealCompression.CodeClosedts\}=3⟺t=IdealCompression.SmallIdealCodes.t20$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IdealCompression.card_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.18 (SmallIdealCodes / card_three_iff).

$$\forall (t:(v:\mathrm{Fin}3)\to \mathrm{Fin}(\mathrm{val}(v)+1)),Nat.card\{s:\mathrm{Finset}(\mathrm{Fin}3)\mid IdealCompression.CodeClosedts\}=6⟺t=IdealCompression.SmallIdealCodes.t302\vee t=IdealCompression.SmallIdealCodes.t311$$

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

Definition 1.19 (SmallIdealCodes / twoTripleModelsIso).

$$\forall (s:\{s:\mathrm{Finset}(\mathrm{Fin}3)\mid \mathrm{CodeClosed}(SmallIdealCodes.t302)s\}),\mathrm{val}((SmallIdealCodes.twoTripleModelsIsos))=Finset.image(\mathrm{fun}(i:\mathrm{Fin}3)\mapsto \mathrm{if}i=0\mathrm{then}1\mathrm{else}\mathrm{if}i=1\mathrm{then}2\mathrm{else}0)\mathrm{val}(s)$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IdealCompression.twoTripleModelsIso (✓ 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 isomorphism takes the image of each subset under the cycle sending 0 to 1, 1 to 2, and 2 to 0.

Definition 1.20 (SmallIdealCodes / pi0CodeOrderIso).

$$\forall (x:\mathrm{WithTop}(IntervalForestBasic.IntervalForest0)),\mathrm{val}((SmallIdealCodes.pi0CodeOrderIsox))=Option.elim(x:\mathrm{Option}(IntervalForestBasic.IntervalForest0))(\{0\}:\mathrm{Finset}(\mathrm{Fin}1))(\mathrm{fun}(\cdot :IntervalForestBasic.IntervalForest0)\mapsto (\{\}:\mathrm{Finset}(\mathrm{Fin}1)))$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IdealCompression.pi0CodeOrderIso (✓ 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 displayed finite map is an order isomorphism from WithTop (IntervalForest 0) to the closed-subset carrier of t1.

Definition 1.21 (SmallIdealCodes / pi1CodeOrderIso).

$$\forall (x:\mathrm{WithTop}(IntervalForestBasic.IntervalForest1)),\mathrm{val}((SmallIdealCodes.pi1CodeOrderIsox))=Option.elim(x:\mathrm{Option}(IntervalForestBasic.IntervalForest1))(\{0,1\}:\mathrm{Finset}(\mathrm{Fin}2))(\mathrm{fun}(P:IntervalForestBasic.IntervalForest1)\mapsto \mathrm{if}P.parent1=\mathrm{none}\mathrm{then}(\{\}:\mathrm{Finset}(\mathrm{Fin}2))\mathrm{else}\{0\})$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IdealCompression.pi1CodeOrderIso (✓ 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 displayed finite map is an order isomorphism from WithTop (IntervalForest 1) to the closed-subset carrier of t20.

Definition 1.22 (SmallIdealCodes / pi2CodeOrderIso).

$$\forall (x:\mathrm{WithTop}(IntervalForestBasic.IntervalForest2)),\mathrm{val}((SmallIdealCodes.pi2CodeOrderIsox))=Option.elim(x:\mathrm{Option}(IntervalForestBasic.IntervalForest2))(\{0,1,2\}:\mathrm{Finset}(\mathrm{Fin}3))(\mathrm{fun}(P:IntervalForestBasic.IntervalForest2)\mapsto \mathrm{if}P.parent1=\mathrm{none}\mathrm{then}(\mathrm{if}P.parent2=\mathrm{none}\mathrm{then}(\{\}:\mathrm{Finset}(\mathrm{Fin}3))\mathrm{else}\{2\})\mathrm{else}(\mathrm{if}P.parent2=\mathrm{none}\mathrm{then}\{0\}\mathrm{else}\mathrm{if}P.parent2=\mathrm{some}0\mathrm{then}\{0,1\}\mathrm{else}\{0,2\}))$$

Formalization. D5/S3/Combinatorics/PriorityLattice/IdealCompression.pi2CodeOrderIso (✓ 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 displayed finite map is an order isomorphism from WithTop (IntervalForest 2) to the closed-subset carrier of t3 0 2.

Theorem 1.23 (IntervalForest / compressCode_self_iff).

$$\forall (nk:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn)(h:ForestCovers.IntervalForest.edgeCountP=k)(i:\mathrm{Fin}k),\mathrm{val}((IdealCompression.IntervalForest.compressCodePhi))=\mathrm{val}(i)⟺\mathrm{val}((IdealCompression.IntervalForest.supportParentP(Finset.orderIsoOfFin(ForestCovers.IntervalForest.supportP)hi)))+1=\mathrm{val}(\mathrm{val}((Finset.orderIsoOfFin(ForestCovers.IntervalForest.supportP)hi)))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IdealCompression.compressCode_self_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.24 (IntervalForest / support_adjacent_of_needed).

$$\forall (nk:\mathrm{Nat})(P:IntervalForestBasic.IntervalForestn)(h:ForestCovers.IntervalForest.edgeCountP=k)(ij:\mathrm{Fin}k),\mathrm{val}(i)+1=\mathrm{val}(j)\to \mathrm{val}((IdealCompression.IntervalForest.compressCodePhj))\le \mathrm{val}(i)\to \mathrm{val}(\mathrm{val}((Finset.orderIsoOfFin(ForestCovers.IntervalForest.supportP)hi)))+1=\mathrm{val}(\mathrm{val}((Finset.orderIsoOfFin(ForestCovers.IntervalForest.supportP)hj)))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/IdealCompression.support_adjacent_of_needed (✓ 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/IdealCompression.CodeClosed
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.card_three_iff
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.card_two_iff
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.code_one
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.code_three
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.code_two
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.compressCode
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.compressCode_self_iff
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.firstIndex
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.firstNeeded
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.idealCodeOrderIso
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.pi0CodeOrderIso
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.pi1CodeOrderIso
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.pi2CodeOrderIso
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.pi_one_card
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.pi_two_card
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.supportParent
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.supportParent_spec
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.support_adjacent_of_needed
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.t1
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.t20
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.t21
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.t3
• Truth anchor: D5/S3/Combinatorics/PriorityLattice/IdealCompression.twoTripleModelsIso
• Dependency: D5/S3/Combinatorics/PriorityLattice/ForestCovers