PP0007

prime_field_polynomial_normalization_transport

Reencoding both finite prefixes preserves every actual normalization witness.

Alpha v34 checked-use · first admitted v31 · 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.

Length is representation length, not polynomial degree. Leading zeros and the empty zero polynomial are allowed; the canonical argument guard x<p also applies to the empty case. Evaluation is defined by actual field-operation steps, not an assumed residue invariant. Polynomial division, gcd, irreducibles and general prime-power extension fields remain open; this does not close G091.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ d. ∀ e. ∀ B. ∀ C. ∀ D. ∀ E. ∀ l. BetaPrefixEqual(b,c,B,C,l) → BetaPrefixEqual(d,e,D,E,l) → FpCoefficientReduction(p,b,c,d,e,l) → FpCoefficientReduction(p,B,C,D,E,l)

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

Definition DAG

CanonicalModularResidue(m,a,r) · 1BetaPrefixEqual(b,c,d,e,l) · 2FpCoefficientReduction(p,b,c,d,e,l) · 2BetaAt(b,c,i,x) · 2

Actual proof prerequisites

none
Original expanded first-order statement 
forall p b c d e B C D E l. (forall mdr_i_pfp_transport_source mdr_a_pfp_transport_source. (exists mdr_gap_pfp_transport_sourceb. mdr_gap_pfp_transport_sourceb + S (mdr_i_pfp_transport_source) = (l)) -> (((exists ff_h_mdr_pfp_transport_sourceo. ff_h_mdr_pfp_transport_sourceo + S (mdr_a_pfp_transport_source) = S ((S (mdr_i_pfp_transport_source)) * c)) /\ exists ff_q_mdr_pfp_transport_sourceo. b = ff_q_mdr_pfp_transport_sourceo * S ((S (mdr_i_pfp_transport_source)) * c) + (mdr_a_pfp_transport_source))) -> (((exists ff_h_mdr_pfp_transport_sourcen. ff_h_mdr_pfp_transport_sourcen + S (mdr_a_pfp_transport_source) = S ((S (mdr_i_pfp_transport_source)) * C)) /\ exists ff_q_mdr_pfp_transport_sourcen. B = ff_q_mdr_pfp_transport_sourcen * S ((S (mdr_i_pfp_transport_source)) * C) + (mdr_a_pfp_transport_source)))) -> (forall mdr_i_pfp_transport_target mdr_a_pfp_transport_target. (exists mdr_gap_pfp_transport_targetb. mdr_gap_pfp_transport_targetb + S (mdr_i_pfp_transport_target) = (l)) -> (((exists ff_h_mdr_pfp_transport_targeto. ff_h_mdr_pfp_transport_targeto + S (mdr_a_pfp_transport_target) = S ((S (mdr_i_pfp_transport_target)) * e)) /\ exists ff_q_mdr_pfp_transport_targeto. d = ff_q_mdr_pfp_transport_targeto * S ((S (mdr_i_pfp_transport_target)) * e) + (mdr_a_pfp_transport_target))) -> (((exists ff_h_mdr_pfp_transport_targetn. ff_h_mdr_pfp_transport_targetn + S (mdr_a_pfp_transport_target) = S ((S (mdr_i_pfp_transport_target)) * E)) /\ exists ff_q_mdr_pfp_transport_targetn. D = ff_q_mdr_pfp_transport_targetn * S ((S (mdr_i_pfp_transport_target)) * E) + (mdr_a_pfp_transport_target)))) -> (forall pfp_index_transport_old. (exists pfa_gap_transport_oldindex. pfa_gap_transport_oldindex + S (pfp_index_transport_old) = (l)) -> exists pfp_source_transport_old pfp_residue_transport_old. ((((exists ff_h_pfp_transport_oldsource. ff_h_pfp_transport_oldsource + S (pfp_source_transport_old) = S ((S (pfp_index_transport_old)) * c)) /\ exists ff_q_pfp_transport_oldsource. b = ff_q_pfp_transport_oldsource * S ((S (pfp_index_transport_old)) * c) + (pfp_source_transport_old))) /\ (((((exists ff_h_pfp_transport_oldtarget. ff_h_pfp_transport_oldtarget + S (pfp_residue_transport_old) = S ((S (pfp_index_transport_old)) * e)) /\ exists ff_q_pfp_transport_oldtarget. d = ff_q_pfp_transport_oldtarget * S ((S (pfp_index_transport_old)) * e) + (pfp_residue_transport_old))) /\ ((((exists pfa_gap_transport_oldresiduebound. pfa_gap_transport_oldresiduebound + S (pfp_residue_transport_old) = (p)) /\ ((exists pfa_offset_left_transport_oldresiduecongruence pfa_offset_right_transport_oldresiduecongruence. (pfp_source_transport_old) + (p) * pfa_offset_left_transport_oldresiduecongruence = (pfp_residue_transport_old) + (p) * pfa_offset_right_transport_oldresiduecongruence))))))))) -> (forall pfp_index_transport_new. (exists pfa_gap_transport_newindex. pfa_gap_transport_newindex + S (pfp_index_transport_new) = (l)) -> exists pfp_source_transport_new pfp_residue_transport_new. ((((exists ff_h_pfp_transport_newsource. ff_h_pfp_transport_newsource + S (pfp_source_transport_new) = S ((S (pfp_index_transport_new)) * C)) /\ exists ff_q_pfp_transport_newsource. B = ff_q_pfp_transport_newsource * S ((S (pfp_index_transport_new)) * C) + (pfp_source_transport_new))) /\ (((((exists ff_h_pfp_transport_newtarget. ff_h_pfp_transport_newtarget + S (pfp_residue_transport_new) = S ((S (pfp_index_transport_new)) * E)) /\ exists ff_q_pfp_transport_newtarget. D = ff_q_pfp_transport_newtarget * S ((S (pfp_index_transport_new)) * E) + (pfp_residue_transport_new))) /\ ((((exists pfa_gap_transport_newresiduebound. pfa_gap_transport_newresiduebound + S (pfp_residue_transport_new) = (p)) /\ ((exists pfa_offset_left_transport_newresiduecongruence pfa_offset_right_transport_newresiduecongruence. (pfp_source_transport_new) + (p) * pfa_offset_left_transport_newresiduecongruence = (pfp_residue_transport_new) + (p) * pfa_offset_right_transport_newresiduecongruence)))))))))

Complete tactic proof in conservative notation

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

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

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 d
  5. L5
    intro e
  6. L6
    intro B
  7. L7
    intro C
  8. L8
    intro D
  9. L9
    intro E
  10. L10
    intro l
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hs
  2. L12
    intro ht
  3. L13
    intro h
  4. L14
    intro i
  5. L15
    intro hi
03Establish hpointL16–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply h.

  1. L16
    have hpoint : ∃ a. ∃ r. BetaAt(b,c,i,a) ∧ (BetaAt(d,e,i,r) ∧ CanonicalModularResidue(p,a,r))Definitions: BetaAt(b,c,i,a)BetaAt(d,e,i,r)CanonicalModularResidue(p,a,r)Original native command in the exact edition
  2. L17
    specialize h (i)
  3. L18
    apply h
  4. L19
    exact hi
04Separate the logical casesL20–23

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

  1. L20
    cases hpoint
  2. L21
    cases hpoint_witness
  3. L22
    cases hpoint_witness_witness
  4. L23
    cases hpoint_witness_witness_right
05Construct an explicit witnessL24–25

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

  1. L24
    exists x
  2. L25
    exists x1
06Separate the logical casesL26–26

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

  1. L26
    split
07Use earlier factsL27–31

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

  1. L27
    specialize hs (i)
  2. L28
    specialize hs (x)
  3. L29
    apply hs
  4. L30
    exact hi
  5. L31
    exact hpoint_witness_witness_left
08Separate the logical casesL32–32

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

  1. L32
    split
09Use earlier factsL33–38

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

  1. L33
    specialize ht (i)
  2. L34
    specialize ht (x1)
  3. L35
    apply ht
  4. L36
    exact hi
  5. L37
    exact hpoint_witness_witness_right_left
  6. L38
    exact hpoint_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro B
  7. 0007intro C
  8. 0008intro D
  9. 0009intro E
  10. 0010intro l
  11. 0011intro hs
  12. 0012intro ht
  13. 0013intro h
  14. 0014intro i
  15. 0015intro hi
  16. 0016have hpoint : ∃ a. ∃ r. BetaAt(b,c,i,a) ∧ (BetaAt(d,e,i,r) ∧ CanonicalModularResidue(p,a,r))
  17. 0017specialize h (i)
  18. 0018apply h
  19. 0019exact hi
  20. 0020cases hpoint
  21. 0021cases hpoint_witness
  22. 0022cases hpoint_witness_witness
  23. 0023cases hpoint_witness_witness_right
  24. 0024exists x
  25. 0025exists x1
  26. 0026split
  27. 0027specialize hs (i)
  28. 0028specialize hs (x)
  29. 0029apply hs
  30. 0030exact hi
  31. 0031exact hpoint_witness_witness_left
  32. 0032split
  33. 0033specialize ht (i)
  34. 0034specialize ht (x1)
  35. 0035apply ht
  36. 0036exact hi
  37. 0037exact hpoint_witness_witness_right_left
  38. 0038exact hpoint_witness_witness_right_right