PP0007

prime_field_polynomial_normalization_transport

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

Reencoding both finite prefixes preserves every actual normalization witness.

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 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)))))))))

Constructive proof overview

Generated structural guide

Reencoding both finite prefixes preserves every actual normalization witness.

The unchanged tactic script uses 0 declared prerequisites and contains 38 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

none

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

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.

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 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: CanonicalModularResidueBetaAt
  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 exact 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 : exists a r. ((((exists ff_h_pfp_transport_chosen_source. ff_h_pfp_transport_chosen_source + S (a) = S ((S (i)) * c)) /\ exists ff_q_pfp_transport_chosen_source. b = ff_q_pfp_transport_chosen_source * S ((S (i)) * c) + (a))) /\ (((((exists ff_h_pfp_transport_chosen_target. ff_h_pfp_transport_chosen_target + S (r) = S ((S (i)) * e)) /\ exists ff_q_pfp_transport_chosen_target. d = ff_q_pfp_transport_chosen_target * S ((S (i)) * e) + (r))) /\ ((((exists pfa_gap_transport_chosen_residuebound. pfa_gap_transport_chosen_residuebound + S (r) = (p)) /\ ((exists pfa_offset_left_transport_chosen_residuecongruence pfa_offset_right_transport_chosen_residuecongruence. (a) + (p) * pfa_offset_left_transport_chosen_residuecongruence = (r) + (p) * pfa_offset_right_transport_chosen_residuecongruence))))))))
  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