PG0035

prime_field_polynomial_bounded_representative_at_length_exists

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

From L<=K construct a genuine leading-zero beta prefix of length K, retain canonical coefficients, and prove formal equivalence to the input, including empty prefixes.

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 ab ac L K. (~((p) = 1) /\ forall pfa_factor_left_alignment_prime pfa_factor_right_alignment_prime. (p) = pfa_factor_left_alignment_prime * pfa_factor_right_alignment_prime -> pfa_factor_left_alignment_prime = 1 \/ pfa_factor_right_alignment_prime = 1) -> (forall fom_index_pfp_alignment_input. (exists fom_gap_pfp_alignment_input_index_bound. fom_gap_pfp_alignment_input_index_bound + S (fom_index_pfp_alignment_input) = L) -> exists fom_value_pfp_alignment_input. ((((exists fom_beta_height_pfp_alignment_input_entry. fom_beta_height_pfp_alignment_input_entry + S (fom_value_pfp_alignment_input) = S ((S (fom_index_pfp_alignment_input)) * ac)) /\ exists fom_beta_quotient_pfp_alignment_input_entry. ab = fom_beta_quotient_pfp_alignment_input_entry * S ((S (fom_index_pfp_alignment_input)) * ac) + (fom_value_pfp_alignment_input))) /\ (exists fom_gap_pfp_alignment_input_value_bound. fom_gap_pfp_alignment_input_value_bound + S (fom_value_pfp_alignment_input) = p))) -> (exists pfrep_gap_alignment_length_bound. pfrep_gap_alignment_length_bound+(L)=(K)) -> (exists ub uc. ((forall fom_index_pfp_alignment_output_bounded. (exists fom_gap_pfp_alignment_output_bounded_index_bound. fom_gap_pfp_alignment_output_bounded_index_bound + S (fom_index_pfp_alignment_output_bounded) = K) -> exists fom_value_pfp_alignment_output_bounded. ((((exists fom_beta_height_pfp_alignment_output_bounded_entry. fom_beta_height_pfp_alignment_output_bounded_entry + S (fom_value_pfp_alignment_output_bounded) = S ((S (fom_index_pfp_alignment_output_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_alignment_output_bounded_entry. ub = fom_beta_quotient_pfp_alignment_output_bounded_entry * S ((S (fom_index_pfp_alignment_output_bounded)) * uc) + (fom_value_pfp_alignment_output_bounded))) /\ (exists fom_gap_pfp_alignment_output_bounded_value_bound. fom_gap_pfp_alignment_output_bounded_value_bound + S (fom_value_pfp_alignment_output_bounded) = p))) /\ ((forall pfrep_power_alignment_output_equivalent pfrep_left_alignment_output_equivalent pfrep_right_alignment_output_equivalent. ((exists pfrep_position_alignment_output_equivalentfirst. ((pfrep_position_alignment_output_equivalentfirst+S (pfrep_power_alignment_output_equivalent)=(L)) /\ ((((exists ff_h_pfp_alignment_output_equivalentfirstentry. ff_h_pfp_alignment_output_equivalentfirstentry + S (pfrep_left_alignment_output_equivalent) = S ((S (pfrep_position_alignment_output_equivalentfirst)) * ac)) /\ exists ff_q_pfp_alignment_output_equivalentfirstentry. ab = ff_q_pfp_alignment_output_equivalentfirstentry * S ((S (pfrep_position_alignment_output_equivalentfirst)) * ac) + (pfrep_left_alignment_output_equivalent)))))) \/ (((exists pfrep_gap_alignment_output_equivalentfirstoutside. pfrep_gap_alignment_output_equivalentfirstoutside+(L)=(pfrep_power_alignment_output_equivalent)) /\ (((pfrep_left_alignment_output_equivalent)=0))))) -> ((exists pfrep_position_alignment_output_equivalentsecond. ((pfrep_position_alignment_output_equivalentsecond+S (pfrep_power_alignment_output_equivalent)=(K)) /\ ((((exists ff_h_pfp_alignment_output_equivalentsecondentry. ff_h_pfp_alignment_output_equivalentsecondentry + S (pfrep_right_alignment_output_equivalent) = S ((S (pfrep_position_alignment_output_equivalentsecond)) * uc)) /\ exists ff_q_pfp_alignment_output_equivalentsecondentry. ub = ff_q_pfp_alignment_output_equivalentsecondentry * S ((S (pfrep_position_alignment_output_equivalentsecond)) * uc) + (pfrep_right_alignment_output_equivalent)))))) \/ (((exists pfrep_gap_alignment_output_equivalentsecondoutside. pfrep_gap_alignment_output_equivalentsecondoutside+(K)=(pfrep_power_alignment_output_equivalent)) /\ (((pfrep_right_alignment_output_equivalent)=0))))) -> pfrep_left_alignment_output_equivalent=pfrep_right_alignment_output_equivalent))))

Constructive proof overview

Generated structural guide

From L<=K construct a genuine leading-zero beta prefix of length K, retain canonical coefficients, and prove formal equivalence to the input, including empty prefixes.

The unchanged tactic script uses 3 declared prerequisites and contains 42 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_field_polynomial_left_pad_exists Alpha theorem; checked-use authorized prime_field_polynomial_left_pad_bounded Alpha theorem; checked-use authorized prime_field_polynomial_left_pad_equivalent Alpha theorem; checked-use authorized

Direct dependents

PG0038 prime_field_polynomial_common_representatives_at_length_exists PG0046 prime_field_polynomial_aligned_add_cancel_left PG0047 prime_field_polynomial_aligned_add_associative

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

42 script commands · 11 reading checkpoints · 1 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro K
  6. L6
    intro hp
  7. L7
    intro ha
  8. L8
    intro hlen
02Separate the logical casesL9–9

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

  1. L9
    cases hlen
03Establish hpadL10–15

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

  1. L10
    have hpad : ∃ ub. ∃ uc. PolynomialLeftPad(ab,ac,L,x,ub,uc)Definitions: PolynomialLeftPad
  2. L11
    specialize prime_field_polynomial_left_pad_exists (ab)
  3. L12
    specialize prime_field_polynomial_left_pad_exists (ac)
  4. L13
    specialize prime_field_polynomial_left_pad_exists (x)
  5. L14
    specialize prime_field_polynomial_left_pad_exists (L)
  6. L15
    apply prime_field_polynomial_left_pad_exists
04Separate the logical casesL16–17

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

  1. L16
    cases hpad
  2. L17
    cases hpad_witness
05Construct an explicit witnessL18–19

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

  1. L18
    exists x1
  2. L19
    exists x2
06Separate the logical casesL20–20

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

  1. L20
    split
07Calculate and transport equalitiesL21–21

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

  1. L21
    rewrite <- hlen_witness
08Use earlier factsL22–31

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

  1. L22
    specialize prime_field_polynomial_left_pad_bounded (p)
  2. L23
    specialize prime_field_polynomial_left_pad_bounded (ab)
  3. L24
    specialize prime_field_polynomial_left_pad_bounded (ac)
  4. L25
    specialize prime_field_polynomial_left_pad_bounded (L)
  5. L26
    specialize prime_field_polynomial_left_pad_bounded (x)
  6. L27
    specialize prime_field_polynomial_left_pad_bounded (x1)
  7. L28
    specialize prime_field_polynomial_left_pad_bounded (x2)
  8. L29
    apply prime_field_polynomial_left_pad_bounded
  9. L30
    exact hp
  10. L31
    exact ha
09Use earlier factsL32–32

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

  1. L32
    exact hpad_witness_witness
10Calculate and transport equalitiesL33–34

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

  1. L33
    rewrite <- hlen_witness
  2. L34
    rewrite <- hlen_witness
11Use earlier factsL35–42

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

  1. L35
    specialize prime_field_polynomial_left_pad_equivalent (ab)
  2. L36
    specialize prime_field_polynomial_left_pad_equivalent (ac)
  3. L37
    specialize prime_field_polynomial_left_pad_equivalent (L)
  4. L38
    specialize prime_field_polynomial_left_pad_equivalent (x)
  5. L39
    specialize prime_field_polynomial_left_pad_equivalent (x1)
  6. L40
    specialize prime_field_polynomial_left_pad_equivalent (x2)
  7. L41
    apply prime_field_polynomial_left_pad_equivalent
  8. L42
    exact hpad_witness_witness

Library-wide reading audit

Original exact command ledger · 42 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro K
  6. 0006intro hp
  7. 0007intro ha
  8. 0008intro hlen
  9. 0009cases hlen
  10. 0010have hpad : exists ub uc. (((forall pfp_repeat_index_alignment_constructed_padzeros. (exists pfa_gap_alignment_constructed_padzerosindex. pfa_gap_alignment_constructed_padzerosindex + S (pfp_repeat_index_alignment_constructed_padzeros) = (x)) -> (((exists ff_h_pfp_alignment_constructed_padzerosentry. ff_h_pfp_alignment_constructed_padzerosentry + S (0) = S ((S (pfp_repeat_index_alignment_constructed_padzeros)) * uc)) /\ exists ff_q_pfp_alignment_constructed_padzerosentry. ub = ff_q_pfp_alignment_constructed_padzerosentry * S ((S (pfp_repeat_index_alignment_constructed_padzeros)) * uc) + (0)))) /\ ((forall pfrep_index_alignment_constructed_pad pfrep_value_alignment_constructed_pad. (exists pfa_gap_alignment_constructed_padbound. pfa_gap_alignment_constructed_padbound + S (pfrep_index_alignment_constructed_pad) = (L)) -> (((exists ff_h_pfp_alignment_constructed_padinput. ff_h_pfp_alignment_constructed_padinput + S (pfrep_value_alignment_constructed_pad) = S ((S (pfrep_index_alignment_constructed_pad)) * ac)) /\ exists ff_q_pfp_alignment_constructed_padinput. ab = ff_q_pfp_alignment_constructed_padinput * S ((S (pfrep_index_alignment_constructed_pad)) * ac) + (pfrep_value_alignment_constructed_pad))) -> (((exists ff_h_pfp_alignment_constructed_padoutput. ff_h_pfp_alignment_constructed_padoutput + S (pfrep_value_alignment_constructed_pad) = S ((S ((x)+pfrep_index_alignment_constructed_pad)) * uc)) /\ exists ff_q_pfp_alignment_constructed_padoutput. ub = ff_q_pfp_alignment_constructed_padoutput * S ((S ((x)+pfrep_index_alignment_constructed_pad)) * uc) + (pfrep_value_alignment_constructed_pad)))))))
  11. 0011specialize prime_field_polynomial_left_pad_exists (ab)
  12. 0012specialize prime_field_polynomial_left_pad_exists (ac)
  13. 0013specialize prime_field_polynomial_left_pad_exists (x)
  14. 0014specialize prime_field_polynomial_left_pad_exists (L)
  15. 0015apply prime_field_polynomial_left_pad_exists
  16. 0016cases hpad
  17. 0017cases hpad_witness
  18. 0018exists x1
  19. 0019exists x2
  20. 0020split
  21. 0021rewrite <- hlen_witness
  22. 0022specialize prime_field_polynomial_left_pad_bounded (p)
  23. 0023specialize prime_field_polynomial_left_pad_bounded (ab)
  24. 0024specialize prime_field_polynomial_left_pad_bounded (ac)
  25. 0025specialize prime_field_polynomial_left_pad_bounded (L)
  26. 0026specialize prime_field_polynomial_left_pad_bounded (x)
  27. 0027specialize prime_field_polynomial_left_pad_bounded (x1)
  28. 0028specialize prime_field_polynomial_left_pad_bounded (x2)
  29. 0029apply prime_field_polynomial_left_pad_bounded
  30. 0030exact hp
  31. 0031exact ha
  32. 0032exact hpad_witness_witness
  33. 0033rewrite <- hlen_witness
  34. 0034rewrite <- hlen_witness
  35. 0035specialize prime_field_polynomial_left_pad_equivalent (ab)
  36. 0036specialize prime_field_polynomial_left_pad_equivalent (ac)
  37. 0037specialize prime_field_polynomial_left_pad_equivalent (L)
  38. 0038specialize prime_field_polynomial_left_pad_equivalent (x)
  39. 0039specialize prime_field_polynomial_left_pad_equivalent (x1)
  40. 0040specialize prime_field_polynomial_left_pad_equivalent (x2)
  41. 0041apply prime_field_polynomial_left_pad_equivalent
  42. 0042exact hpad_witness_witness