PG0038

prime_field_polynomial_common_representatives_at_length_exists

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

Construct two actual canonical common-length representatives by independent leading-zero padding at any supplied common upper bound.

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 bb bc M K. (~((p) = 1) /\ forall pfa_factor_left_common_at_prime pfa_factor_right_common_at_prime. (p) = pfa_factor_left_common_at_prime * pfa_factor_right_common_at_prime -> pfa_factor_left_common_at_prime = 1 \/ pfa_factor_right_common_at_prime = 1) -> (forall fom_index_pfp_common_at_A. (exists fom_gap_pfp_common_at_A_index_bound. fom_gap_pfp_common_at_A_index_bound + S (fom_index_pfp_common_at_A) = L) -> exists fom_value_pfp_common_at_A. ((((exists fom_beta_height_pfp_common_at_A_entry. fom_beta_height_pfp_common_at_A_entry + S (fom_value_pfp_common_at_A) = S ((S (fom_index_pfp_common_at_A)) * ac)) /\ exists fom_beta_quotient_pfp_common_at_A_entry. ab = fom_beta_quotient_pfp_common_at_A_entry * S ((S (fom_index_pfp_common_at_A)) * ac) + (fom_value_pfp_common_at_A))) /\ (exists fom_gap_pfp_common_at_A_value_bound. fom_gap_pfp_common_at_A_value_bound + S (fom_value_pfp_common_at_A) = p))) -> (forall fom_index_pfp_common_at_B. (exists fom_gap_pfp_common_at_B_index_bound. fom_gap_pfp_common_at_B_index_bound + S (fom_index_pfp_common_at_B) = M) -> exists fom_value_pfp_common_at_B. ((((exists fom_beta_height_pfp_common_at_B_entry. fom_beta_height_pfp_common_at_B_entry + S (fom_value_pfp_common_at_B) = S ((S (fom_index_pfp_common_at_B)) * bc)) /\ exists fom_beta_quotient_pfp_common_at_B_entry. bb = fom_beta_quotient_pfp_common_at_B_entry * S ((S (fom_index_pfp_common_at_B)) * bc) + (fom_value_pfp_common_at_B))) /\ (exists fom_gap_pfp_common_at_B_value_bound. fom_gap_pfp_common_at_B_value_bound + S (fom_value_pfp_common_at_B) = p))) -> (exists pfrep_gap_common_at_L. pfrep_gap_common_at_L+(L)=(K)) -> (exists pfrep_gap_common_at_M. pfrep_gap_common_at_M+(M)=(K)) -> (exists ub uc vb vc. ((forall fom_index_pfp_common_at_output_left_bounded. (exists fom_gap_pfp_common_at_output_left_bounded_index_bound. fom_gap_pfp_common_at_output_left_bounded_index_bound + S (fom_index_pfp_common_at_output_left_bounded) = K) -> exists fom_value_pfp_common_at_output_left_bounded. ((((exists fom_beta_height_pfp_common_at_output_left_bounded_entry. fom_beta_height_pfp_common_at_output_left_bounded_entry + S (fom_value_pfp_common_at_output_left_bounded) = S ((S (fom_index_pfp_common_at_output_left_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_common_at_output_left_bounded_entry. ub = fom_beta_quotient_pfp_common_at_output_left_bounded_entry * S ((S (fom_index_pfp_common_at_output_left_bounded)) * uc) + (fom_value_pfp_common_at_output_left_bounded))) /\ (exists fom_gap_pfp_common_at_output_left_bounded_value_bound. fom_gap_pfp_common_at_output_left_bounded_value_bound + S (fom_value_pfp_common_at_output_left_bounded) = p))) /\ (((forall fom_index_pfp_common_at_output_right_bounded. (exists fom_gap_pfp_common_at_output_right_bounded_index_bound. fom_gap_pfp_common_at_output_right_bounded_index_bound + S (fom_index_pfp_common_at_output_right_bounded) = K) -> exists fom_value_pfp_common_at_output_right_bounded. ((((exists fom_beta_height_pfp_common_at_output_right_bounded_entry. fom_beta_height_pfp_common_at_output_right_bounded_entry + S (fom_value_pfp_common_at_output_right_bounded) = S ((S (fom_index_pfp_common_at_output_right_bounded)) * vc)) /\ exists fom_beta_quotient_pfp_common_at_output_right_bounded_entry. vb = fom_beta_quotient_pfp_common_at_output_right_bounded_entry * S ((S (fom_index_pfp_common_at_output_right_bounded)) * vc) + (fom_value_pfp_common_at_output_right_bounded))) /\ (exists fom_gap_pfp_common_at_output_right_bounded_value_bound. fom_gap_pfp_common_at_output_right_bounded_value_bound + S (fom_value_pfp_common_at_output_right_bounded) = p))) /\ ((((forall pfrep_power_common_at_output_common_left pfrep_left_common_at_output_common_left pfrep_right_common_at_output_common_left. ((exists pfrep_position_common_at_output_common_leftfirst. ((pfrep_position_common_at_output_common_leftfirst+S (pfrep_power_common_at_output_common_left)=(L)) /\ ((((exists ff_h_pfp_common_at_output_common_leftfirstentry. ff_h_pfp_common_at_output_common_leftfirstentry + S (pfrep_left_common_at_output_common_left) = S ((S (pfrep_position_common_at_output_common_leftfirst)) * ac)) /\ exists ff_q_pfp_common_at_output_common_leftfirstentry. ab = ff_q_pfp_common_at_output_common_leftfirstentry * S ((S (pfrep_position_common_at_output_common_leftfirst)) * ac) + (pfrep_left_common_at_output_common_left)))))) \/ (((exists pfrep_gap_common_at_output_common_leftfirstoutside. pfrep_gap_common_at_output_common_leftfirstoutside+(L)=(pfrep_power_common_at_output_common_left)) /\ (((pfrep_left_common_at_output_common_left)=0))))) -> ((exists pfrep_position_common_at_output_common_leftsecond. ((pfrep_position_common_at_output_common_leftsecond+S (pfrep_power_common_at_output_common_left)=(K)) /\ ((((exists ff_h_pfp_common_at_output_common_leftsecondentry. ff_h_pfp_common_at_output_common_leftsecondentry + S (pfrep_right_common_at_output_common_left) = S ((S (pfrep_position_common_at_output_common_leftsecond)) * uc)) /\ exists ff_q_pfp_common_at_output_common_leftsecondentry. ub = ff_q_pfp_common_at_output_common_leftsecondentry * S ((S (pfrep_position_common_at_output_common_leftsecond)) * uc) + (pfrep_right_common_at_output_common_left)))))) \/ (((exists pfrep_gap_common_at_output_common_leftsecondoutside. pfrep_gap_common_at_output_common_leftsecondoutside+(K)=(pfrep_power_common_at_output_common_left)) /\ (((pfrep_right_common_at_output_common_left)=0))))) -> pfrep_left_common_at_output_common_left=pfrep_right_common_at_output_common_left) /\ ((forall pfrep_power_common_at_output_common_right pfrep_left_common_at_output_common_right pfrep_right_common_at_output_common_right. ((exists pfrep_position_common_at_output_common_rightfirst. ((pfrep_position_common_at_output_common_rightfirst+S (pfrep_power_common_at_output_common_right)=(M)) /\ ((((exists ff_h_pfp_common_at_output_common_rightfirstentry. ff_h_pfp_common_at_output_common_rightfirstentry + S (pfrep_left_common_at_output_common_right) = S ((S (pfrep_position_common_at_output_common_rightfirst)) * bc)) /\ exists ff_q_pfp_common_at_output_common_rightfirstentry. bb = ff_q_pfp_common_at_output_common_rightfirstentry * S ((S (pfrep_position_common_at_output_common_rightfirst)) * bc) + (pfrep_left_common_at_output_common_right)))))) \/ (((exists pfrep_gap_common_at_output_common_rightfirstoutside. pfrep_gap_common_at_output_common_rightfirstoutside+(M)=(pfrep_power_common_at_output_common_right)) /\ (((pfrep_left_common_at_output_common_right)=0))))) -> ((exists pfrep_position_common_at_output_common_rightsecond. ((pfrep_position_common_at_output_common_rightsecond+S (pfrep_power_common_at_output_common_right)=(K)) /\ ((((exists ff_h_pfp_common_at_output_common_rightsecondentry. ff_h_pfp_common_at_output_common_rightsecondentry + S (pfrep_right_common_at_output_common_right) = S ((S (pfrep_position_common_at_output_common_rightsecond)) * vc)) /\ exists ff_q_pfp_common_at_output_common_rightsecondentry. vb = ff_q_pfp_common_at_output_common_rightsecondentry * S ((S (pfrep_position_common_at_output_common_rightsecond)) * vc) + (pfrep_right_common_at_output_common_right)))))) \/ (((exists pfrep_gap_common_at_output_common_rightsecondoutside. pfrep_gap_common_at_output_common_rightsecondoutside+(K)=(pfrep_power_common_at_output_common_right)) /\ (((pfrep_right_common_at_output_common_right)=0))))) -> pfrep_left_common_at_output_common_right=pfrep_right_common_at_output_common_right)))))))))

Constructive proof overview

Generated structural guide

Construct two actual canonical common-length representatives by independent leading-zero padding at any supplied common upper bound.

The unchanged tactic script uses 1 declared prerequisite and contains 50 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PG0035 prime_field_polynomial_bounded_representative_at_length_exists

Direct dependents

PG0039 prime_field_polynomial_common_representatives_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

50 script commands · 13 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 bounded representative at length exists

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–10

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 bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro K
  9. L9
    intro hp
  10. L10
    intro ha
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hb
  2. L12
    intro hL
  3. L13
    intro hM
03Establish huL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial bounded representative at length exists.

  1. L14
    have hu : ∃ ub. ∃ uc. BetaPrefixInto(ub,uc,K,p) ∧ PolynomialEquivalent(ab,ac,L,ub,uc,K)Definitions: BetaPrefixIntoPolynomialEquivalent
  2. L15
    specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  3. L16
    specialize prime_field_polynomial_bounded_representative_at_length_exists (ab)
  4. L17
    specialize prime_field_polynomial_bounded_representative_at_length_exists (ac)
  5. L18
    specialize prime_field_polynomial_bounded_representative_at_length_exists (L)
  6. L19
    specialize prime_field_polynomial_bounded_representative_at_length_exists (K)
  7. L20
    apply prime_field_polynomial_bounded_representative_at_length_exists
  8. L21
    exact hp
  9. L22
    exact ha
  10. L23
    exact hL
04Separate the logical casesL24–26

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

  1. L24
    cases hu
  2. L25
    cases hu_witness
  3. L26
    cases hu_witness_witness
05Establish hvL27–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial bounded representative at length exists.

  1. L27
    have hv : ∃ vb. ∃ vc. BetaPrefixInto(vb,vc,K,p) ∧ PolynomialEquivalent(bb,bc,M,vb,vc,K)Definitions: BetaPrefixIntoPolynomialEquivalent
  2. L28
    specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  3. L29
    specialize prime_field_polynomial_bounded_representative_at_length_exists (bb)
  4. L30
    specialize prime_field_polynomial_bounded_representative_at_length_exists (bc)
  5. L31
    specialize prime_field_polynomial_bounded_representative_at_length_exists (M)
  6. L32
    specialize prime_field_polynomial_bounded_representative_at_length_exists (K)
  7. L33
    apply prime_field_polynomial_bounded_representative_at_length_exists
  8. L34
    exact hp
  9. L35
    exact hb
  10. L36
    exact hM
06Separate the logical casesL37–39

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

  1. L37
    cases hv
  2. L38
    cases hv_witness
  3. L39
    cases hv_witness_witness
07Construct an explicit witnessL40–43

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

  1. L40
    exists x
  2. L41
    exists x1
  3. L42
    exists x2
  4. L43
    exists x3
08Separate the logical casesL44–44

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

  1. L44
    split
09Use earlier factsL45–45

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

  1. L45
    exact hu_witness_witness_left
10Separate the logical casesL46–46

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

  1. L46
    split
11Use earlier factsL47–47

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

  1. L47
    exact hv_witness_witness_left
12Separate the logical casesL48–48

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

  1. L48
    split
13Use earlier factsL49–50

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

  1. L49
    exact hu_witness_witness_right
  2. L50
    exact hv_witness_witness_right

Library-wide reading audit

Original exact command ledger · 50 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro K
  9. 0009intro hp
  10. 0010intro ha
  11. 0011intro hb
  12. 0012intro hL
  13. 0013intro hM
  14. 0014have hu : exists ub uc. ((forall fom_index_pfp_common_construct_left_bounded. (exists fom_gap_pfp_common_construct_left_bounded_index_bound. fom_gap_pfp_common_construct_left_bounded_index_bound + S (fom_index_pfp_common_construct_left_bounded) = K) -> exists fom_value_pfp_common_construct_left_bounded. ((((exists fom_beta_height_pfp_common_construct_left_bounded_entry. fom_beta_height_pfp_common_construct_left_bounded_entry + S (fom_value_pfp_common_construct_left_bounded) = S ((S (fom_index_pfp_common_construct_left_bounded)) * uc)) /\ exists fom_beta_quotient_pfp_common_construct_left_bounded_entry. ub = fom_beta_quotient_pfp_common_construct_left_bounded_entry * S ((S (fom_index_pfp_common_construct_left_bounded)) * uc) + (fom_value_pfp_common_construct_left_bounded))) /\ (exists fom_gap_pfp_common_construct_left_bounded_value_bound. fom_gap_pfp_common_construct_left_bounded_value_bound + S (fom_value_pfp_common_construct_left_bounded) = p))) /\ ((forall pfrep_power_common_construct_left_equivalent pfrep_left_common_construct_left_equivalent pfrep_right_common_construct_left_equivalent. ((exists pfrep_position_common_construct_left_equivalentfirst. ((pfrep_position_common_construct_left_equivalentfirst+S (pfrep_power_common_construct_left_equivalent)=(L)) /\ ((((exists ff_h_pfp_common_construct_left_equivalentfirstentry. ff_h_pfp_common_construct_left_equivalentfirstentry + S (pfrep_left_common_construct_left_equivalent) = S ((S (pfrep_position_common_construct_left_equivalentfirst)) * ac)) /\ exists ff_q_pfp_common_construct_left_equivalentfirstentry. ab = ff_q_pfp_common_construct_left_equivalentfirstentry * S ((S (pfrep_position_common_construct_left_equivalentfirst)) * ac) + (pfrep_left_common_construct_left_equivalent)))))) \/ (((exists pfrep_gap_common_construct_left_equivalentfirstoutside. pfrep_gap_common_construct_left_equivalentfirstoutside+(L)=(pfrep_power_common_construct_left_equivalent)) /\ (((pfrep_left_common_construct_left_equivalent)=0))))) -> ((exists pfrep_position_common_construct_left_equivalentsecond. ((pfrep_position_common_construct_left_equivalentsecond+S (pfrep_power_common_construct_left_equivalent)=(K)) /\ ((((exists ff_h_pfp_common_construct_left_equivalentsecondentry. ff_h_pfp_common_construct_left_equivalentsecondentry + S (pfrep_right_common_construct_left_equivalent) = S ((S (pfrep_position_common_construct_left_equivalentsecond)) * uc)) /\ exists ff_q_pfp_common_construct_left_equivalentsecondentry. ub = ff_q_pfp_common_construct_left_equivalentsecondentry * S ((S (pfrep_position_common_construct_left_equivalentsecond)) * uc) + (pfrep_right_common_construct_left_equivalent)))))) \/ (((exists pfrep_gap_common_construct_left_equivalentsecondoutside. pfrep_gap_common_construct_left_equivalentsecondoutside+(K)=(pfrep_power_common_construct_left_equivalent)) /\ (((pfrep_right_common_construct_left_equivalent)=0))))) -> pfrep_left_common_construct_left_equivalent=pfrep_right_common_construct_left_equivalent)))
  15. 0015specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  16. 0016specialize prime_field_polynomial_bounded_representative_at_length_exists (ab)
  17. 0017specialize prime_field_polynomial_bounded_representative_at_length_exists (ac)
  18. 0018specialize prime_field_polynomial_bounded_representative_at_length_exists (L)
  19. 0019specialize prime_field_polynomial_bounded_representative_at_length_exists (K)
  20. 0020apply prime_field_polynomial_bounded_representative_at_length_exists
  21. 0021exact hp
  22. 0022exact ha
  23. 0023exact hL
  24. 0024cases hu
  25. 0025cases hu_witness
  26. 0026cases hu_witness_witness
  27. 0027have hv : exists vb vc. ((forall fom_index_pfp_common_construct_right_bounded. (exists fom_gap_pfp_common_construct_right_bounded_index_bound. fom_gap_pfp_common_construct_right_bounded_index_bound + S (fom_index_pfp_common_construct_right_bounded) = K) -> exists fom_value_pfp_common_construct_right_bounded. ((((exists fom_beta_height_pfp_common_construct_right_bounded_entry. fom_beta_height_pfp_common_construct_right_bounded_entry + S (fom_value_pfp_common_construct_right_bounded) = S ((S (fom_index_pfp_common_construct_right_bounded)) * vc)) /\ exists fom_beta_quotient_pfp_common_construct_right_bounded_entry. vb = fom_beta_quotient_pfp_common_construct_right_bounded_entry * S ((S (fom_index_pfp_common_construct_right_bounded)) * vc) + (fom_value_pfp_common_construct_right_bounded))) /\ (exists fom_gap_pfp_common_construct_right_bounded_value_bound. fom_gap_pfp_common_construct_right_bounded_value_bound + S (fom_value_pfp_common_construct_right_bounded) = p))) /\ ((forall pfrep_power_common_construct_right_equivalent pfrep_left_common_construct_right_equivalent pfrep_right_common_construct_right_equivalent. ((exists pfrep_position_common_construct_right_equivalentfirst. ((pfrep_position_common_construct_right_equivalentfirst+S (pfrep_power_common_construct_right_equivalent)=(M)) /\ ((((exists ff_h_pfp_common_construct_right_equivalentfirstentry. ff_h_pfp_common_construct_right_equivalentfirstentry + S (pfrep_left_common_construct_right_equivalent) = S ((S (pfrep_position_common_construct_right_equivalentfirst)) * bc)) /\ exists ff_q_pfp_common_construct_right_equivalentfirstentry. bb = ff_q_pfp_common_construct_right_equivalentfirstentry * S ((S (pfrep_position_common_construct_right_equivalentfirst)) * bc) + (pfrep_left_common_construct_right_equivalent)))))) \/ (((exists pfrep_gap_common_construct_right_equivalentfirstoutside. pfrep_gap_common_construct_right_equivalentfirstoutside+(M)=(pfrep_power_common_construct_right_equivalent)) /\ (((pfrep_left_common_construct_right_equivalent)=0))))) -> ((exists pfrep_position_common_construct_right_equivalentsecond. ((pfrep_position_common_construct_right_equivalentsecond+S (pfrep_power_common_construct_right_equivalent)=(K)) /\ ((((exists ff_h_pfp_common_construct_right_equivalentsecondentry. ff_h_pfp_common_construct_right_equivalentsecondentry + S (pfrep_right_common_construct_right_equivalent) = S ((S (pfrep_position_common_construct_right_equivalentsecond)) * vc)) /\ exists ff_q_pfp_common_construct_right_equivalentsecondentry. vb = ff_q_pfp_common_construct_right_equivalentsecondentry * S ((S (pfrep_position_common_construct_right_equivalentsecond)) * vc) + (pfrep_right_common_construct_right_equivalent)))))) \/ (((exists pfrep_gap_common_construct_right_equivalentsecondoutside. pfrep_gap_common_construct_right_equivalentsecondoutside+(K)=(pfrep_power_common_construct_right_equivalent)) /\ (((pfrep_right_common_construct_right_equivalent)=0))))) -> pfrep_left_common_construct_right_equivalent=pfrep_right_common_construct_right_equivalent)))
  28. 0028specialize prime_field_polynomial_bounded_representative_at_length_exists (p)
  29. 0029specialize prime_field_polynomial_bounded_representative_at_length_exists (bb)
  30. 0030specialize prime_field_polynomial_bounded_representative_at_length_exists (bc)
  31. 0031specialize prime_field_polynomial_bounded_representative_at_length_exists (M)
  32. 0032specialize prime_field_polynomial_bounded_representative_at_length_exists (K)
  33. 0033apply prime_field_polynomial_bounded_representative_at_length_exists
  34. 0034exact hp
  35. 0035exact hb
  36. 0036exact hM
  37. 0037cases hv
  38. 0038cases hv_witness
  39. 0039cases hv_witness_witness
  40. 0040exists x
  41. 0041exists x1
  42. 0042exists x2
  43. 0043exists x3
  44. 0044split
  45. 0045exact hu_witness_witness_left
  46. 0046split
  47. 0047exact hv_witness_witness_left
  48. 0048split
  49. 0049exact hu_witness_witness_right
  50. 0050exact hv_witness_witness_right