PX0010

prime_field_polynomial_equivalent_transitive

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

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

∀ b. ∀ c. ∀ L. ∀ d. ∀ e. ∀ M. ∀ f. ∀ g. ∀ N. PolynomialEquivalent(b,c,L,d,e,M) → PolynomialEquivalent(d,e,M,f,g,N) → PolynomialEquivalent(b,c,L,f,g,N)

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

Definition DAG

PolynomialPowerCoefficient(b,c,L,k,a) · 1PolynomialEquivalent(b,c,L,d,e,M) · 3

Actual proof prerequisites

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

Complete tactic proof in conservative notation

All 36 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

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.

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 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 : ∃ z. PolynomialPowerCoefficient(d,e,M,k,z)Definitions: PolynomialPowerCoefficient(d,e,M,k,z)Original native command in the exact edition
  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 defined 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 : ∃ z. PolynomialPowerCoefficient(d,e,M,k,z)
  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