Paper IX · Lean source
InvalidRegularityDerivativeSign.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_regularity/controls/InvalidRegularityDerivativeSign.lean16 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/polynomial_regularity/controls/InvalidRegularityDerivativeSign.leanSkip declarations and read code
1 module
2 public import PolynomialRegularityControls
3
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7
8 namespace Komorebi.InvalidRegularityDerivativeSign
9
10 /-- Deliberately invalid: F(Y,T)=Y+T has derivative -I, not +I. -/
11 theorem wrong_parameter_derivative (p : ℕ) [Fact p.Prime] (t : Fin 1 → ℚ_[p]) :
12 HasStrictFDerivAt (fun u : Fin 1 → ℚ_[p] => -u)
13 (ContinuousLinearMap.id ℚ_[p] (Fin 1 → ℚ_[p])) t := by
14 exact PolynomialRegularityControls.linear_strict_derivative t
15
16 end Komorebi.InvalidRegularityDerivativeSign
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: 309e40ab0dfde1d9fd2664ecd13aa87a42478b3521b4d2646e48c76fe273bd71
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation