PX0016

prime_field_polynomial_left_pad_bounded

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 expanded first-order arithmetic 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)))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 46 exact native proof lines.

Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

PX000A prime_field_polynomial_left_pad_index_cases prime_field_zero_below_prime Alpha theorem; checked-use authorized

Direct dependents

PX0071 prime_field_polynomial_convolution_both_left_paddings_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 : (exists pfa_gap_left_pad_bound_zero. pfa_gap_left_pad_bound_zero + S (i) = (t)) \/ exists j. (((exists pfa_gap_left_pad_bound_source. pfa_gap_left_pad_bound_source + S (j) = (L)) /\ ((i=t+j))))
  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 : exists a. (((((exists ff_h_pfp_left_pad_bound_entry. ff_h_pfp_left_pad_bound_entry + S (a) = S ((S (x)) * c)) /\ exists ff_q_pfp_left_pad_bound_entry. b = ff_q_pfp_left_pad_bound_entry * S ((S (x)) * c) + (a))) /\ ((exists pfa_gap_left_pad_bound_value. pfa_gap_left_pad_bound_value + S (a) = (p)))))
  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 exact 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 : (exists pfa_gap_left_pad_bound_zero. pfa_gap_left_pad_bound_zero + S (i) = (t)) \/ exists j. (((exists pfa_gap_left_pad_bound_source. pfa_gap_left_pad_bound_source + S (j) = (L)) /\ ((i=t+j))))
  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 : exists a. (((((exists ff_h_pfp_left_pad_bound_entry. ff_h_pfp_left_pad_bound_entry + S (a) = S ((S (x)) * c)) /\ exists ff_q_pfp_left_pad_bound_entry. b = ff_q_pfp_left_pad_bound_entry * S ((S (x)) * c) + (a))) /\ ((exists pfa_gap_left_pad_bound_value. pfa_gap_left_pad_bound_value + S (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