EI0012

eisenstein_norm_to_weighted_norm

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

The exact linear embedding (a,b)↦(2a-b,b) has actual weight-three norm four times the Eisenstein norm.

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 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))) -> (exists ee_real_square_image ee_imag_square_image. (((((((((2) * (ap))) + (bn))) * (((((2) * (ap))) + (bn))))) + (((((((2) * (an))) + (bp))) * (((((2) * (an))) + (bp)))))) = ((ee_real_square_image) + (((((((((2) * (ap))) + (bn))) * (((((2) * (an))) + (bp))))) + (((((((2) * (an))) + (bp))) * (((((2) * (ap))) + (bn))))))))) /\ ((((((bp) * (bp))) + (((bn) * (bn)))) = ((ee_imag_square_image) + (((((bp) * (bn))) + (((bn) * (bp))))))) /\ (4 * N) = ee_real_square_image + 3 * ee_imag_square_image))

Constructive proof overview

Generated structural guide

The exact linear embedding (a,b)↦(2a-b,b) has actual weight-three norm four times the Eisenstein norm.

The unchanged tactic script uses 2 declared prerequisites and contains 41 exact native proof lines.

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

Proof neighborhood

Direct dependencies

gaussian_signed_square_exists Alpha theorem; checked-use authorized EI000F eisenstein_norm_weighted_square_identity

Direct dependents

EI0030 eisenstein_coordinate_norm_zero

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

41 script commands · 15 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 (1)
eisenstein norm weighted square identity
01Fix variables and assumptionsL1–6

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 N
  6. L6
    intro hnorm
02Establish haL7–10

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

  1. L7
    have ha : exists sa. ((((ap) * (ap))) + (((an) * (an)))) = ((sa) + (((((ap) * (an))) + (((an) * (ap))))))
  2. L8
    specialize gaussian_signed_square_exists ap
  3. L9
    specialize gaussian_signed_square_exists an
  4. L10
    apply gaussian_signed_square_exists
03Separate the logical casesL11–11

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

  1. L11
    cases ha
04Establish hbL12–15

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

  1. L12
    have hb : exists sb. ((((bp) * (bp))) + (((bn) * (bn)))) = ((sb) + (((((bp) * (bn))) + (((bn) * (bp))))))
  2. L13
    specialize gaussian_signed_square_exists bp
  3. L14
    specialize gaussian_signed_square_exists bn
  4. L15
    apply gaussian_signed_square_exists
05Separate the logical casesL16–16

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

  1. L16
    cases hb
06Establish htL17–20

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

  1. L17
    have ht : exists sh. ((((((((2) * (ap))) + (bn))) * (((((2) * (ap))) + (bn))))) + (((((((2) * (an))) + (bp))) * (((((2) * (an))) + (bp)))))) = ((sh) + (((((((((2) * (ap))) + (bn))) * (((((2) * (an))) + (bp))))) + (((((((2) * (an))) + (bp))) * (((((2) * (ap))) + (bn))))))))
  2. L18
    specialize gaussian_signed_square_exists ((((2) * (ap))) + (bn))
  3. L19
    specialize gaussian_signed_square_exists ((((2) * (an))) + (bp))
  4. L20
    apply gaussian_signed_square_exists
07Separate the logical casesL21–21

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

  1. L21
    cases ht
08Construct an explicit witnessL22–23

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

  1. L22
    exists x2
  2. L23
    exists x1
09Separate the logical casesL24–24

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

  1. L24
    split
10Use earlier factsL25–25

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

  1. L25
    exact ht_witness
11Separate the logical casesL26–26

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

  1. L26
    split
12Use earlier factsL27–27

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

  1. L27
    exact hb_witness
13Calculate and transport equalitiesL28–28

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

  1. L28
    symm
14Use earlier factsL29–38

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

  1. L29
    specialize eisenstein_norm_weighted_square_identity ap
  2. L30
    specialize eisenstein_norm_weighted_square_identity an
  3. L31
    specialize eisenstein_norm_weighted_square_identity bp
  4. L32
    specialize eisenstein_norm_weighted_square_identity bn
  5. L33
    specialize eisenstein_norm_weighted_square_identity x
  6. L34
    specialize eisenstein_norm_weighted_square_identity x1
  7. L35
    specialize eisenstein_norm_weighted_square_identity x2
  8. L36
    specialize eisenstein_norm_weighted_square_identity N
  9. L37
    apply eisenstein_norm_weighted_square_identity
  10. L38
    exact ha_witness
15Use earlier factsL39–41

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

  1. L39
    exact hb_witness
  2. L40
    exact ht_witness
  3. L41
    exact hnorm

Library-wide reading audit

Original exact command ledger · 41 lines
  1. 0001intro ap
  2. 0002intro an
  3. 0003intro bp
  4. 0004intro bn
  5. 0005intro N
  6. 0006intro hnorm
  7. 0007have ha : exists sa. ((((ap) * (ap))) + (((an) * (an)))) = ((sa) + (((((ap) * (an))) + (((an) * (ap))))))
  8. 0008specialize gaussian_signed_square_exists ap
  9. 0009specialize gaussian_signed_square_exists an
  10. 0010apply gaussian_signed_square_exists
  11. 0011cases ha
  12. 0012have hb : exists sb. ((((bp) * (bp))) + (((bn) * (bn)))) = ((sb) + (((((bp) * (bn))) + (((bn) * (bp))))))
  13. 0013specialize gaussian_signed_square_exists bp
  14. 0014specialize gaussian_signed_square_exists bn
  15. 0015apply gaussian_signed_square_exists
  16. 0016cases hb
  17. 0017have ht : exists sh. ((((((((2) * (ap))) + (bn))) * (((((2) * (ap))) + (bn))))) + (((((((2) * (an))) + (bp))) * (((((2) * (an))) + (bp)))))) = ((sh) + (((((((((2) * (ap))) + (bn))) * (((((2) * (an))) + (bp))))) + (((((((2) * (an))) + (bp))) * (((((2) * (ap))) + (bn))))))))
  18. 0018specialize gaussian_signed_square_exists ((((2) * (ap))) + (bn))
  19. 0019specialize gaussian_signed_square_exists ((((2) * (an))) + (bp))
  20. 0020apply gaussian_signed_square_exists
  21. 0021cases ht
  22. 0022exists x2
  23. 0023exists x1
  24. 0024split
  25. 0025exact ht_witness
  26. 0026split
  27. 0027exact hb_witness
  28. 0028symm
  29. 0029specialize eisenstein_norm_weighted_square_identity ap
  30. 0030specialize eisenstein_norm_weighted_square_identity an
  31. 0031specialize eisenstein_norm_weighted_square_identity bp
  32. 0032specialize eisenstein_norm_weighted_square_identity bn
  33. 0033specialize eisenstein_norm_weighted_square_identity x
  34. 0034specialize eisenstein_norm_weighted_square_identity x1
  35. 0035specialize eisenstein_norm_weighted_square_identity x2
  36. 0036specialize eisenstein_norm_weighted_square_identity N
  37. 0037apply eisenstein_norm_weighted_square_identity
  38. 0038exact ha_witness
  39. 0039exact hb_witness
  40. 0040exact ht_witness
  41. 0041exact hnorm