EI000C

eisenstein_coordinate_norm_exists

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

Every arbitrary signed-coordinate representation has a natural Eisenstein norm, by actual signed normalization and checked representative invariance.

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. exists n. (((((((((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)))

Constructive proof overview

Generated structural guide

Every arbitrary signed-coordinate representation has a natural Eisenstein norm, by actual signed normalization and checked representative invariance.

The unchanged tactic script uses 5 declared prerequisites and contains 57 exact native proof lines.

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

Proof neighborhood

Direct dependencies

signed_balance_total Alpha theorem; checked-use authorized signed_decode_normal Alpha theorem; checked-use authorized EI0009 eisenstein_normal_coordinate_norm_exists EI000B eisenstein_coordinate_norm_transport add_comm Stable theorem; checked-use authorized

Direct dependents

EI002F eisenstein_coordinate_norm_product EI0033 eisenstein_signed_euclidean_division_exists EI0036 eisenstein_norm_exists

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

57 script commands · 18 reading checkpoints · 3 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 (2)
eisenstein normal coordinate norm existseisenstein coordinate norm transport
01Fix variables and assumptionsL1–4

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
02Establish hfirstL5–8

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

  1. L5
    have hfirst : exists code. (exists sb_pos_ee_first sb_neg_ee_first. (((code = 2 * sb_pos_ee_first /\ sb_neg_ee_first = 0) \/ exists sd_half_ee_first. ((code = 2 * sd_half_ee_first + 1 /\ sb_pos_ee_first = 0) /\ sb_neg_ee_first = S sd_half_ee_first)) /\ ap + sb_neg_ee_first = an + sb_pos_ee_first))
  2. L6
    specialize signed_balance_total ap
  3. L7
    specialize signed_balance_total an
  4. L8
    apply signed_balance_total
03Separate the logical casesL9–12

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

  1. L9
    cases hfirst
  2. L10
    cases hfirst_witness
  3. L11
    cases hfirst_witness_witness
  4. L12
    cases hfirst_witness_witness_witness
04Establish hsecondL13–16

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

  1. L13
    have hsecond : exists code. (exists sb_pos_ee_second sb_neg_ee_second. (((code = 2 * sb_pos_ee_second /\ sb_neg_ee_second = 0) \/ exists sd_half_ee_second. ((code = 2 * sd_half_ee_second + 1 /\ sb_pos_ee_second = 0) /\ sb_neg_ee_second = S sd_half_ee_second)) /\ bp + sb_neg_ee_second = bn + sb_pos_ee_second))
  2. L14
    specialize signed_balance_total bp
  3. L15
    specialize signed_balance_total bn
  4. L16
    apply signed_balance_total
05Separate the logical casesL17–20

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

  1. L17
    cases hsecond
  2. L18
    cases hsecond_witness
  3. L19
    cases hsecond_witness_witness
  4. L20
    cases hsecond_witness_witness_witness
06Establish hnormL21–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein normal coordinate norm exists.

  1. L21
    have hnorm : exists n. ((((((((x1) * (x1))) + (((x2) * (x2))))) + (((((x4) * (x4))) + (((x5) * (x5))))))) + (((((x1) * (x5))) + (((x2) * (x4)))))) = ((((((((((x1) * (x2))) + (((x2) * (x1))))) + (((((x4) * (x5))) + (((x5) * (x4))))))) + (((((x1) * (x4))) + (((x2) * (x5))))))) + (n))
  2. L22
    specialize eisenstein_normal_coordinate_norm_exists x1
  3. L23
    specialize eisenstein_normal_coordinate_norm_exists x2
  4. L24
    specialize eisenstein_normal_coordinate_norm_exists x4
  5. L25
    specialize eisenstein_normal_coordinate_norm_exists x5
  6. L26
    apply eisenstein_normal_coordinate_norm_exists
  7. L27
    specialize signed_decode_normal x
  8. L28
    specialize signed_decode_normal x1
  9. L29
    specialize signed_decode_normal x2
  10. L30
    apply signed_decode_normal
07Use earlier factsL31–36

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

  1. L31
    exact hfirst_witness_witness_witness_left
  2. L32
    specialize signed_decode_normal x3
  3. L33
    specialize signed_decode_normal x4
  4. L34
    specialize signed_decode_normal x5
  5. L35
    apply signed_decode_normal
  6. L36
    exact hsecond_witness_witness_witness_left
08Separate the logical casesL37–37

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

  1. L37
    cases hnorm
09Construct an explicit witnessL38–38

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

  1. L38
    exists x6
10Use earlier factsL39–48

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

  1. L39
    specialize eisenstein_coordinate_norm_transport x1
  2. L40
    specialize eisenstein_coordinate_norm_transport x2
  3. L41
    specialize eisenstein_coordinate_norm_transport x4
  4. L42
    specialize eisenstein_coordinate_norm_transport x5
  5. L43
    specialize eisenstein_coordinate_norm_transport ap
  6. L44
    specialize eisenstein_coordinate_norm_transport an
  7. L45
    specialize eisenstein_coordinate_norm_transport bp
  8. L46
    specialize eisenstein_coordinate_norm_transport bn
  9. L47
    specialize eisenstein_coordinate_norm_transport x6
  10. L48
    apply eisenstein_coordinate_norm_transport
11Calculate and transport equalitiesL49–49

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L49
    trans an + x1
12Use earlier factsL50–50

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

  1. L50
    apply add_comm
13Calculate and transport equalitiesL51–51

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L51
    symm
14Use earlier factsL52–52

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

  1. L52
    exact hfirst_witness_witness_witness_right
15Calculate and transport equalitiesL53–53

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L53
    trans bn + x4
16Use earlier factsL54–54

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

  1. L54
    apply add_comm
17Calculate and transport equalitiesL55–55

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L55
    symm
18Use earlier factsL56–57

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

  1. L56
    exact hsecond_witness_witness_witness_right
  2. L57
    exact hnorm_witness

Library-wide reading audit

Original exact command ledger · 57 lines
  1. 0001intro ap
  2. 0002intro an
  3. 0003intro bp
  4. 0004intro bn
  5. 0005have hfirst : exists code. (exists sb_pos_ee_first sb_neg_ee_first. (((code = 2 * sb_pos_ee_first /\ sb_neg_ee_first = 0) \/ exists sd_half_ee_first. ((code = 2 * sd_half_ee_first + 1 /\ sb_pos_ee_first = 0) /\ sb_neg_ee_first = S sd_half_ee_first)) /\ ap + sb_neg_ee_first = an + sb_pos_ee_first))
  6. 0006specialize signed_balance_total ap
  7. 0007specialize signed_balance_total an
  8. 0008apply signed_balance_total
  9. 0009cases hfirst
  10. 0010cases hfirst_witness
  11. 0011cases hfirst_witness_witness
  12. 0012cases hfirst_witness_witness_witness
  13. 0013have hsecond : exists code. (exists sb_pos_ee_second sb_neg_ee_second. (((code = 2 * sb_pos_ee_second /\ sb_neg_ee_second = 0) \/ exists sd_half_ee_second. ((code = 2 * sd_half_ee_second + 1 /\ sb_pos_ee_second = 0) /\ sb_neg_ee_second = S sd_half_ee_second)) /\ bp + sb_neg_ee_second = bn + sb_pos_ee_second))
  14. 0014specialize signed_balance_total bp
  15. 0015specialize signed_balance_total bn
  16. 0016apply signed_balance_total
  17. 0017cases hsecond
  18. 0018cases hsecond_witness
  19. 0019cases hsecond_witness_witness
  20. 0020cases hsecond_witness_witness_witness
  21. 0021have hnorm : exists n. ((((((((x1) * (x1))) + (((x2) * (x2))))) + (((((x4) * (x4))) + (((x5) * (x5))))))) + (((((x1) * (x5))) + (((x2) * (x4)))))) = ((((((((((x1) * (x2))) + (((x2) * (x1))))) + (((((x4) * (x5))) + (((x5) * (x4))))))) + (((((x1) * (x4))) + (((x2) * (x5))))))) + (n))
  22. 0022specialize eisenstein_normal_coordinate_norm_exists x1
  23. 0023specialize eisenstein_normal_coordinate_norm_exists x2
  24. 0024specialize eisenstein_normal_coordinate_norm_exists x4
  25. 0025specialize eisenstein_normal_coordinate_norm_exists x5
  26. 0026apply eisenstein_normal_coordinate_norm_exists
  27. 0027specialize signed_decode_normal x
  28. 0028specialize signed_decode_normal x1
  29. 0029specialize signed_decode_normal x2
  30. 0030apply signed_decode_normal
  31. 0031exact hfirst_witness_witness_witness_left
  32. 0032specialize signed_decode_normal x3
  33. 0033specialize signed_decode_normal x4
  34. 0034specialize signed_decode_normal x5
  35. 0035apply signed_decode_normal
  36. 0036exact hsecond_witness_witness_witness_left
  37. 0037cases hnorm
  38. 0038exists x6
  39. 0039specialize eisenstein_coordinate_norm_transport x1
  40. 0040specialize eisenstein_coordinate_norm_transport x2
  41. 0041specialize eisenstein_coordinate_norm_transport x4
  42. 0042specialize eisenstein_coordinate_norm_transport x5
  43. 0043specialize eisenstein_coordinate_norm_transport ap
  44. 0044specialize eisenstein_coordinate_norm_transport an
  45. 0045specialize eisenstein_coordinate_norm_transport bp
  46. 0046specialize eisenstein_coordinate_norm_transport bn
  47. 0047specialize eisenstein_coordinate_norm_transport x6
  48. 0048apply eisenstein_coordinate_norm_transport
  49. 0049trans an + x1
  50. 0050apply add_comm
  51. 0051symm
  52. 0052exact hfirst_witness_witness_witness_right
  53. 0053trans bn + x4
  54. 0054apply add_comm
  55. 0055symm
  56. 0056exact hsecond_witness_witness_witness_right
  57. 0057exact hnorm_witness