Paper IX · Lean source
InvalidJointMissingParameterTerm.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/InvalidJointMissingParameterTerm.lean10 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/polynomial_regularity/controls/InvalidJointMissingParameterTerm.lean1 module
2 public import PolynomialJointMotionControls
3 @[expose] public section
4 open Komorebi.PolynomialJointMotionControls
5
6 -- Invalid: F(Y,T)=Y+T, H=1, p=2, s=0, M=2, a=0, v=1.
7 -- The prescribed parameter is 4 and the exact solved root is -8.
8 -- Omitting K v predicts -4 and leaves an error not divisible by 2^4.
9 example : (2 : ℤ_[2]) ^ 4 ∣ (-8 : ℤ_[2]) - (-(2 : ℤ_[2]) ^ 2 * 1) := by
10 exact omitted_parameter_term_fails
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: a76fb6d3d3b668569ce3e7116426a45104f622f5510cdbfadafb554218c2ca51
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation