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.
layer 0 · 27 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD0002 · beta_horner_derivative_value_existsEvery arbitrary beta-coded natural polynomial has an actual simultaneous value and exact formal derivative.
layer 1 · 44 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD0003 · beta_horner_derivative_value_projectionThe first component of simultaneous formal differentiation is exactly the preexisting polynomial Horner value.
layer 0 · 15 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD0004 · beta_horner_derivative_only_projectionA simultaneously evaluated polynomial pair yields an actual formal-derivative witness.
layer 0 · 9 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD0005 · beta_horner_derivative_only_existsThe exact formal derivative of every arbitrary beta-coded natural polynomial exists.
layer 2 · 13 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD0006 · beta_horner_derivative_first_component_functionalThe value component of every simultaneous polynomial/derivative evaluation is unique.
layer 1 · 33 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD0007 · beta_horner_derivative_emptyThe empty beta-coded polynomial and its exact formal derivative both evaluate to zero.
layer 0 · 28 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.
layer 0 · 106 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD0009 · beta_horner_derivative_functionalBoth the value and exact formal derivative of every beta-coded polynomial are simultaneously unique.
layer 1 · 112 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD000A · beta_horner_derivative_second_component_functionalThe formal derivative component is independent of every possible choice of coupled beta trace.
layer 2 · 24 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD000B · beta_horner_derivative_exists_uniqueEvery arbitrary beta-coded natural polynomial has exactly one simultaneously evaluated value/formal-derivative pair.
layer 2 · 28 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD000C · beta_horner_derivative_only_functionalThe exact formal derivative, considered without its accompanying polynomial value, is functional.
layer 3 · 21 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD000D · beta_horner_derivative_only_exists_uniqueEvery beta-coded natural polynomial has one and only one exact formal derivative at every evaluation point.
layer 4 · 23 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD000E · beta_horner_derivative_constantA one-coefficient polynomial evaluates to its actual decoded constant and has formal derivative zero.
layer 1 · 49 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableHD000F · beta_horner_derivative_linearA genuine two-coefficient polynomial a*t+k has the exact decoded formal derivative a.
layer 2 · 51 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 15 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.
Separate complete second-wave branches: Full G095 proof · Alpha v27.