JT002F

jordan_tuple_normalize_exists

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

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

Exact expanded first-order arithmetic 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)))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 48 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_field_polynomial_normalization_exists Alpha theorem; checked-use authorized prime_field_polynomial_normalization_bounded Alpha theorem; checked-use authorized prime_field_polynomial_normalization_entry Alpha theorem; checked-use authorized

Direct dependents

JT0032 jordan_canonical_crt_tuple_exists JT0045 jordan_enumeration_reduce_primitive

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

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.

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–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
  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 : ((exists jt_gap_normalizeresiduebound. jt_gap_normalizeresiduebound+S (r)=(n)) /\ (exists jt_left_normalizeresiduemod jt_right_normalizeresiduemod. (a)+(n)*jt_left_normalizeresiduemod=(r)+(n)*jt_right_normalizeresiduemod))
  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 exact command ledger · 48 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005intro hn
  6. 0006have hnorm : exists d e. forall jt_index_normalizeactual. (exists jt_gap_normalizeactualindex. jt_gap_normalizeactualindex+S (jt_index_normalizeactual)=(k)) -> exists jt_input_normalizeactual jt_output_normalizeactual. ((((exists fs_h_jt_normalizeactualinput. fs_h_jt_normalizeactualinput + S (jt_input_normalizeactual) = S ((S (jt_index_normalizeactual)) * c)) /\ exists fs_q_jt_normalizeactualinput. b = fs_q_jt_normalizeactualinput * S ((S (jt_index_normalizeactual)) * c) + (jt_input_normalizeactual))) /\ (((((exists fs_h_jt_normalizeactualoutput. fs_h_jt_normalizeactualoutput + S (jt_output_normalizeactual) = S ((S (jt_index_normalizeactual)) * e)) /\ exists fs_q_jt_normalizeactualoutput. d = fs_q_jt_normalizeactualoutput * S ((S (jt_index_normalizeactual)) * e) + (jt_output_normalizeactual))) /\ (((exists jt_gap_normalizeactualbound. jt_gap_normalizeactualbound+S (jt_output_normalizeactual)=(n)) /\ (exists jt_left_normalizeactualmod jt_right_normalizeactualmod. (jt_input_normalizeactual)+(n)*jt_left_normalizeactualmod=(jt_output_normalizeactual)+(n)*jt_right_normalizeactualmod))))))
  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 : ((exists jt_gap_normalizeresiduebound. jt_gap_normalizeresiduebound+S (r)=(n)) /\ (exists jt_left_normalizeresiduemod jt_right_normalizeresiduemod. (a)+(n)*jt_left_normalizeresiduemod=(r)+(n)*jt_right_normalizeresiduemod))
  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