PX0016

prime_field_polynomial_left_pad_bounded

Actual leading-zero padding preserves canonical prime-field bounds at its exact enlarged length.

Alpha v34 checked-use · first admitted v33 · 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.

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ L. ∀ t. ∀ d. ∀ e. Prime(p) → BetaPrefixInto(b,c,L,p) → PolynomialLeftPad(b,c,L,t,d,e) → BetaPrefixInto(d,e,t + L,p)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BetaPrefixInto(b,c,l,B) · 2PolynomialLeftPad(b,c,L,t,d,e) · 1Lt(a,b) · 3Prime(p) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

prime_field_polynomial_left_pad_index_casesprime_field_zero_below_prime · checked external prerequisite
Original expanded first-order statement 
forall p b c L t d e. (~((p) = 1) /\ forall pfa_factor_left_left_pad_bounded_prime pfa_factor_right_left_pad_bounded_prime. (p) = pfa_factor_left_left_pad_bounded_prime * pfa_factor_right_left_pad_bounded_prime -> pfa_factor_left_left_pad_bounded_prime = 1 \/ pfa_factor_right_left_pad_bounded_prime = 1) -> (forall fom_index_pfp_left_pad_bounded_source. (exists fom_gap_pfp_left_pad_bounded_source_index_bound. fom_gap_pfp_left_pad_bounded_source_index_bound + S (fom_index_pfp_left_pad_bounded_source) = L) -> exists fom_value_pfp_left_pad_bounded_source. ((((exists fom_beta_height_pfp_left_pad_bounded_source_entry. fom_beta_height_pfp_left_pad_bounded_source_entry + S (fom_value_pfp_left_pad_bounded_source) = S ((S (fom_index_pfp_left_pad_bounded_source)) * c)) /\ exists fom_beta_quotient_pfp_left_pad_bounded_source_entry. b = fom_beta_quotient_pfp_left_pad_bounded_source_entry * S ((S (fom_index_pfp_left_pad_bounded_source)) * c) + (fom_value_pfp_left_pad_bounded_source))) /\ (exists fom_gap_pfp_left_pad_bounded_source_value_bound. fom_gap_pfp_left_pad_bounded_source_value_bound + S (fom_value_pfp_left_pad_bounded_source) = p))) -> (((forall pfp_repeat_index_left_pad_bounded_graphzeros. (exists pfa_gap_left_pad_bounded_graphzerosindex. pfa_gap_left_pad_bounded_graphzerosindex + S (pfp_repeat_index_left_pad_bounded_graphzeros) = (t)) -> (((exists ff_h_pfp_left_pad_bounded_graphzerosentry. ff_h_pfp_left_pad_bounded_graphzerosentry + S (0) = S ((S (pfp_repeat_index_left_pad_bounded_graphzeros)) * e)) /\ exists ff_q_pfp_left_pad_bounded_graphzerosentry. d = ff_q_pfp_left_pad_bounded_graphzerosentry * S ((S (pfp_repeat_index_left_pad_bounded_graphzeros)) * e) + (0)))) /\ ((forall pfrep_index_left_pad_bounded_graph pfrep_value_left_pad_bounded_graph. (exists pfa_gap_left_pad_bounded_graphbound. pfa_gap_left_pad_bounded_graphbound + S (pfrep_index_left_pad_bounded_graph) = (L)) -> (((exists ff_h_pfp_left_pad_bounded_graphinput. ff_h_pfp_left_pad_bounded_graphinput + S (pfrep_value_left_pad_bounded_graph) = S ((S (pfrep_index_left_pad_bounded_graph)) * c)) /\ exists ff_q_pfp_left_pad_bounded_graphinput. b = ff_q_pfp_left_pad_bounded_graphinput * S ((S (pfrep_index_left_pad_bounded_graph)) * c) + (pfrep_value_left_pad_bounded_graph))) -> (((exists ff_h_pfp_left_pad_bounded_graphoutput. ff_h_pfp_left_pad_bounded_graphoutput + S (pfrep_value_left_pad_bounded_graph) = S ((S ((t)+pfrep_index_left_pad_bounded_graph)) * e)) /\ exists ff_q_pfp_left_pad_bounded_graphoutput. d = ff_q_pfp_left_pad_bounded_graphoutput * S ((S ((t)+pfrep_index_left_pad_bounded_graph)) * e) + (pfrep_value_left_pad_bounded_graph))))))) -> (forall fom_index_pfp_left_pad_bounded_target. (exists fom_gap_pfp_left_pad_bounded_target_index_bound. fom_gap_pfp_left_pad_bounded_target_index_bound + S (fom_index_pfp_left_pad_bounded_target) = t+L) -> exists fom_value_pfp_left_pad_bounded_target. ((((exists fom_beta_height_pfp_left_pad_bounded_target_entry. fom_beta_height_pfp_left_pad_bounded_target_entry + S (fom_value_pfp_left_pad_bounded_target) = S ((S (fom_index_pfp_left_pad_bounded_target)) * e)) /\ exists fom_beta_quotient_pfp_left_pad_bounded_target_entry. d = fom_beta_quotient_pfp_left_pad_bounded_target_entry * S ((S (fom_index_pfp_left_pad_bounded_target)) * e) + (fom_value_pfp_left_pad_bounded_target))) /\ (exists fom_gap_pfp_left_pad_bounded_target_value_bound. fom_gap_pfp_left_pad_bounded_target_value_bound + S (fom_value_pfp_left_pad_bounded_target) = p)))

Complete tactic proof in conservative notation

All 46 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

46 script commands · 15 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
prime field polynomial left pad index cases
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro L
  5. L5
    intro t
  6. L6
    intro d
  7. L7
    intro e
  8. L8
    intro hp
  9. L9
    intro hc
  10. L10
    intro h
02Fix variables and assumptionsL11–12

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro i
  2. L12
    intro hi
03Separate the logical casesL13–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L13
    cases h
04Establish hoL14–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial left pad index cases.

  1. L14
    have ho : Lt(i,t) ∨ (∃ x. Lt(x,L) ∧ i = t + x)Definitions: Lt(i,t)Lt(x,L)Original native command in the exact edition
  2. L15
    specialize prime_field_polynomial_left_pad_index_cases (t)
  3. L16
    specialize prime_field_polynomial_left_pad_index_cases (L)
  4. L17
    specialize prime_field_polynomial_left_pad_index_cases (i)
  5. L18
    apply prime_field_polynomial_left_pad_index_cases
  6. L19
    exact hi
05Separate the logical casesL20–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    cases ho
06Construct an explicit witnessL21–21

Supply the displayed value, then prove that it has the required property.

  1. L21
    exists 0
07Separate the logical casesL22–22

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L22
    split
08Use earlier factsL23–28

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L23
    specialize h_left (i)
  2. L24
    apply h_left
  3. L25
    exact ho_left
  4. L26
    specialize prime_field_zero_below_prime (p)
  5. L27
    apply prime_field_zero_below_prime
  6. L28
    exact hp
09Separate the logical casesL29–30

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    cases ho_right
  2. L30
    cases ho_right_witness
10Establish hvL31–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hc.

  1. L31
    have hv : ∃ a. BetaAt(b,c,x,a) ∧ Lt(a,p)Definitions: BetaAt(b,c,x,a)Lt(a,p)Original native command in the exact edition
  2. L32
    specialize hc (x)
  3. L33
    apply hc
  4. L34
    exact ho_right_witness_left
11Separate the logical casesL35–36

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L35
    cases hv
  2. L36
    cases hv_witness
12Construct an explicit witnessL37–37

Supply the displayed value, then prove that it has the required property.

  1. L37
    exists x1
13Separate the logical casesL38–38

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L38
    split
14Calculate and transport equalitiesL39–40

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L39
    rewrite ho_right_witness_right
  2. L40
    rewrite ho_right_witness_right
15Use earlier factsL41–46

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L41
    specialize h_right (x)
  2. L42
    specialize h_right (x1)
  3. L43
    apply h_right
  4. L44
    exact ho_right_witness_left
  5. L45
    exact hv_witness_left
  6. L46
    exact hv_witness_right

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro L
  5. 0005intro t
  6. 0006intro d
  7. 0007intro e
  8. 0008intro hp
  9. 0009intro hc
  10. 0010intro h
  11. 0011intro i
  12. 0012intro hi
  13. 0013cases h
  14. 0014have ho : Lt(i,t) ∨ (∃ x. Lt(x,L) ∧ i = t + x)
  15. 0015specialize prime_field_polynomial_left_pad_index_cases (t)
  16. 0016specialize prime_field_polynomial_left_pad_index_cases (L)
  17. 0017specialize prime_field_polynomial_left_pad_index_cases (i)
  18. 0018apply prime_field_polynomial_left_pad_index_cases
  19. 0019exact hi
  20. 0020cases ho
  21. 0021exists 0
  22. 0022split
  23. 0023specialize h_left (i)
  24. 0024apply h_left
  25. 0025exact ho_left
  26. 0026specialize prime_field_zero_below_prime (p)
  27. 0027apply prime_field_zero_below_prime
  28. 0028exact hp
  29. 0029cases ho_right
  30. 0030cases ho_right_witness
  31. 0031have hv : ∃ a. BetaAt(b,c,x,a) ∧ Lt(a,p)
  32. 0032specialize hc (x)
  33. 0033apply hc
  34. 0034exact ho_right_witness_left
  35. 0035cases hv
  36. 0036cases hv_witness
  37. 0037exists x1
  38. 0038split
  39. 0039rewrite ho_right_witness_right
  40. 0040rewrite ho_right_witness_right
  41. 0041specialize h_right (x)
  42. 0042specialize h_right (x1)
  43. 0043apply h_right
  44. 0044exact ho_right_witness_left
  45. 0045exact hv_witness_left
  46. 0046exact hv_witness_right