Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

PairedIdealIntersectionDeterminants

Abstract

Actual ideal-intersection graphs and uniform higher-prime Laplacian obstructions.

The public mathematical input is unit-exponent.tex at immutable revision b93becea662a746badeadba42fdc3d3eb3db9382. General endpoint arguments follow the completed mathematical note supplied 2026-11-02. The formal proofs and this exposition are independently authored; no priority claim follows.

Theorem 1.1 (Full symbolic determinant).

Lean statement: D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_tensorK_sub_scalar

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_tensorK_sub_scalar (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. the-omega-institute/ideal-intersection-laplacian contributors (2026). Six-support complement quotient, global endpoint spectrum, fixed-gap expansion and integer finiteness. URL: https://github.com/the-omega-institute/ideal-intersection-laplacian/blob/b93becea662a746badeadba42fdc3d3eb3db9382/paper/core/body.tex.

Commentary.

The scalar-shift determinant is expanded symbolically over an arbitrary commutative ring. This is a binding normalization identity, with no fixed positive certificate.

Theorem 1.2 (Exact H4 endpoint reduction).

Lean statement: D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_two_sub_two

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_two_sub_two (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. the-omega-institute/ideal-intersection-laplacian contributors (2026). Six-support complement quotient, global endpoint spectrum, fixed-gap expansion and integer finiteness. URL: https://github.com/the-omega-institute/ideal-intersection-laplacian/blob/b93becea662a746badeadba42fdc3d3eb3db9382/paper/core/body.tex.

Commentary.

At a=2 and shift two, the determinant is exactly P2(b,c).

Theorem 1.3 (Exact H5 endpoint reduction).

Lean statement: D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_three_sub_two

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_three_sub_two (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. the-omega-institute/ideal-intersection-laplacian contributors (2026). Six-support complement quotient, global endpoint spectrum, fixed-gap expansion and integer finiteness. URL: https://github.com/the-omega-institute/ideal-intersection-laplacian/blob/b93becea662a746badeadba42fdc3d3eb3db9382/paper/core/body.tex.

Commentary.

At a=3 and shift two, the determinant is exactly P3(b,c).

Theorem 1.4 (H5 upper endpoint).

Lean statement: D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_three_sub_three

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_three_sub_three (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. the-omega-institute/ideal-intersection-laplacian contributors (2026). Six-support complement quotient, global endpoint spectrum, fixed-gap expansion and integer finiteness. URL: https://github.com/the-omega-institute/ideal-intersection-laplacian/blob/b93becea662a746badeadba42fdc3d3eb3db9382/paper/core/body.tex.

Commentary.

With p=bc and s=b+c, det(K3-3I)=-35p squared+8ps-20s squared+149p+11s+4.

Theorem 1.5 (Shifted H4 determinant).

Lean statement: D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_two_add_one

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_two_add_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. the-omega-institute/ideal-intersection-laplacian contributors (2026). Six-support complement quotient, global endpoint spectrum, fixed-gap expansion and integer finiteness. URL: https://github.com/the-omega-institute/ideal-intersection-laplacian/blob/b93becea662a746badeadba42fdc3d3eb3db9382/paper/core/body.tex.

Commentary.

With p=bc and s=b+c, det(K2+I)=4(10p squared+39ps+102p+24s squared+104s+96).

Theorem 1.6 (Strict upper-endpoint sign for every tail).

Lean statement: D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_three_sub_three_neg

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_three_sub_three_neg (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. the-omega-institute/ideal-intersection-laplacian contributors (2026). Six-support complement quotient, global endpoint spectrum, fixed-gap expansion and integer finiteness. URL: https://github.com/the-omega-institute/ideal-intersection-laplacian/blob/b93becea662a746badeadba42fdc3d3eb3db9382/paper/core/body.tex.

Commentary.

For b,c at least two, p at least four, s at least four and s at most p. Thus the determinant is at most -27p squared+149p-272=-(27(p-4) squared+67(p-4)+108), strictly negative.

Theorem 1.7 (H5 paired eigenvalue in (1,3)).

Lean statement: D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.three_symmetric_low_eigenpair

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.three_symmetric_low_eigenpair (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. the-omega-institute/ideal-intersection-laplacian contributors (2026). Six-support complement quotient, global endpoint spectrum, fixed-gap expansion and integer finiteness. URL: https://github.com/the-omega-institute/ideal-intersection-laplacian/blob/b93becea662a746badeadba42fdc3d3eb3db9382/paper/core/body.tex.

Commentary.

A negative determinant prevents S3-3I from being positive semidefinite, so its Hermitian spectral expansion has a negative eigenvalue. Combining with the shared strict lower bound gives a paired eigenvalue in (1,3) throughout b,c at least two.

References