PX0010

prime_field_polynomial_equivalent_transitive

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

Transitivity obtains an actual intermediate coefficient; it never assumes existential decoding.

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 b c L d e M f g N. (forall pfrep_power_equivalent_transitive_a pfrep_left_equivalent_transitive_a pfrep_right_equivalent_transitive_a. ((exists pfrep_position_equivalent_transitive_afirst. ((pfrep_position_equivalent_transitive_afirst+S (pfrep_power_equivalent_transitive_a)=(L)) /\ ((((exists ff_h_pfp_equivalent_transitive_afirstentry. ff_h_pfp_equivalent_transitive_afirstentry + S (pfrep_left_equivalent_transitive_a) = S ((S (pfrep_position_equivalent_transitive_afirst)) * c)) /\ exists ff_q_pfp_equivalent_transitive_afirstentry. b = ff_q_pfp_equivalent_transitive_afirstentry * S ((S (pfrep_position_equivalent_transitive_afirst)) * c) + (pfrep_left_equivalent_transitive_a)))))) \/ (((exists pfrep_gap_equivalent_transitive_afirstoutside. pfrep_gap_equivalent_transitive_afirstoutside+(L)=(pfrep_power_equivalent_transitive_a)) /\ (((pfrep_left_equivalent_transitive_a)=0))))) -> ((exists pfrep_position_equivalent_transitive_asecond. ((pfrep_position_equivalent_transitive_asecond+S (pfrep_power_equivalent_transitive_a)=(M)) /\ ((((exists ff_h_pfp_equivalent_transitive_asecondentry. ff_h_pfp_equivalent_transitive_asecondentry + S (pfrep_right_equivalent_transitive_a) = S ((S (pfrep_position_equivalent_transitive_asecond)) * e)) /\ exists ff_q_pfp_equivalent_transitive_asecondentry. d = ff_q_pfp_equivalent_transitive_asecondentry * S ((S (pfrep_position_equivalent_transitive_asecond)) * e) + (pfrep_right_equivalent_transitive_a)))))) \/ (((exists pfrep_gap_equivalent_transitive_asecondoutside. pfrep_gap_equivalent_transitive_asecondoutside+(M)=(pfrep_power_equivalent_transitive_a)) /\ (((pfrep_right_equivalent_transitive_a)=0))))) -> pfrep_left_equivalent_transitive_a=pfrep_right_equivalent_transitive_a) -> (forall pfrep_power_equivalent_transitive_b pfrep_left_equivalent_transitive_b pfrep_right_equivalent_transitive_b. ((exists pfrep_position_equivalent_transitive_bfirst. ((pfrep_position_equivalent_transitive_bfirst+S (pfrep_power_equivalent_transitive_b)=(M)) /\ ((((exists ff_h_pfp_equivalent_transitive_bfirstentry. ff_h_pfp_equivalent_transitive_bfirstentry + S (pfrep_left_equivalent_transitive_b) = S ((S (pfrep_position_equivalent_transitive_bfirst)) * e)) /\ exists ff_q_pfp_equivalent_transitive_bfirstentry. d = ff_q_pfp_equivalent_transitive_bfirstentry * S ((S (pfrep_position_equivalent_transitive_bfirst)) * e) + (pfrep_left_equivalent_transitive_b)))))) \/ (((exists pfrep_gap_equivalent_transitive_bfirstoutside. pfrep_gap_equivalent_transitive_bfirstoutside+(M)=(pfrep_power_equivalent_transitive_b)) /\ (((pfrep_left_equivalent_transitive_b)=0))))) -> ((exists pfrep_position_equivalent_transitive_bsecond. ((pfrep_position_equivalent_transitive_bsecond+S (pfrep_power_equivalent_transitive_b)=(N)) /\ ((((exists ff_h_pfp_equivalent_transitive_bsecondentry. ff_h_pfp_equivalent_transitive_bsecondentry + S (pfrep_right_equivalent_transitive_b) = S ((S (pfrep_position_equivalent_transitive_bsecond)) * g)) /\ exists ff_q_pfp_equivalent_transitive_bsecondentry. f = ff_q_pfp_equivalent_transitive_bsecondentry * S ((S (pfrep_position_equivalent_transitive_bsecond)) * g) + (pfrep_right_equivalent_transitive_b)))))) \/ (((exists pfrep_gap_equivalent_transitive_bsecondoutside. pfrep_gap_equivalent_transitive_bsecondoutside+(N)=(pfrep_power_equivalent_transitive_b)) /\ (((pfrep_right_equivalent_transitive_b)=0))))) -> pfrep_left_equivalent_transitive_b=pfrep_right_equivalent_transitive_b) -> (forall pfrep_power_equivalent_transitive_result pfrep_left_equivalent_transitive_result pfrep_right_equivalent_transitive_result. ((exists pfrep_position_equivalent_transitive_resultfirst. ((pfrep_position_equivalent_transitive_resultfirst+S (pfrep_power_equivalent_transitive_result)=(L)) /\ ((((exists ff_h_pfp_equivalent_transitive_resultfirstentry. ff_h_pfp_equivalent_transitive_resultfirstentry + S (pfrep_left_equivalent_transitive_result) = S ((S (pfrep_position_equivalent_transitive_resultfirst)) * c)) /\ exists ff_q_pfp_equivalent_transitive_resultfirstentry. b = ff_q_pfp_equivalent_transitive_resultfirstentry * S ((S (pfrep_position_equivalent_transitive_resultfirst)) * c) + (pfrep_left_equivalent_transitive_result)))))) \/ (((exists pfrep_gap_equivalent_transitive_resultfirstoutside. pfrep_gap_equivalent_transitive_resultfirstoutside+(L)=(pfrep_power_equivalent_transitive_result)) /\ (((pfrep_left_equivalent_transitive_result)=0))))) -> ((exists pfrep_position_equivalent_transitive_resultsecond. ((pfrep_position_equivalent_transitive_resultsecond+S (pfrep_power_equivalent_transitive_result)=(N)) /\ ((((exists ff_h_pfp_equivalent_transitive_resultsecondentry. ff_h_pfp_equivalent_transitive_resultsecondentry + S (pfrep_right_equivalent_transitive_result) = S ((S (pfrep_position_equivalent_transitive_resultsecond)) * g)) /\ exists ff_q_pfp_equivalent_transitive_resultsecondentry. f = ff_q_pfp_equivalent_transitive_resultsecondentry * S ((S (pfrep_position_equivalent_transitive_resultsecond)) * g) + (pfrep_right_equivalent_transitive_result)))))) \/ (((exists pfrep_gap_equivalent_transitive_resultsecondoutside. pfrep_gap_equivalent_transitive_resultsecondoutside+(N)=(pfrep_power_equivalent_transitive_result)) /\ (((pfrep_right_equivalent_transitive_result)=0))))) -> pfrep_left_equivalent_transitive_result=pfrep_right_equivalent_transitive_result)

Constructive proof overview

Generated structural guide

Transitivity obtains an actual intermediate coefficient; it never assumes existential decoding.

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

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

Proof neighborhood

Direct dependencies

PX000C prime_field_polynomial_power_coefficient_exists

Direct dependents

PX006E prime_field_polynomial_convolution_left_padding_equivalent_left PX006F prime_field_polynomial_convolution_left_padding_equivalent_right PX0070 prime_field_polynomial_convolution_both_left_paddings_equivalent PX0072 prime_field_polynomial_equivalent_implies_left_pad PX0079 prime_field_polynomial_convolution_equivalent_congruent

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

36 script commands · 7 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.

Named ingredients (1)
prime field polynomial power coefficient exists
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro L
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro M
  7. L7
    intro f
  8. L8
    intro g
  9. L9
    intro N
  10. L10
    intro he
02Fix variables and assumptionsL11–16

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

  1. L11
    intro hf
  2. L12
    intro k
  3. L13
    intro a
  4. L14
    intro r
  5. L15
    intro ha
  6. L16
    intro hr
03Establish hvL17–22

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

  1. L17
    have hv : exists z. ((exists pfrep_position_equivalent_middle. ((pfrep_position_equivalent_middle+S (k)=(M)) /\ ((((exists ff_h_pfp_equivalent_middleentry. ff_h_pfp_equivalent_middleentry + S (z) = S ((S (pfrep_position_equivalent_middle)) * e)) /\ exists ff_q_pfp_equivalent_middleentry. d = ff_q_pfp_equivalent_middleentry * S ((S (pfrep_position_equivalent_middle)) * e) + (z)))))) \/ (((exists pfrep_gap_equivalent_middleoutside. pfrep_gap_equivalent_middleoutside+(M)=(k)) /\ (((z)=0)))))
  2. L18
    specialize prime_field_polynomial_power_coefficient_exists (d)
  3. L19
    specialize prime_field_polynomial_power_coefficient_exists (e)
  4. L20
    specialize prime_field_polynomial_power_coefficient_exists (M)
  5. L21
    specialize prime_field_polynomial_power_coefficient_exists (k)
  6. L22
    apply prime_field_polynomial_power_coefficient_exists
04Separate the logical casesL23–23

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

  1. L23
    cases hv
05Calculate and transport equalitiesL24–24

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

  1. L24
    trans x
06Use earlier factsL25–34

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

  1. L25
    specialize he (k)
  2. L26
    specialize he (a)
  3. L27
    specialize he (x)
  4. L28
    apply he
  5. L29
    exact ha
  6. L30
    exact hv_witness
  7. L31
    specialize hf (k)
  8. L32
    specialize hf (x)
  9. L33
    specialize hf (r)
  10. L34
    apply hf
07Use earlier factsL35–36

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

  1. L35
    exact hv_witness
  2. L36
    exact hr

Library-wide reading audit

Original exact command ledger · 36 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro L
  4. 0004intro d
  5. 0005intro e
  6. 0006intro M
  7. 0007intro f
  8. 0008intro g
  9. 0009intro N
  10. 0010intro he
  11. 0011intro hf
  12. 0012intro k
  13. 0013intro a
  14. 0014intro r
  15. 0015intro ha
  16. 0016intro hr
  17. 0017have hv : exists z. ((exists pfrep_position_equivalent_middle. ((pfrep_position_equivalent_middle+S (k)=(M)) /\ ((((exists ff_h_pfp_equivalent_middleentry. ff_h_pfp_equivalent_middleentry + S (z) = S ((S (pfrep_position_equivalent_middle)) * e)) /\ exists ff_q_pfp_equivalent_middleentry. d = ff_q_pfp_equivalent_middleentry * S ((S (pfrep_position_equivalent_middle)) * e) + (z)))))) \/ (((exists pfrep_gap_equivalent_middleoutside. pfrep_gap_equivalent_middleoutside+(M)=(k)) /\ (((z)=0)))))
  18. 0018specialize prime_field_polynomial_power_coefficient_exists (d)
  19. 0019specialize prime_field_polynomial_power_coefficient_exists (e)
  20. 0020specialize prime_field_polynomial_power_coefficient_exists (M)
  21. 0021specialize prime_field_polynomial_power_coefficient_exists (k)
  22. 0022apply prime_field_polynomial_power_coefficient_exists
  23. 0023cases hv
  24. 0024trans x
  25. 0025specialize he (k)
  26. 0026specialize he (a)
  27. 0027specialize he (x)
  28. 0028apply he
  29. 0029exact ha
  30. 0030exact hv_witness
  31. 0031specialize hf (k)
  32. 0032specialize hf (x)
  33. 0033specialize hf (r)
  34. 0034apply hf
  35. 0035exact hv_witness
  36. 0036exact hr