Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

PrincipalIdeals

Abstract

Priority-forest interval structure and counting.

Theorem 1.1 (forest_ideal_shape_iff).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/PrincipalIdeals.forest_ideal_shape_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.2 (gamma_formula).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/PrincipalIdeals.gamma_formula (✓ 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 (gammaPos_formula).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PriorityLattice/PrincipalIdeals.gammaPos_formula (✓ 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 (gamma).

Formalization. D5/S3/Combinatorics/PriorityLattice/PrincipalIdeals.gamma (✓ 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 : Pi n // ∃ m ≤ n, Nonempty (Set.Iic x ≃o Pi m)}.

Definition 1.5 (gammaPos).

Formalization. D5/S3/Combinatorics/PriorityLattice/PrincipalIdeals.gammaPos (✓ 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 : Pi n // ∃ m, 1 <= m ∧ m <= n ∧ Nonempty (Set.Iic x ≃o Pi m)}.

Definition 1.6 (claimGamma).

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

Section 6, item 3, p. 24: How many principal ideals of Π(n) are isomorphic to Π(m), for some 1≤ m≤ n? Let γₙ denote the number of principal ideals of Π(n) that are isomorphic to Π(m) with m ≤ n. The sequence (γₙ)ₙ≥₁ begins as 2, 4, 8, 14, 22 ,32, 44, … This sequence seems to be https://oeis.org/A014206, which is given by the formula γₙ = n² + n + 2. The data give n² − n + 2, with m = 0 allowed. The positive-parameter reading gives n² + 2 − 2n. Both counts include the greatest element’s ideal; natural subtraction is taken in the displayed order. These are the counting conventions of Lillo and Rosas; the count formulas resolve their final-section questions.

Theorem 1.7 (result).

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

Resolves. Problems/lillo-rosas-2026-priority-lattice-principal-ideals (proved) by D5/S3/Combinatorics/PriorityLattice/PrincipalIdeals.result.

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