EI0012

eisenstein_norm_to_weighted_norm

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

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

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.

A floor quotient in the fundamental parallelogram already gives the required strict norm decrease; global nearest-point optimality is not asserted. The shared carrier is identical to the Gaussian carrier, but the multiplication law and norm are different. Eisenstein gcd, factorization, and prime classification remain separate targets.

Exact theorem in conservative defined notation

∀ ap. ∀ an. ∀ bp. ∀ bn. ∀ N. EisensteinCoordinateNorm(ap,an,bp,bn,N) → WeightedSignedNormThree(2 · ap + bn,2 · an + bp,bp,bn,4 · N)

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

Definition DAG

SignedDifferenceSquare(p,n,s) · 3EisensteinCoordinateNorm(ap,an,bp,bn,n) · 1WeightedSignedNormThree(ap,an,bp,bn,n) · 1

Actual proof prerequisites

gaussian_signed_square_exists · checked external prerequisiteeisenstein_norm_weighted_square_identity
Original expanded first-order 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))

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ∃ sa. SignedDifferenceSquare(ap,an,sa)Definitions: SignedDifferenceSquare(ap,an,sa)Original native command in the exact edition
  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 : ∃ sb. SignedDifferenceSquare(bp,bn,sb)Definitions: SignedDifferenceSquare(bp,bn,sb)Original native command in the exact edition
  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 : ∃ sh. SignedDifferenceSquare(2 · ap + bn,2 · an + bp,sh)Definitions: SignedDifferenceSquare(2 · ap + bn,2 · an + bp,sh)Original native command in the exact edition
  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 defined 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 : ∃ sa. SignedDifferenceSquare(ap,an,sa)
  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 : ∃ sb. SignedDifferenceSquare(bp,bn,sb)
  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 : ∃ sh. SignedDifferenceSquare(2 · ap + bn,2 · an + bp,sh)
  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