Paper VIII · Lean sources

Packet Operator Algorithms, Exact Compilation, and GPU Realization

Inherited / related evidence Coverage and evidence

The edition relies on earlier or related formal evidence. That evidence is not a fresh full-edition replay.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

Source files 40

Source locations and editions

Files are shown relative to source/complete/Paper_VIII_Complete_v0.6.0_With_Visual_Appendix/original_snapshot/formalization/.

Historical editions keep their original paths. Package caches and build files are omitted.

40 files

BandedCount.lean
115 lines · 13 declaration locations
BlockJacobi.lean
160 lines · 15 declaration locations
BoundaryChecks.lean
77 lines · 7 declaration locations
BudgetConvolution.lean
225 lines · 18 declaration locations
CirculantFourier.lean
180 lines · 15 declaration locations
ClippedPrecision.lean
290 lines · 21 declaration locations
CompactRangeFactors.lean
101 lines · 12 declaration locations
CompactTruncation.lean
68 lines · 7 declaration locations
ContinuousPrecision.lean
163 lines · 12 declaration locations
DiagonalTruncation.lean
127 lines · 15 declaration locations
DiscoveryCertificate.lean
168 lines · 10 declaration locations
DiscretePrecision.lean
157 lines · 13 declaration locations
ExactTreeCompiler.lean
199 lines · 18 declaration locations
FrobeniusOptimality.lean
123 lines · 5 declaration locations
GraphSchedules.lean
210 lines · 23 declaration locations
InverseSupport.lean
134 lines · 11 declaration locations
KernelFrame.lean
109 lines · 13 declaration locations
KrylovPackets.lean
209 lines · 12 declaration locations
LowRankAlgebra.lean
151 lines · 11 declaration locations
LowRankChains.lean
100 lines · 8 declaration locations
PacketCostModels.lean
198 lines · 29 declaration locations
PacketIR.lean
165 lines · 14 declaration locations
PacketPerturbation.lean
75 lines · 6 declaration locations
ProductChainError.lean
202 lines · 16 declaration locations
QuantizedTreeCompiler.lean
145 lines · 8 declaration locations
QuantumPacketCore.lean
242 lines · 24 declaration locations
RecompressionEndpoints.lean
86 lines · 8 declaration locations
SchedulingContracts.lean
183 lines · 22 declaration locations
SchurSupport.lean
92 lines · 4 declaration locations
SmallCoreNorms.lean
215 lines · 23 declaration locations
SmallCoreRecompression.lean
154 lines · 9 declaration locations
SmallCoreTransfer.lean
94 lines · 9 declaration locations
SpectralOptimality.lean
137 lines · 8 declaration locations
StoredBudgetCompiler.lean
281 lines · 29 declaration locations
StructuredTensor.lean
145 lines · 15 declaration locations
ToeplitzEmbedding.lean
80 lines · 9 declaration locations
TransferSupport.lean
162 lines · 12 declaration locations
TreeCompilerUpdates.lean
173 lines · 15 declaration locations
TriangularSolve.lean
133 lines · 10 declaration locations
WalshTransform.lean
133 lines · 12 declaration locations