JT002F

jordan_tuple_normalize_exists

Canonical coordinate reduction works for every nonzero modulus, not just fields.

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

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ n. ∀ b. ∀ c. ∀ k. ¬n = 0 → ∃ x. ∃ y. BetaPrefixInto(x,y,k,n) ∧ JordanTupleCongruence(n,b,c,x,y,k)

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

Definition DAG

CanonicalModularResidue(m,a,r) · 1BetaPrefixInto(b,c,l,B) · 1FpCoefficientReduction(p,b,c,d,e,l) · 1JordanTupleCongruence(n,b,c,d,e,k) · 1

Actual proof prerequisites

prime_field_polynomial_normalization_exists · checked external prerequisiteprime_field_polynomial_normalization_bounded · checked external prerequisiteprime_field_polynomial_normalization_entry · checked external prerequisite
Original expanded first-order statement 
forall n b c k. ~(n=0) -> exists d e. ((forall jt_index_normalizebound. (exists jt_gap_normalizeboundindex. jt_gap_normalizeboundindex+S (jt_index_normalizebound)=(k)) -> exists jt_value_normalizebound. ((((exists fs_h_jt_normalizeboundat. fs_h_jt_normalizeboundat + S (jt_value_normalizebound) = S ((S (jt_index_normalizebound)) * e)) /\ exists fs_q_jt_normalizeboundat. d = fs_q_jt_normalizeboundat * S ((S (jt_index_normalizebound)) * e) + (jt_value_normalizebound))) /\ (exists jt_gap_normalizeboundvalue. jt_gap_normalizeboundvalue+S (jt_value_normalizebound)=(n)))) /\ (forall jt_index_normalizemod jt_left_normalizemod jt_right_normalizemod. (exists jt_gap_normalizemodindex. jt_gap_normalizemodindex+S (jt_index_normalizemod)=(k)) -> (((exists fs_h_jt_normalizemodleft. fs_h_jt_normalizemodleft + S (jt_left_normalizemod) = S ((S (jt_index_normalizemod)) * c)) /\ exists fs_q_jt_normalizemodleft. b = fs_q_jt_normalizemodleft * S ((S (jt_index_normalizemod)) * c) + (jt_left_normalizemod))) -> (((exists fs_h_jt_normalizemodright. fs_h_jt_normalizemodright + S (jt_right_normalizemod) = S ((S (jt_index_normalizemod)) * e)) /\ exists fs_q_jt_normalizemodright. d = fs_q_jt_normalizemodright * S ((S (jt_index_normalizemod)) * e) + (jt_right_normalizemod))) -> (exists jt_left_normalizemodmod jt_right_normalizemodmod. (jt_left_normalizemod)+(n)*jt_left_normalizemodmod=(jt_right_normalizemod)+(n)*jt_right_normalizemodmod)))

Complete tactic proof in conservative notation

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

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

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

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

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro k
  5. L5
    intro hn
02Establish hnormL6–12

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

  1. L6
    have hnorm : ∃ d. ∃ e. FpCoefficientReduction(n,b,c,d,e,k)Definitions: FpCoefficientReduction(n,b,c,d,e,k)Original native command in the exact edition
  2. L7
    specialize prime_field_polynomial_normalization_exists (n)
  3. L8
    specialize prime_field_polynomial_normalization_exists (b)
  4. L9
    specialize prime_field_polynomial_normalization_exists (c)
  5. L10
    specialize prime_field_polynomial_normalization_exists (k)
  6. L11
    apply prime_field_polynomial_normalization_exists
  7. L12
    exact hn
03Separate the logical casesL13–14

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

  1. L13
    cases hnorm
  2. L14
    cases hnorm_witness
04Construct an explicit witnessL15–16

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

  1. L15
    exists x
  2. L16
    exists x1
05Separate the logical casesL17–17

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

  1. L17
    split
06Use earlier factsL18–25

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

  1. L18
    specialize prime_field_polynomial_normalization_bounded (n)
  2. L19
    specialize prime_field_polynomial_normalization_bounded (b)
  3. L20
    specialize prime_field_polynomial_normalization_bounded (c)
  4. L21
    specialize prime_field_polynomial_normalization_bounded (x)
  5. L22
    specialize prime_field_polynomial_normalization_bounded (x1)
  6. L23
    specialize prime_field_polynomial_normalization_bounded (k)
  7. L24
    apply prime_field_polynomial_normalization_bounded
  8. L25
    exact hnorm_witness_witness
07Fix variables and assumptionsL26–31

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

  1. L26
    intro i
  2. L27
    intro a
  3. L28
    intro r
  4. L29
    intro hi
  5. L30
    intro ha
  6. L31
    intro hr
08Establish hvalueL32–41

Establish this local claim before using it. It is not an additional assumption.

  1. L32
    have hvalue : CanonicalModularResidue(n,a,r)Definitions: CanonicalModularResidue(n,a,r)Original native command in the exact edition
  2. L33
    specialize prime_field_polynomial_normalization_entry (n)
  3. L34
    specialize prime_field_polynomial_normalization_entry (b)
  4. L35
    specialize prime_field_polynomial_normalization_entry (c)
  5. L36
    specialize prime_field_polynomial_normalization_entry (x)
  6. L37
    specialize prime_field_polynomial_normalization_entry (x1)
  7. L38
    specialize prime_field_polynomial_normalization_entry (k)
  8. L39
    specialize prime_field_polynomial_normalization_entry (i)
  9. L40
    specialize prime_field_polynomial_normalization_entry (a)
  10. L41
    specialize prime_field_polynomial_normalization_entry (r)
09Use earlier factsL42–46

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

  1. L42
    apply prime_field_polynomial_normalization_entry
  2. L43
    exact hnorm_witness_witness
  3. L44
    exact hi
  4. L45
    exact ha
  5. L46
    exact hr
10Separate the logical casesL47–47

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

  1. L47
    cases hvalue
11Use earlier factsL48–48

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

  1. L48
    exact hvalue_right

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005intro hn
  6. 0006have hnorm : ∃ d. ∃ e. FpCoefficientReduction(n,b,c,d,e,k)
  7. 0007specialize prime_field_polynomial_normalization_exists (n)
  8. 0008specialize prime_field_polynomial_normalization_exists (b)
  9. 0009specialize prime_field_polynomial_normalization_exists (c)
  10. 0010specialize prime_field_polynomial_normalization_exists (k)
  11. 0011apply prime_field_polynomial_normalization_exists
  12. 0012exact hn
  13. 0013cases hnorm
  14. 0014cases hnorm_witness
  15. 0015exists x
  16. 0016exists x1
  17. 0017split
  18. 0018specialize prime_field_polynomial_normalization_bounded (n)
  19. 0019specialize prime_field_polynomial_normalization_bounded (b)
  20. 0020specialize prime_field_polynomial_normalization_bounded (c)
  21. 0021specialize prime_field_polynomial_normalization_bounded (x)
  22. 0022specialize prime_field_polynomial_normalization_bounded (x1)
  23. 0023specialize prime_field_polynomial_normalization_bounded (k)
  24. 0024apply prime_field_polynomial_normalization_bounded
  25. 0025exact hnorm_witness_witness
  26. 0026intro i
  27. 0027intro a
  28. 0028intro r
  29. 0029intro hi
  30. 0030intro ha
  31. 0031intro hr
  32. 0032have hvalue : CanonicalModularResidue(n,a,r)
  33. 0033specialize prime_field_polynomial_normalization_entry (n)
  34. 0034specialize prime_field_polynomial_normalization_entry (b)
  35. 0035specialize prime_field_polynomial_normalization_entry (c)
  36. 0036specialize prime_field_polynomial_normalization_entry (x)
  37. 0037specialize prime_field_polynomial_normalization_entry (x1)
  38. 0038specialize prime_field_polynomial_normalization_entry (k)
  39. 0039specialize prime_field_polynomial_normalization_entry (i)
  40. 0040specialize prime_field_polynomial_normalization_entry (a)
  41. 0041specialize prime_field_polynomial_normalization_entry (r)
  42. 0042apply prime_field_polynomial_normalization_entry
  43. 0043exact hnorm_witness_witness
  44. 0044exact hi
  45. 0045exact ha
  46. 0046exact hr
  47. 0047cases hvalue
  48. 0048exact hvalue_right