Paper IX · Lean source

InvalidSingularUniqueLift.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/controls/InvalidSingularUniqueLift.lean8 lines

Original source path

preserved/PRSC_IX_Consolidated_Manuscript/polynomial_counts/controls/InvalidSingularUniqueLift.lean

1 module
2 public import PolynomialCountControls
3 @[expose] public section
4 open Komorebi.PolynomialCountControls Komorebi.PolynomialLiftCounts
5 
6 -- Invalid: a liftable singular root need not have a unique next-level lift.
7 example : Nat.card (ActualLifts 2 1 squareSystem (fun _ => 0)) = 1 := by
8   exact singular_square_lift_count

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: 2f0d5b8b8d7024842dc6e2bc9a291ef4e7be819d45f47b3ae220f5f5de547277

Original source on GitHub

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