EI000F

eisenstein_norm_weighted_square_identity

The actual signed square identity 4ENorm(a,b)=(2a-b)²+3b² holds for every signed representative.

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. ∀ sa. ∀ sb. ∀ sh. ∀ N. SignedDifferenceSquare(ap,an,sa) → SignedDifferenceSquare(bp,bn,sb) → SignedDifferenceSquare(2 · ap + bn,2 · an + bp,sh) → EisensteinCoordinateNorm(ap,an,bp,bn,N) → sh + 3 · sb = 4 · N

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

Definition DAG

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

Actual proof prerequisites

gaussian_signed_square_scaled · checked external prerequisitegaussian_signed_square_difference_compensation · checked external prerequisiteeisenstein_norm_square_balanceeisenstein_weighted_embedding_compensationmul_assoc · checked external prerequisitemul_add · checked external prerequisite
Original expanded first-order statement 
forall ap an bp bn sa sb sh N. (((((ap) * (ap))) + (((an) * (an)))) = ((sa) + (((((ap) * (an))) + (((an) * (ap))))))) -> (((((bp) * (bp))) + (((bn) * (bn)))) = ((sb) + (((((bp) * (bn))) + (((bn) * (bp))))))) -> (((((((((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))))))))) -> (((((((((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))) -> sh + 3 * sb = 4 * N

Complete tactic proof in conservative notation

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

58 script commands · 9 reading checkpoints · 4 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 (2)
eisenstein weighted embedding compensationeisenstein norm square balance
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 sa
  6. L6
    intro sb
  7. L7
    intro sh
  8. L8
    intro N
  9. L9
    intro ha
  10. L10
    intro hb
02Fix variables and assumptionsL11–12

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

  1. L11
    intro htransformed
  2. L12
    intro hnorm
03Establish hdoubleL13–19

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

  1. L13
    have hdouble : SignedDifferenceSquare(2 · ap,2 · an,2 · 2 · sa)Definitions: SignedDifferenceSquare(2 · ap,2 · an,2 · 2 · sa)Original native command in the exact edition
  2. L14
    specialize gaussian_signed_square_scaled ap
  3. L15
    specialize gaussian_signed_square_scaled an
  4. L16
    specialize gaussian_signed_square_scaled sa
  5. L17
    specialize gaussian_signed_square_scaled 2
  6. L18
    apply gaussian_signed_square_scaled
  7. L19
    exact ha
04Establish hdifferenceL20–29

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

  1. L20
    have hdifference : sh + (((((((((2) * (ap))) * (bp))) + (((((2) * (an))) * (bn))))) + (((((((2) * (ap))) * (bp))) + (((((2) * (an))) * (bn))))))) = ((2 * 2) * sa + sb) + (((((((((2) * (ap))) * (bn))) + (((((2) * (an))) * (bp))))) + (((((((2) * (ap))) * (bn))) + (((((2) * (an))) * (bp)))))))
  2. L21
    specialize gaussian_signed_square_difference_compensation ((2) * (ap))
  3. L22
    specialize gaussian_signed_square_difference_compensation ((2) * (an))
  4. L23
    specialize gaussian_signed_square_difference_compensation bp
  5. L24
    specialize gaussian_signed_square_difference_compensation bn
  6. L25
    specialize gaussian_signed_square_difference_compensation ((2 * 2) * sa)
  7. L26
    specialize gaussian_signed_square_difference_compensation sb
  8. L27
    specialize gaussian_signed_square_difference_compensation sh
  9. L28
    apply gaussian_signed_square_difference_compensation
  10. L29
    exact hdouble
05Use earlier factsL30–31

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

  1. L30
    exact hb
  2. L31
    exact htransformed
06Establish hpL32–33

Establish this local claim before using it. It is not an additional assumption.

  1. L32
    have hp : ((((((2) * (ap))) * (bp))) + (((((2) * (an))) * (bn)))) = 2 * (((((ap) * (bp))) + (((an) * (bn)))))
  2. L33
    simp [mul_assoc, mul_add]
07Establish hnL34–43

Establish this local claim before using it. It is not an additional assumption.

  1. L34
    have hn : ((((((2) * (ap))) * (bn))) + (((((2) * (an))) * (bp)))) = 2 * (((((ap) * (bn))) + (((an) * (bp)))))
  2. L35
    simp [mul_assoc, mul_add]
  3. L36
    rewrite hp at hdifference
  4. L37
    rewrite hp at hdifference
  5. L38
    rewrite hn at hdifference
  6. L39
    rewrite hn at hdifference
  7. L40
    specialize eisenstein_weighted_embedding_compensation sa
  8. L41
    specialize eisenstein_weighted_embedding_compensation sb
  9. L42
    specialize eisenstein_weighted_embedding_compensation ((((ap) * (bp))) + (((an) * (bn))))
  10. L43
    specialize eisenstein_weighted_embedding_compensation ((((ap) * (bn))) + (((an) * (bp))))
08Use earlier factsL44–53

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

  1. L44
    specialize eisenstein_weighted_embedding_compensation sh
  2. L45
    specialize eisenstein_weighted_embedding_compensation N
  3. L46
    apply eisenstein_weighted_embedding_compensation
  4. L47
    specialize eisenstein_norm_square_balance ap
  5. L48
    specialize eisenstein_norm_square_balance an
  6. L49
    specialize eisenstein_norm_square_balance bp
  7. L50
    specialize eisenstein_norm_square_balance bn
  8. L51
    specialize eisenstein_norm_square_balance sa
  9. L52
    specialize eisenstein_norm_square_balance sb
  10. L53
    specialize eisenstein_norm_square_balance N
09Use earlier factsL54–58

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

  1. L54
    apply eisenstein_norm_square_balance
  2. L55
    exact ha
  3. L56
    exact hb
  4. L57
    exact hnorm
  5. L58
    exact hdifference

Library-wide reading audit

Original defined command ledger · 58 lines
  1. 0001intro ap
  2. 0002intro an
  3. 0003intro bp
  4. 0004intro bn
  5. 0005intro sa
  6. 0006intro sb
  7. 0007intro sh
  8. 0008intro N
  9. 0009intro ha
  10. 0010intro hb
  11. 0011intro htransformed
  12. 0012intro hnorm
  13. 0013have hdouble : SignedDifferenceSquare(2 · ap,2 · an,2 · 2 · sa)
  14. 0014specialize gaussian_signed_square_scaled ap
  15. 0015specialize gaussian_signed_square_scaled an
  16. 0016specialize gaussian_signed_square_scaled sa
  17. 0017specialize gaussian_signed_square_scaled 2
  18. 0018apply gaussian_signed_square_scaled
  19. 0019exact ha
  20. 0020have hdifference : sh + (((((((((2) * (ap))) * (bp))) + (((((2) * (an))) * (bn))))) + (((((((2) * (ap))) * (bp))) + (((((2) * (an))) * (bn))))))) = ((2 * 2) * sa + sb) + (((((((((2) * (ap))) * (bn))) + (((((2) * (an))) * (bp))))) + (((((((2) * (ap))) * (bn))) + (((((2) * (an))) * (bp)))))))
  21. 0021specialize gaussian_signed_square_difference_compensation ((2) * (ap))
  22. 0022specialize gaussian_signed_square_difference_compensation ((2) * (an))
  23. 0023specialize gaussian_signed_square_difference_compensation bp
  24. 0024specialize gaussian_signed_square_difference_compensation bn
  25. 0025specialize gaussian_signed_square_difference_compensation ((2 * 2) * sa)
  26. 0026specialize gaussian_signed_square_difference_compensation sb
  27. 0027specialize gaussian_signed_square_difference_compensation sh
  28. 0028apply gaussian_signed_square_difference_compensation
  29. 0029exact hdouble
  30. 0030exact hb
  31. 0031exact htransformed
  32. 0032have hp : ((((((2) * (ap))) * (bp))) + (((((2) * (an))) * (bn)))) = 2 * (((((ap) * (bp))) + (((an) * (bn)))))
  33. 0033simp [mul_assoc, mul_add]
  34. 0034have hn : ((((((2) * (ap))) * (bn))) + (((((2) * (an))) * (bp)))) = 2 * (((((ap) * (bn))) + (((an) * (bp)))))
  35. 0035simp [mul_assoc, mul_add]
  36. 0036rewrite hp at hdifference
  37. 0037rewrite hp at hdifference
  38. 0038rewrite hn at hdifference
  39. 0039rewrite hn at hdifference
  40. 0040specialize eisenstein_weighted_embedding_compensation sa
  41. 0041specialize eisenstein_weighted_embedding_compensation sb
  42. 0042specialize eisenstein_weighted_embedding_compensation ((((ap) * (bp))) + (((an) * (bn))))
  43. 0043specialize eisenstein_weighted_embedding_compensation ((((ap) * (bn))) + (((an) * (bp))))
  44. 0044specialize eisenstein_weighted_embedding_compensation sh
  45. 0045specialize eisenstein_weighted_embedding_compensation N
  46. 0046apply eisenstein_weighted_embedding_compensation
  47. 0047specialize eisenstein_norm_square_balance ap
  48. 0048specialize eisenstein_norm_square_balance an
  49. 0049specialize eisenstein_norm_square_balance bp
  50. 0050specialize eisenstein_norm_square_balance bn
  51. 0051specialize eisenstein_norm_square_balance sa
  52. 0052specialize eisenstein_norm_square_balance sb
  53. 0053specialize eisenstein_norm_square_balance N
  54. 0054apply eisenstein_norm_square_balance
  55. 0055exact ha
  56. 0056exact hb
  57. 0057exact hnorm
  58. 0058exact hdifference