EI000B

eisenstein_coordinate_norm_transport

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

The norm depends only on the represented integers, not on a chosen positive/negative decomposition of either coordinate.

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 original first-admission records.

Exact expanded first-order arithmetic statement

forall ap an bp bn cp cn dp dn n. (((ap) + (cn)) = ((cp) + (an))) -> (((bp) + (dn)) = ((dp) + (bn))) -> (((((((((ap) * (ap))) + (((an) * (an))))) + (((((bp) * (bp))) + (((bn) * (bn))))))) + (((((ap) * (bn))) + (((an) * (bp)))))) = ((((((((((ap) * (an))) + (((an) * (ap))))) + (((((bp) * (bn))) + (((bn) * (bp))))))) + (((((ap) * (bp))) + (((an) * (bn))))))) + (n))) -> (((((((((cp) * (cp))) + (((cn) * (cn))))) + (((((dp) * (dp))) + (((dn) * (dn))))))) + (((((cp) * (dn))) + (((cn) * (dp)))))) = ((((((((((cp) * (cn))) + (((cn) * (cp))))) + (((((dp) * (dn))) + (((dn) * (dp))))))) + (((((cp) * (dp))) + (((cn) * (dn))))))) + (n)))

Constructive proof overview

Generated structural guide

The norm depends only on the represented integers, not on a chosen positive/negative decomposition of either coordinate.

The unchanged tactic script uses 4 declared prerequisites and contains 87 exact native proof lines.

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

Proof neighborhood

Direct dependencies

matrix_integer_pair_product_balance Alpha theorem; checked-use authorized matrix_integer_pair_negation_balance Alpha theorem; checked-use authorized integer_span_pair_add_congruence Alpha theorem; checked-use authorized EI000A eisenstein_pair_natural_value_transport

Direct dependents

EI000C eisenstein_coordinate_norm_exists EI0033 eisenstein_signed_euclidean_division_exists EI0035 eisenstein_norm_for_representation

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

87 script commands · 13 reading checkpoints · 6 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.

Named ingredients (1)
eisenstein pair natural value transport
01Fix variables and assumptionsL1–10

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

  1. L1
    intro ap
  2. L2
    intro an
  3. L3
    intro bp
  4. L4
    intro bn
  5. L5
    intro cp
  6. L6
    intro cn
  7. L7
    intro dp
  8. L8
    intro dn
  9. L9
    intro n
  10. L10
    intro ha
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hb
  2. L12
    intro hnorm
03Establish haaL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix integer pair product balance.

  1. L13
    have haa : ((((((ap) * (ap))) + (((an) * (an))))) + (((((cp) * (cn))) + (((cn) * (cp)))))) = ((((((cp) * (cp))) + (((cn) * (cn))))) + (((((ap) * (an))) + (((an) * (ap))))))
  2. L14
    specialize matrix_integer_pair_product_balance ap
  3. L15
    specialize matrix_integer_pair_product_balance an
  4. L16
    specialize matrix_integer_pair_product_balance cp
  5. L17
    specialize matrix_integer_pair_product_balance cn
  6. L18
    specialize matrix_integer_pair_product_balance ap
  7. L19
    specialize matrix_integer_pair_product_balance an
  8. L20
    specialize matrix_integer_pair_product_balance cp
  9. L21
    specialize matrix_integer_pair_product_balance cn
  10. L22
    apply matrix_integer_pair_product_balance
04Use earlier factsL23–24

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

  1. L23
    exact ha
  2. L24
    exact ha
05Establish hbbL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix integer pair product balance.

  1. L25
    have hbb : ((((((bp) * (bp))) + (((bn) * (bn))))) + (((((dp) * (dn))) + (((dn) * (dp)))))) = ((((((dp) * (dp))) + (((dn) * (dn))))) + (((((bp) * (bn))) + (((bn) * (bp))))))
  2. L26
    specialize matrix_integer_pair_product_balance bp
  3. L27
    specialize matrix_integer_pair_product_balance bn
  4. L28
    specialize matrix_integer_pair_product_balance dp
  5. L29
    specialize matrix_integer_pair_product_balance dn
  6. L30
    specialize matrix_integer_pair_product_balance bp
  7. L31
    specialize matrix_integer_pair_product_balance bn
  8. L32
    specialize matrix_integer_pair_product_balance dp
  9. L33
    specialize matrix_integer_pair_product_balance dn
  10. L34
    apply matrix_integer_pair_product_balance
06Use earlier factsL35–36

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

  1. L35
    exact hb
  2. L36
    exact hb
07Establish habL37–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix integer pair product balance.

  1. L37
    have hab : ((((((ap) * (bp))) + (((an) * (bn))))) + (((((cp) * (dn))) + (((cn) * (dp)))))) = ((((((cp) * (dp))) + (((cn) * (dn))))) + (((((ap) * (bn))) + (((an) * (bp))))))
  2. L38
    specialize matrix_integer_pair_product_balance ap
  3. L39
    specialize matrix_integer_pair_product_balance an
  4. L40
    specialize matrix_integer_pair_product_balance cp
  5. L41
    specialize matrix_integer_pair_product_balance cn
  6. L42
    specialize matrix_integer_pair_product_balance bp
  7. L43
    specialize matrix_integer_pair_product_balance bn
  8. L44
    specialize matrix_integer_pair_product_balance dp
  9. L45
    specialize matrix_integer_pair_product_balance dn
  10. L46
    apply matrix_integer_pair_product_balance
08Use earlier factsL47–48

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

  1. L47
    exact ha
  2. L48
    exact hb
09Establish hsquaresL49–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply integer span pair add congruence.

  1. L49
    have hsquares : ((((((((ap) * (ap))) + (((an) * (an))))) + (((((bp) * (bp))) + (((bn) * (bn))))))) + (((((((cp) * (cn))) + (((cn) * (cp))))) + (((((dp) * (dn))) + (((dn) * (dp)))))))) = ((((((((cp) * (cp))) + (((cn) * (cn))))) + (((((dp) * (dp))) + (((dn) * (dn))))))) + (((((((ap) * (an))) + (((an) * (ap))))) + (((((bp) * (bn))) + (((bn) * (bp))))))))
  2. L50
    specialize integer_span_pair_add_congruence ((((ap) * (ap))) + (((an) * (an))))
  3. L51
    specialize integer_span_pair_add_congruence ((((ap) * (an))) + (((an) * (ap))))
  4. L52
    specialize integer_span_pair_add_congruence ((((bp) * (bp))) + (((bn) * (bn))))
  5. L53
    specialize integer_span_pair_add_congruence ((((bp) * (bn))) + (((bn) * (bp))))
  6. L54
    specialize integer_span_pair_add_congruence ((((cp) * (cp))) + (((cn) * (cn))))
  7. L55
    specialize integer_span_pair_add_congruence ((((cp) * (cn))) + (((cn) * (cp))))
  8. L56
    specialize integer_span_pair_add_congruence ((((dp) * (dp))) + (((dn) * (dn))))
  9. L57
    specialize integer_span_pair_add_congruence ((((dp) * (dn))) + (((dn) * (dp))))
  10. L58
    apply integer_span_pair_add_congruence
10Use earlier factsL59–60

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

  1. L59
    exact haa
  2. L60
    exact hbb
11Establish hnegativeL61–67

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix integer pair negation balance.

  1. L61
    have hnegative : ((((((ap) * (bn))) + (((an) * (bp))))) + (((((cp) * (dp))) + (((cn) * (dn)))))) = ((((((cp) * (dn))) + (((cn) * (dp))))) + (((((ap) * (bp))) + (((an) * (bn))))))
  2. L62
    specialize matrix_integer_pair_negation_balance ((((ap) * (bp))) + (((an) * (bn))))
  3. L63
    specialize matrix_integer_pair_negation_balance ((((ap) * (bn))) + (((an) * (bp))))
  4. L64
    specialize matrix_integer_pair_negation_balance ((((cp) * (dp))) + (((cn) * (dn))))
  5. L65
    specialize matrix_integer_pair_negation_balance ((((cp) * (dn))) + (((cn) * (dp))))
  6. L66
    apply matrix_integer_pair_negation_balance
  7. L67
    exact hab
12Establish hnormpairL68–77

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply integer span pair add congruence.

  1. L68
    have hnormpair : ((((((((((ap) * (ap))) + (((an) * (an))))) + (((((bp) * (bp))) + (((bn) * (bn))))))) + (((((ap) * (bn))) + (((an) * (bp))))))) + (((((((((cp) * (cn))) + (((cn) * (cp))))) + (((((dp) * (dn))) + (((dn) * (dp))))))) + (((((cp) * (dp))) + (((cn) * (dn)))))))) = ((((((((((cp) * (cp))) + (((cn) * (cn))))) + (((((dp) * (dp))) + (((dn) * (dn))))))) + (((((cp) * (dn))) + (((cn) * (dp))))))) + (((((((((ap) * (an))) + (((an) * (ap))))) + (((((bp) * (bn))) + (((bn) * (bp))))))) + (((((ap) * (bp))) + (((an) * (bn))))))))
  2. L69
    specialize integer_span_pair_add_congruence ((((((ap) * (ap))) + (((an) * (an))))) + (((((bp) * (bp))) + (((bn) * (bn))))))
  3. L70
    specialize integer_span_pair_add_congruence ((((((ap) * (an))) + (((an) * (ap))))) + (((((bp) * (bn))) + (((bn) * (bp))))))
  4. L71
    specialize integer_span_pair_add_congruence ((((ap) * (bn))) + (((an) * (bp))))
  5. L72
    specialize integer_span_pair_add_congruence ((((ap) * (bp))) + (((an) * (bn))))
  6. L73
    specialize integer_span_pair_add_congruence ((((((cp) * (cp))) + (((cn) * (cn))))) + (((((dp) * (dp))) + (((dn) * (dn))))))
  7. L74
    specialize integer_span_pair_add_congruence ((((((cp) * (cn))) + (((cn) * (cp))))) + (((((dp) * (dn))) + (((dn) * (dp))))))
  8. L75
    specialize integer_span_pair_add_congruence ((((cp) * (dn))) + (((cn) * (dp))))
  9. L76
    specialize integer_span_pair_add_congruence ((((cp) * (dp))) + (((cn) * (dn))))
  10. L77
    apply integer_span_pair_add_congruence
13Use earlier factsL78–87

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

  1. L78
    exact hsquares
  2. L79
    exact hnegative
  3. L80
    specialize eisenstein_pair_natural_value_transport ((((((((ap) * (ap))) + (((an) * (an))))) + (((((bp) * (bp))) + (((bn) * (bn))))))) + (((((ap) * (bn))) + (((an) * (bp))))))
  4. L81
    specialize eisenstein_pair_natural_value_transport ((((((((ap) * (an))) + (((an) * (ap))))) + (((((bp) * (bn))) + (((bn) * (bp))))))) + (((((ap) * (bp))) + (((an) * (bn))))))
  5. L82
    specialize eisenstein_pair_natural_value_transport ((((((((cp) * (cp))) + (((cn) * (cn))))) + (((((dp) * (dp))) + (((dn) * (dn))))))) + (((((cp) * (dn))) + (((cn) * (dp))))))
  6. L83
    specialize eisenstein_pair_natural_value_transport ((((((((cp) * (cn))) + (((cn) * (cp))))) + (((((dp) * (dn))) + (((dn) * (dp))))))) + (((((cp) * (dp))) + (((cn) * (dn))))))
  7. L84
    specialize eisenstein_pair_natural_value_transport n
  8. L85
    apply eisenstein_pair_natural_value_transport
  9. L86
    exact hnorm
  10. L87
    exact hnormpair

Library-wide reading audit

Original exact command ledger · 87 lines
  1. 0001intro ap
  2. 0002intro an
  3. 0003intro bp
  4. 0004intro bn
  5. 0005intro cp
  6. 0006intro cn
  7. 0007intro dp
  8. 0008intro dn
  9. 0009intro n
  10. 0010intro ha
  11. 0011intro hb
  12. 0012intro hnorm
  13. 0013have haa : ((((((ap) * (ap))) + (((an) * (an))))) + (((((cp) * (cn))) + (((cn) * (cp)))))) = ((((((cp) * (cp))) + (((cn) * (cn))))) + (((((ap) * (an))) + (((an) * (ap))))))
  14. 0014specialize matrix_integer_pair_product_balance ap
  15. 0015specialize matrix_integer_pair_product_balance an
  16. 0016specialize matrix_integer_pair_product_balance cp
  17. 0017specialize matrix_integer_pair_product_balance cn
  18. 0018specialize matrix_integer_pair_product_balance ap
  19. 0019specialize matrix_integer_pair_product_balance an
  20. 0020specialize matrix_integer_pair_product_balance cp
  21. 0021specialize matrix_integer_pair_product_balance cn
  22. 0022apply matrix_integer_pair_product_balance
  23. 0023exact ha
  24. 0024exact ha
  25. 0025have hbb : ((((((bp) * (bp))) + (((bn) * (bn))))) + (((((dp) * (dn))) + (((dn) * (dp)))))) = ((((((dp) * (dp))) + (((dn) * (dn))))) + (((((bp) * (bn))) + (((bn) * (bp))))))
  26. 0026specialize matrix_integer_pair_product_balance bp
  27. 0027specialize matrix_integer_pair_product_balance bn
  28. 0028specialize matrix_integer_pair_product_balance dp
  29. 0029specialize matrix_integer_pair_product_balance dn
  30. 0030specialize matrix_integer_pair_product_balance bp
  31. 0031specialize matrix_integer_pair_product_balance bn
  32. 0032specialize matrix_integer_pair_product_balance dp
  33. 0033specialize matrix_integer_pair_product_balance dn
  34. 0034apply matrix_integer_pair_product_balance
  35. 0035exact hb
  36. 0036exact hb
  37. 0037have hab : ((((((ap) * (bp))) + (((an) * (bn))))) + (((((cp) * (dn))) + (((cn) * (dp)))))) = ((((((cp) * (dp))) + (((cn) * (dn))))) + (((((ap) * (bn))) + (((an) * (bp))))))
  38. 0038specialize matrix_integer_pair_product_balance ap
  39. 0039specialize matrix_integer_pair_product_balance an
  40. 0040specialize matrix_integer_pair_product_balance cp
  41. 0041specialize matrix_integer_pair_product_balance cn
  42. 0042specialize matrix_integer_pair_product_balance bp
  43. 0043specialize matrix_integer_pair_product_balance bn
  44. 0044specialize matrix_integer_pair_product_balance dp
  45. 0045specialize matrix_integer_pair_product_balance dn
  46. 0046apply matrix_integer_pair_product_balance
  47. 0047exact ha
  48. 0048exact hb
  49. 0049have hsquares : ((((((((ap) * (ap))) + (((an) * (an))))) + (((((bp) * (bp))) + (((bn) * (bn))))))) + (((((((cp) * (cn))) + (((cn) * (cp))))) + (((((dp) * (dn))) + (((dn) * (dp)))))))) = ((((((((cp) * (cp))) + (((cn) * (cn))))) + (((((dp) * (dp))) + (((dn) * (dn))))))) + (((((((ap) * (an))) + (((an) * (ap))))) + (((((bp) * (bn))) + (((bn) * (bp))))))))
  50. 0050specialize integer_span_pair_add_congruence ((((ap) * (ap))) + (((an) * (an))))
  51. 0051specialize integer_span_pair_add_congruence ((((ap) * (an))) + (((an) * (ap))))
  52. 0052specialize integer_span_pair_add_congruence ((((bp) * (bp))) + (((bn) * (bn))))
  53. 0053specialize integer_span_pair_add_congruence ((((bp) * (bn))) + (((bn) * (bp))))
  54. 0054specialize integer_span_pair_add_congruence ((((cp) * (cp))) + (((cn) * (cn))))
  55. 0055specialize integer_span_pair_add_congruence ((((cp) * (cn))) + (((cn) * (cp))))
  56. 0056specialize integer_span_pair_add_congruence ((((dp) * (dp))) + (((dn) * (dn))))
  57. 0057specialize integer_span_pair_add_congruence ((((dp) * (dn))) + (((dn) * (dp))))
  58. 0058apply integer_span_pair_add_congruence
  59. 0059exact haa
  60. 0060exact hbb
  61. 0061have hnegative : ((((((ap) * (bn))) + (((an) * (bp))))) + (((((cp) * (dp))) + (((cn) * (dn)))))) = ((((((cp) * (dn))) + (((cn) * (dp))))) + (((((ap) * (bp))) + (((an) * (bn))))))
  62. 0062specialize matrix_integer_pair_negation_balance ((((ap) * (bp))) + (((an) * (bn))))
  63. 0063specialize matrix_integer_pair_negation_balance ((((ap) * (bn))) + (((an) * (bp))))
  64. 0064specialize matrix_integer_pair_negation_balance ((((cp) * (dp))) + (((cn) * (dn))))
  65. 0065specialize matrix_integer_pair_negation_balance ((((cp) * (dn))) + (((cn) * (dp))))
  66. 0066apply matrix_integer_pair_negation_balance
  67. 0067exact hab
  68. 0068have hnormpair : ((((((((((ap) * (ap))) + (((an) * (an))))) + (((((bp) * (bp))) + (((bn) * (bn))))))) + (((((ap) * (bn))) + (((an) * (bp))))))) + (((((((((cp) * (cn))) + (((cn) * (cp))))) + (((((dp) * (dn))) + (((dn) * (dp))))))) + (((((cp) * (dp))) + (((cn) * (dn)))))))) = ((((((((((cp) * (cp))) + (((cn) * (cn))))) + (((((dp) * (dp))) + (((dn) * (dn))))))) + (((((cp) * (dn))) + (((cn) * (dp))))))) + (((((((((ap) * (an))) + (((an) * (ap))))) + (((((bp) * (bn))) + (((bn) * (bp))))))) + (((((ap) * (bp))) + (((an) * (bn))))))))
  69. 0069specialize integer_span_pair_add_congruence ((((((ap) * (ap))) + (((an) * (an))))) + (((((bp) * (bp))) + (((bn) * (bn))))))
  70. 0070specialize integer_span_pair_add_congruence ((((((ap) * (an))) + (((an) * (ap))))) + (((((bp) * (bn))) + (((bn) * (bp))))))
  71. 0071specialize integer_span_pair_add_congruence ((((ap) * (bn))) + (((an) * (bp))))
  72. 0072specialize integer_span_pair_add_congruence ((((ap) * (bp))) + (((an) * (bn))))
  73. 0073specialize integer_span_pair_add_congruence ((((((cp) * (cp))) + (((cn) * (cn))))) + (((((dp) * (dp))) + (((dn) * (dn))))))
  74. 0074specialize integer_span_pair_add_congruence ((((((cp) * (cn))) + (((cn) * (cp))))) + (((((dp) * (dn))) + (((dn) * (dp))))))
  75. 0075specialize integer_span_pair_add_congruence ((((cp) * (dn))) + (((cn) * (dp))))
  76. 0076specialize integer_span_pair_add_congruence ((((cp) * (dp))) + (((cn) * (dn))))
  77. 0077apply integer_span_pair_add_congruence
  78. 0078exact hsquares
  79. 0079exact hnegative
  80. 0080specialize eisenstein_pair_natural_value_transport ((((((((ap) * (ap))) + (((an) * (an))))) + (((((bp) * (bp))) + (((bn) * (bn))))))) + (((((ap) * (bn))) + (((an) * (bp))))))
  81. 0081specialize eisenstein_pair_natural_value_transport ((((((((ap) * (an))) + (((an) * (ap))))) + (((((bp) * (bn))) + (((bn) * (bp))))))) + (((((ap) * (bp))) + (((an) * (bn))))))
  82. 0082specialize eisenstein_pair_natural_value_transport ((((((((cp) * (cp))) + (((cn) * (cn))))) + (((((dp) * (dp))) + (((dn) * (dn))))))) + (((((cp) * (dn))) + (((cn) * (dp))))))
  83. 0083specialize eisenstein_pair_natural_value_transport ((((((((cp) * (cn))) + (((cn) * (cp))))) + (((((dp) * (dn))) + (((dn) * (dp))))))) + (((((cp) * (dp))) + (((cn) * (dn))))))
  84. 0084specialize eisenstein_pair_natural_value_transport n
  85. 0085apply eisenstein_pair_natural_value_transport
  86. 0086exact hnorm
  87. 0087exact hnormpair