Paper IX · Lean source

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

Original source path

preserved/PRSC_IX_Consolidated_Manuscript/polynomial_counts/controls/InvalidUnconditionalLiftCount.lean

1 module
2 public import PolynomialCountControls
3 @[expose] public section
4 open Komorebi.PolynomialCountControls Komorebi.PolynomialLiftCounts
5 
6 -- Invalid: rank-nullity's nonzero count cannot ignore the residual obstruction.
7 example : Nat.card (ActualLifts 2 1 squareMinusTwo (fun _ => 0)) = 2 := by
8   exact obstructed_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: b1de2ddde8561112c4b6cf99c3569d823f59ebb93dad48c8d15408772ee84589

Original source on GitHub

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