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
- Truth anchor:
D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_tensorK_sub_scalar - Truth anchor:
D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_three_sub_three - Truth anchor:
D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_three_sub_three_neg - Truth anchor:
D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_three_sub_two - Truth anchor:
D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_two_add_one - Truth anchor:
D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.det_two_sub_two - Truth anchor:
D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionDeterminants.three_symmetric_low_eigenpair - Dependency: D5/S3/Combinatorics/SpectralGraph/PairedIdealIntersectionObstructions