Exact Horner derivatives · constructive traces · G095 partial
Independently checked constructive theorems build coupled beta-coded Horner value and formal-derivative traces for arbitrary natural polynomials, including exact successor laws and uniqueness.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not Stable
Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
HD0001 beta_horner_derivative_trace_existsEvery beta-coded polynomial has two actual coupled Horner traces, the second being its formal derivative trace.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD0002 beta_horner_derivative_value_existsEvery arbitrary beta-coded natural polynomial has an actual simultaneous value and exact formal derivative.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD0003 beta_horner_derivative_value_projectionThe first component of simultaneous formal differentiation is exactly the preexisting polynomial Horner value.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD0004 beta_horner_derivative_only_projectionA simultaneously evaluated polynomial pair yields an actual formal-derivative witness.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD0005 beta_horner_derivative_only_existsThe exact formal derivative of every arbitrary beta-coded natural polynomial exists.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD0006 beta_horner_derivative_first_component_functionalThe value component of every simultaneous polynomial/derivative evaluation is unique.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD0007 beta_horner_derivative_emptyThe empty beta-coded polynomial and its exact formal derivative both evaluate to zero.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD0008 beta_horner_derivative_successor_decomposeA successor polynomial obeys both exact Horner recurrences: f_new=f_old*t+a and f'_new=f'_old*t+f_old.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD0009 beta_horner_derivative_functionalBoth the value and exact formal derivative of every beta-coded polynomial are simultaneously unique.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD000A beta_horner_derivative_second_component_functionalThe formal derivative component is independent of every possible choice of coupled beta trace.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD000B beta_horner_derivative_exists_uniqueEvery arbitrary beta-coded natural polynomial has exactly one simultaneously evaluated value/formal-derivative pair.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD000C beta_horner_derivative_only_functionalThe exact formal derivative, considered without its accompanying polynomial value, is functional.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD000D beta_horner_derivative_only_exists_uniqueEvery beta-coded natural polynomial has one and only one exact formal derivative at every evaluation point.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD000E beta_horner_derivative_constantA one-coefficient polynomial evaluates to its actual decoded constant and has formal derivative zero.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableHD000F beta_horner_derivative_linearA genuine two-coefficient polynomial a*t+k has the exact decoded formal derivative a.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableND0001 Beta(b,c,i,x)Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0ND0002 Horner(b,c,x,ell,z)A complete beta-coded natural-polynomial Horner trace with an explicitly witnessed terminal value.
Conservative definition · notation layer 1ND0050 HornerDerivativeTrace(b,c,t,l,u,v,d,e)Parallel beta-coded Horner value and derivative traces satisfying the exact formal differentiation recurrence.
Conservative definition · notation layer 2ND0051 HornerDerivative(b,c,t,l,n,z)The exact jointly witnessed natural Horner polynomial value and its formal derivative.
Conservative definition · notation layer 3ND0052 HornerDerivativeOnly(b,c,t,l,z)The exact natural formal derivative obtained by existentially packaging its actual Horner value.
Conservative definition · notation layer 4PD0004 Prime(p)p is nonunit and every factorization of p has a unit factor.
Conservative definition · notation layer 0PD0008 ModEq(m,a,b)Balanced-natural congruence modulo m.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0014 Product(b,c,l,z)z is the product of a beta-coded prefix of length l.
Conservative definition · notation layer 1PD0019 Repeat(b,c,a,l)The decoded prefix repeats a for l positions.
Conservative definition · notation layer 1PD0020 Pow(a,e,z)z is the relational e-th power of a.
Conservative definition · notation layer 2Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.
Separate complete second-wave branches: Full G095 proof · Alpha v27.