Mathematics · proofs · software

Paper IX · Lean source

FiniteFiberCountsAudit.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

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

polynomial_counts/development/linear/FiniteFiberCountsAudit.lean23 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/polynomial_counts/development/linear/FiniteFiberCountsAudit.lean

Skip source text

1 module
2 public import FiniteFiberCounts
3 
4 #print axioms Komorebi.FiniteFiberCounts.Fiber
5 #print axioms Komorebi.FiniteFiberCounts.translate
6 #print axioms Komorebi.FiniteFiberCounts.difference
7 #print axioms Komorebi.FiniteFiberCounts.translate_zero
8 #print axioms Komorebi.FiniteFiberCounts.translate_add
9 #print axioms Komorebi.FiniteFiberCounts.translate_difference
10 #print axioms Komorebi.FiniteFiberCounts.difference_translate
11 #print axioms Komorebi.FiniteFiberCounts.fiberAddTorsor
12 #print axioms Komorebi.FiniteFiberCounts.fiberEquivKernel
13 #print axioms Komorebi.FiniteFiberCounts.translate_exists_unique
14 #print axioms Komorebi.FiniteFiberCounts.fiber_nonempty_iff_class_zero
15 #print axioms Komorebi.FiniteFiberCounts.fiber_card_eq_kernel
16 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_empty
17 #print axioms Komorebi.FiniteFiberCounts.rank
18 #print axioms Komorebi.FiniteFiberCounts.kernel_finrank
19 #print axioms Komorebi.FiniteFiberCounts.kernel_card
20 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_nonempty
21 #print axioms Komorebi.FiniteFiberCounts.fiber_card
22 #print axioms Komorebi.FiniteFiberCounts.cokernel_finrank
23 #print axioms Komorebi.FiniteFiberCounts.cokernel_card

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: d3e592bbadf059f9f5a40ddbf0ecd06981dffcabf9b1812076ab2f33f9c3f97a

Original source on GitHub

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation