Apoth3osis
MODULES
14
Full PSL formalization stack
DECLARATIONS
184
Theorems, lemmas, and definitions
LINES
3,947
Lean 4 source across 14 modules
SORRY
0
No incomplete proof terms
AUDITS
57
Hostile audits passed across PSL formalization
AUTHORS
2
Wei & Wei (MSU / NCSU)
>_PAPER.PROOF.CODE

Persistent Sheaf Laplacian
Orientation-Independence

Machine-checked proof that the persistent sheaf Laplacian's kernel dimension, characteristic polynomial, and full eigenvalue spectrum are invariant under arbitrary simplex orientation changes. First formal verification of spectral-level orientation-independence for this central TDA operator.

Lean 4 v4.24.0Mathlib v4.24.014 modules3,947 lines184 declarations0 sorry
>_HERITAGE.RESEARCHERS
Guo-Wei Wei, MSU Foundation Professor of Mathematics

Guo-Wei Wei

MSU Research Foundation Distinguished Professor of Mathematics & Biochemistry, Michigan State University

Pioneer of persistent Laplacians and their applications to molecular bioscience. Developed the persistent sheaf Laplacian framework for fusing geometric and physical data in topological data analysis.

Xiaoqi Wei, Postdoctoral Research Scholar at NC State University

Xiaoqi Wei

Postdoctoral Research Scholar, Department of Mathematics, North Carolina State University

Co-developer of the persistent sheaf Laplacian theory. Research focuses on topological methods in biology and multi-scale data analysis using sheaf-theoretic tools.

>_PAPER.PROOF.MAP
PAPER SECTIONLEAN MODULESTATUS
Simplicial complexes and q-simplicesBasic.SimplicialComplexPROVED
Orientation infrastructure and permutation signsBasic.OrientationPROVED
Cellular sheaves on simplicial complexesBasic.CellularSheafPROVED
Sheaf cochain complex and coboundary mapsCochain.CochainComplex + CochainMatrixPROVED
Hodge-type sheaf Laplacian definitionLaplacian.SheafLaplacianPROVED
Spectral theory and canonical definitionsLaplacian.SpectrumPROVED
Orientation-independence (core result)Laplacian.OrientationIndependencePROVED
Persistent filtrationsPersistent.FiltrationPROVED
Persistent coboundary and LaplacianPersistent.PersistentCoboundary + PersistentSheafLaplacianPROVED
Persistent Betti numbersPersistent.BettiNumbersPROVED
Constant sheaf reduction to graph LaplacianApplications.ConstantSheafReductionPROVED
Multi-sensor data fusion applicationApplications.DataFusionPROVED
>_KEY.MATHEMATICS
coboundaryMatrix_orientationSign_conj
Do1=Sq+1⋅Do2⋅SqD_{o_1} = S_{q+1} \cdot D_{o_2} \cdot S_q

The coboundary matrix under orientation o₁ is a diagonal ±1 conjugate of the coboundary under o₂.

sheafLaplacianMatrix_orientationSign_conj
Lo1=S⋅Lo2⋅SL_{o_1} = S \cdot L_{o_2} \cdot S

The sheaf Laplacian transforms by diagonal sign conjugation under orientation change.

sheafLaplacianKerEquiv
ker⁡Lo1≃Rker⁡Lo2\ker L_{o_1} \simeq_{\mathbb{R}} \ker L_{o_2}

The kernels of the Laplacian under different orientations are linearly isomorphic.

finrank_ker_sheafLaplacianMatrix_eq
dim⁡ker⁡Lo1=dim⁡ker⁡Lo2\dim \ker L_{o_1} = \dim \ker L_{o_2}

Harmonic sheaf nullity is independent of orientation choice.

sheafLaplacianMatrix_charpoly_eq
χLo1(t)=χLo2(t)\chi_{L_{o_1}}(t) = \chi_{L_{o_2}}(t)

The characteristic polynomial is invariant under orientation change.

sheafLaplacianMatrix_spectrum_eq
σ(Lo1)=σ(Lo2)\sigma(L_{o_1}) = \sigma(L_{o_2})

The full eigenvalue spectrum is orientation-independent.

sign_reorderPerm_eraseIdx_of_get_eq
sgn(πl1′→l2′)=sgn(πl1→l2)⋅(−1)j1⋅(−1)j2\text{sgn}(\pi_{l_1' \to l_2'}) = \text{sgn}(\pi_{l_1 \to l_2}) \cdot (-1)^{j_1} \cdot (-1)^{j_2}

Permutation sign decomposes predictably when a shared vertex is erased from two orderings.

signedIncidence_eq_orientationSimplexSign_mul_of_qface
εo1(σ,τ)=so1,o2(τ)⋅so1,o2(σ)⋅εo2(σ,τ)\varepsilon_{o_1}(\sigma,\tau) = s_{o_1,o_2}(\tau) \cdot s_{o_1,o_2}(\sigma) \cdot \varepsilon_{o_2}(\sigma,\tau)

Signed incidence numbers factor through orientation simplex signs.

orientationSignMatrix_mul_self
S⋅S=IS \cdot S = I

The orientation sign matrix is self-inverse (involutory).

finrank_ker_sheafLaplacianMatrix_eq_harmonicSheafNullity
dim⁡ker⁡Lo=βharmonic(F,q)\dim \ker L_o = \beta^{\text{harmonic}}(F, q)

The kernel dimension under any orientation equals the canonical harmonic sheaf nullity.

sheafLaplacianMatrix_spectrum_eq_sorted
σ(Lo)=σcanonical(F,q)\sigma(L_o) = \sigma^{\text{canonical}}(F, q)

The spectrum under any orientation equals the canonical sheaf Laplacian spectrum.

>_DEPENDENCY.GRAPH

Hover over nodes to trace the proof spine from foundational infrastructure through core Laplacian theory to persistent and application layers.

SimplicialComplexCellularSheafOrientationCochainComplexCochainMatrixSheafLaplacianSpectrumOrientIndepFiltrationPersistCoboundaryPersistLaplacianBettiNumbersConstantSheafDataFusion
Foundation Core Bridge / Application Persistent Layer
>_PROOF.BLUEPRINT
>_ARTIFACTS

Lean Proof Artifacts

lean-proofs.tar.gzComplete Lean proof surface (14 modules + lakefile).\u2193OrientationIndependence.leanCore result: diagonal sign conjugation → spectral invariance.\u2193Orientation.leanOrientation infrastructure: reorder permutations, signed incidence, sign decomposition.\u2193Spectrum.leanCanonical spectral definitions using sorted orientation.\u2193CochainComplex.leanSheaf cochain spaces and coboundary maps.\u2193
>_PROVENANCE.CHAIN
PAPER

Wei & Wei (2021). Persistent sheaf Laplacians. arXiv:2112.10906

LEAN 4

14 modules, 184 declarations. Orientation sign infrastructure + spectral invariance.

VERIFICATION

lake build passes, 0 sorry/admit, all 14 modules compile against Lean 4 v4.24.0 + Mathlib.

GITHUB

Standalone researcher package with lakefile, build instructions, and full theorem inventory.

>_VERIFICATION.SEAL
FORMALLY VERIFIED • LEAN 4 • MACHINE-CHECKED • APOTH3OSIS∀∃⊢→∧∨¬≡QED184 theorems • 0 sorry14 modules · 57 audits0 SORRY

Formal Verification Certificate

The persistent sheaf Laplacian orientation-independence formalization has been verified as a standalone Lean 4 package. The central conjugation claim and all downstream invariance theorems are kernel-checked with zero sorry placeholders.

184 THEOREMS VERIFIED14 MODULES3,947 LINES0 SORRY57 HOSTILE AUDITS

Persistent Sheaf Laplacian • Lean 4 + Mathlib • Apoth3osis Labs

ARXIV PAPERPPC INDEXGITHUB