EI003C

eisenstein_multiply_for_representations

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

Every witness of canonical Eisenstein multiplication represents the same actual product of any chosen integer representatives.

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 ac bc cc a b c d e f g h. (exists ge_representation_real_code_multiply_fixed_first ge_representation_imaginary_code_multiply_fixed_first. (((ac) = ((ge_representation_real_code_multiply_fixed_first) + (ge_representation_imaginary_code_multiply_fixed_first)) * S ((ge_representation_real_code_multiply_fixed_first) + (ge_representation_imaginary_code_multiply_fixed_first)) + ((ge_representation_imaginary_code_multiply_fixed_first) + (ge_representation_imaginary_code_multiply_fixed_first))) /\ ((exists ge_balance_positive_multiply_fixed_firstreal ge_balance_negative_multiply_fixed_firstreal. (((((ge_representation_real_code_multiply_fixed_first) = 2 * (ge_balance_positive_multiply_fixed_firstreal) /\ (ge_balance_negative_multiply_fixed_firstreal) = 0) \/ exists ge_signed_half_multiply_fixed_firstrealdecode. (((ge_representation_real_code_multiply_fixed_first) = 2 * ge_signed_half_multiply_fixed_firstrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_firstreal) = 0) /\ (ge_balance_negative_multiply_fixed_firstreal) = S ge_signed_half_multiply_fixed_firstrealdecode))) /\ ((a) + ge_balance_negative_multiply_fixed_firstreal = (b) + ge_balance_positive_multiply_fixed_firstreal))) /\ (exists ge_balance_positive_multiply_fixed_firstimaginary ge_balance_negative_multiply_fixed_firstimaginary. (((((ge_representation_imaginary_code_multiply_fixed_first) = 2 * (ge_balance_positive_multiply_fixed_firstimaginary) /\ (ge_balance_negative_multiply_fixed_firstimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_firstimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_first) = 2 * ge_signed_half_multiply_fixed_firstimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_firstimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_firstimaginary) = S ge_signed_half_multiply_fixed_firstimaginarydecode))) /\ ((c) + ge_balance_negative_multiply_fixed_firstimaginary = (d) + ge_balance_positive_multiply_fixed_firstimaginary)))))) -> (exists ge_representation_real_code_multiply_fixed_second ge_representation_imaginary_code_multiply_fixed_second. (((bc) = ((ge_representation_real_code_multiply_fixed_second) + (ge_representation_imaginary_code_multiply_fixed_second)) * S ((ge_representation_real_code_multiply_fixed_second) + (ge_representation_imaginary_code_multiply_fixed_second)) + ((ge_representation_imaginary_code_multiply_fixed_second) + (ge_representation_imaginary_code_multiply_fixed_second))) /\ ((exists ge_balance_positive_multiply_fixed_secondreal ge_balance_negative_multiply_fixed_secondreal. (((((ge_representation_real_code_multiply_fixed_second) = 2 * (ge_balance_positive_multiply_fixed_secondreal) /\ (ge_balance_negative_multiply_fixed_secondreal) = 0) \/ exists ge_signed_half_multiply_fixed_secondrealdecode. (((ge_representation_real_code_multiply_fixed_second) = 2 * ge_signed_half_multiply_fixed_secondrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_secondreal) = 0) /\ (ge_balance_negative_multiply_fixed_secondreal) = S ge_signed_half_multiply_fixed_secondrealdecode))) /\ ((e) + ge_balance_negative_multiply_fixed_secondreal = (f) + ge_balance_positive_multiply_fixed_secondreal))) /\ (exists ge_balance_positive_multiply_fixed_secondimaginary ge_balance_negative_multiply_fixed_secondimaginary. (((((ge_representation_imaginary_code_multiply_fixed_second) = 2 * (ge_balance_positive_multiply_fixed_secondimaginary) /\ (ge_balance_negative_multiply_fixed_secondimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_secondimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_second) = 2 * ge_signed_half_multiply_fixed_secondimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_secondimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_secondimaginary) = S ge_signed_half_multiply_fixed_secondimaginarydecode))) /\ ((g) + ge_balance_negative_multiply_fixed_secondimaginary = (h) + ge_balance_positive_multiply_fixed_secondimaginary)))))) -> (exists ee_first_rp_multiply_fixed_graph ee_first_rn_multiply_fixed_graph ee_first_ip_multiply_fixed_graph ee_first_in_multiply_fixed_graph ee_second_rp_multiply_fixed_graph ee_second_rn_multiply_fixed_graph ee_second_ip_multiply_fixed_graph ee_second_in_multiply_fixed_graph. ((exists ge_representation_real_code_multiply_fixed_graphfirst ge_representation_imaginary_code_multiply_fixed_graphfirst. (((ac) = ((ge_representation_real_code_multiply_fixed_graphfirst) + (ge_representation_imaginary_code_multiply_fixed_graphfirst)) * S ((ge_representation_real_code_multiply_fixed_graphfirst) + (ge_representation_imaginary_code_multiply_fixed_graphfirst)) + ((ge_representation_imaginary_code_multiply_fixed_graphfirst) + (ge_representation_imaginary_code_multiply_fixed_graphfirst))) /\ ((exists ge_balance_positive_multiply_fixed_graphfirstreal ge_balance_negative_multiply_fixed_graphfirstreal. (((((ge_representation_real_code_multiply_fixed_graphfirst) = 2 * (ge_balance_positive_multiply_fixed_graphfirstreal) /\ (ge_balance_negative_multiply_fixed_graphfirstreal) = 0) \/ exists ge_signed_half_multiply_fixed_graphfirstrealdecode. (((ge_representation_real_code_multiply_fixed_graphfirst) = 2 * ge_signed_half_multiply_fixed_graphfirstrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_graphfirstreal) = 0) /\ (ge_balance_negative_multiply_fixed_graphfirstreal) = S ge_signed_half_multiply_fixed_graphfirstrealdecode))) /\ ((ee_first_rp_multiply_fixed_graph) + ge_balance_negative_multiply_fixed_graphfirstreal = (ee_first_rn_multiply_fixed_graph) + ge_balance_positive_multiply_fixed_graphfirstreal))) /\ (exists ge_balance_positive_multiply_fixed_graphfirstimaginary ge_balance_negative_multiply_fixed_graphfirstimaginary. (((((ge_representation_imaginary_code_multiply_fixed_graphfirst) = 2 * (ge_balance_positive_multiply_fixed_graphfirstimaginary) /\ (ge_balance_negative_multiply_fixed_graphfirstimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_graphfirstimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_graphfirst) = 2 * ge_signed_half_multiply_fixed_graphfirstimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_graphfirstimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_graphfirstimaginary) = S ge_signed_half_multiply_fixed_graphfirstimaginarydecode))) /\ ((ee_first_ip_multiply_fixed_graph) + ge_balance_negative_multiply_fixed_graphfirstimaginary = (ee_first_in_multiply_fixed_graph) + ge_balance_positive_multiply_fixed_graphfirstimaginary)))))) /\ ((exists ge_representation_real_code_multiply_fixed_graphsecond ge_representation_imaginary_code_multiply_fixed_graphsecond. (((bc) = ((ge_representation_real_code_multiply_fixed_graphsecond) + (ge_representation_imaginary_code_multiply_fixed_graphsecond)) * S ((ge_representation_real_code_multiply_fixed_graphsecond) + (ge_representation_imaginary_code_multiply_fixed_graphsecond)) + ((ge_representation_imaginary_code_multiply_fixed_graphsecond) + (ge_representation_imaginary_code_multiply_fixed_graphsecond))) /\ ((exists ge_balance_positive_multiply_fixed_graphsecondreal ge_balance_negative_multiply_fixed_graphsecondreal. (((((ge_representation_real_code_multiply_fixed_graphsecond) = 2 * (ge_balance_positive_multiply_fixed_graphsecondreal) /\ (ge_balance_negative_multiply_fixed_graphsecondreal) = 0) \/ exists ge_signed_half_multiply_fixed_graphsecondrealdecode. (((ge_representation_real_code_multiply_fixed_graphsecond) = 2 * ge_signed_half_multiply_fixed_graphsecondrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_graphsecondreal) = 0) /\ (ge_balance_negative_multiply_fixed_graphsecondreal) = S ge_signed_half_multiply_fixed_graphsecondrealdecode))) /\ ((ee_second_rp_multiply_fixed_graph) + ge_balance_negative_multiply_fixed_graphsecondreal = (ee_second_rn_multiply_fixed_graph) + ge_balance_positive_multiply_fixed_graphsecondreal))) /\ (exists ge_balance_positive_multiply_fixed_graphsecondimaginary ge_balance_negative_multiply_fixed_graphsecondimaginary. (((((ge_representation_imaginary_code_multiply_fixed_graphsecond) = 2 * (ge_balance_positive_multiply_fixed_graphsecondimaginary) /\ (ge_balance_negative_multiply_fixed_graphsecondimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_graphsecondimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_graphsecond) = 2 * ge_signed_half_multiply_fixed_graphsecondimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_graphsecondimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_graphsecondimaginary) = S ge_signed_half_multiply_fixed_graphsecondimaginarydecode))) /\ ((ee_second_ip_multiply_fixed_graph) + ge_balance_negative_multiply_fixed_graphsecondimaginary = (ee_second_in_multiply_fixed_graph) + ge_balance_positive_multiply_fixed_graphsecondimaginary)))))) /\ (exists ge_representation_real_code_multiply_fixed_graphoutput ge_representation_imaginary_code_multiply_fixed_graphoutput. (((cc) = ((ge_representation_real_code_multiply_fixed_graphoutput) + (ge_representation_imaginary_code_multiply_fixed_graphoutput)) * S ((ge_representation_real_code_multiply_fixed_graphoutput) + (ge_representation_imaginary_code_multiply_fixed_graphoutput)) + ((ge_representation_imaginary_code_multiply_fixed_graphoutput) + (ge_representation_imaginary_code_multiply_fixed_graphoutput))) /\ ((exists ge_balance_positive_multiply_fixed_graphoutputreal ge_balance_negative_multiply_fixed_graphoutputreal. (((((ge_representation_real_code_multiply_fixed_graphoutput) = 2 * (ge_balance_positive_multiply_fixed_graphoutputreal) /\ (ge_balance_negative_multiply_fixed_graphoutputreal) = 0) \/ exists ge_signed_half_multiply_fixed_graphoutputrealdecode. (((ge_representation_real_code_multiply_fixed_graphoutput) = 2 * ge_signed_half_multiply_fixed_graphoutputrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_graphoutputreal) = 0) /\ (ge_balance_negative_multiply_fixed_graphoutputreal) = S ge_signed_half_multiply_fixed_graphoutputrealdecode))) /\ ((((((((ee_first_rp_multiply_fixed_graph) * (ee_second_rp_multiply_fixed_graph))) + (((ee_first_rn_multiply_fixed_graph) * (ee_second_rn_multiply_fixed_graph))))) + (((((ee_first_ip_multiply_fixed_graph) * (ee_second_in_multiply_fixed_graph))) + (((ee_first_in_multiply_fixed_graph) * (ee_second_ip_multiply_fixed_graph))))))) + ge_balance_negative_multiply_fixed_graphoutputreal = (((((((ee_first_rp_multiply_fixed_graph) * (ee_second_rn_multiply_fixed_graph))) + (((ee_first_rn_multiply_fixed_graph) * (ee_second_rp_multiply_fixed_graph))))) + (((((ee_first_ip_multiply_fixed_graph) * (ee_second_ip_multiply_fixed_graph))) + (((ee_first_in_multiply_fixed_graph) * (ee_second_in_multiply_fixed_graph))))))) + ge_balance_positive_multiply_fixed_graphoutputreal))) /\ (exists ge_balance_positive_multiply_fixed_graphoutputimaginary ge_balance_negative_multiply_fixed_graphoutputimaginary. (((((ge_representation_imaginary_code_multiply_fixed_graphoutput) = 2 * (ge_balance_positive_multiply_fixed_graphoutputimaginary) /\ (ge_balance_negative_multiply_fixed_graphoutputimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_graphoutputimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_graphoutput) = 2 * ge_signed_half_multiply_fixed_graphoutputimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_graphoutputimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_graphoutputimaginary) = S ge_signed_half_multiply_fixed_graphoutputimaginarydecode))) /\ ((((((((((ee_first_rp_multiply_fixed_graph) * (ee_second_ip_multiply_fixed_graph))) + (((ee_first_rn_multiply_fixed_graph) * (ee_second_in_multiply_fixed_graph))))) + (((((ee_first_ip_multiply_fixed_graph) * (ee_second_rp_multiply_fixed_graph))) + (((ee_first_in_multiply_fixed_graph) * (ee_second_rn_multiply_fixed_graph))))))) + (((((ee_first_ip_multiply_fixed_graph) * (ee_second_in_multiply_fixed_graph))) + (((ee_first_in_multiply_fixed_graph) * (ee_second_ip_multiply_fixed_graph))))))) + ge_balance_negative_multiply_fixed_graphoutputimaginary = (((((((((ee_first_rp_multiply_fixed_graph) * (ee_second_in_multiply_fixed_graph))) + (((ee_first_rn_multiply_fixed_graph) * (ee_second_ip_multiply_fixed_graph))))) + (((((ee_first_ip_multiply_fixed_graph) * (ee_second_rn_multiply_fixed_graph))) + (((ee_first_in_multiply_fixed_graph) * (ee_second_rp_multiply_fixed_graph))))))) + (((((ee_first_ip_multiply_fixed_graph) * (ee_second_ip_multiply_fixed_graph))) + (((ee_first_in_multiply_fixed_graph) * (ee_second_in_multiply_fixed_graph))))))) + ge_balance_positive_multiply_fixed_graphoutputimaginary))))))))) -> (exists ge_representation_real_code_multiply_fixed_output ge_representation_imaginary_code_multiply_fixed_output. (((cc) = ((ge_representation_real_code_multiply_fixed_output) + (ge_representation_imaginary_code_multiply_fixed_output)) * S ((ge_representation_real_code_multiply_fixed_output) + (ge_representation_imaginary_code_multiply_fixed_output)) + ((ge_representation_imaginary_code_multiply_fixed_output) + (ge_representation_imaginary_code_multiply_fixed_output))) /\ ((exists ge_balance_positive_multiply_fixed_outputreal ge_balance_negative_multiply_fixed_outputreal. (((((ge_representation_real_code_multiply_fixed_output) = 2 * (ge_balance_positive_multiply_fixed_outputreal) /\ (ge_balance_negative_multiply_fixed_outputreal) = 0) \/ exists ge_signed_half_multiply_fixed_outputrealdecode. (((ge_representation_real_code_multiply_fixed_output) = 2 * ge_signed_half_multiply_fixed_outputrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_outputreal) = 0) /\ (ge_balance_negative_multiply_fixed_outputreal) = S ge_signed_half_multiply_fixed_outputrealdecode))) /\ ((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + ge_balance_negative_multiply_fixed_outputreal = (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + ge_balance_positive_multiply_fixed_outputreal))) /\ (exists ge_balance_positive_multiply_fixed_outputimaginary ge_balance_negative_multiply_fixed_outputimaginary. (((((ge_representation_imaginary_code_multiply_fixed_output) = 2 * (ge_balance_positive_multiply_fixed_outputimaginary) /\ (ge_balance_negative_multiply_fixed_outputimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_outputimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_output) = 2 * ge_signed_half_multiply_fixed_outputimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_outputimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_outputimaginary) = S ge_signed_half_multiply_fixed_outputimaginarydecode))) /\ ((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) + ge_balance_negative_multiply_fixed_outputimaginary = (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) + ge_balance_positive_multiply_fixed_outputimaginary))))))

Constructive proof overview

Generated structural guide

Every witness of canonical Eisenstein multiplication represents the same actual product of any chosen integer representatives.

The unchanged tactic script uses 3 declared prerequisites and contains 76 exact native proof lines.

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

Proof neighborhood

Direct dependencies

gaussian_representation_integer_transport Alpha theorem; checked-use authorized EI0023 eisenstein_product_integer_congruence gaussian_representation_equal Alpha theorem; checked-use authorized

Direct dependents

EI003E eisenstein_multiply_functional

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

76 script commands · 9 reading checkpoints · 0 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 product integer congruence
01Fix variables and assumptionsL1–10

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

  1. L1
    intro ac
  2. L2
    intro bc
  3. L3
    intro cc
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro d
  8. L8
    intro e
  9. L9
    intro f
  10. L10
    intro g
02Fix variables and assumptionsL11–14

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

  1. L11
    intro h
  2. L12
    intro hfirst
  3. L13
    intro hsecond
  4. L14
    intro hoperation
03Separate the logical casesL15–24

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

  1. L15
    cases hoperation
  2. L16
    cases hoperation_witness
  3. L17
    cases hoperation_witness_witness
  4. L18
    cases hoperation_witness_witness_witness
  5. L19
    cases hoperation_witness_witness_witness_witness
  6. L20
    cases hoperation_witness_witness_witness_witness_witness
  7. L21
    cases hoperation_witness_witness_witness_witness_witness_witness
  8. L22
    cases hoperation_witness_witness_witness_witness_witness_witness_witness
  9. L23
    cases hoperation_witness_witness_witness_witness_witness_witness_witness_witness
  10. L24
    cases hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right
04Use earlier factsL25–34

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

  1. L25
    specialize gaussian_representation_integer_transport cc
  2. L26
    specialize gaussian_representation_integer_transport ((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))
  3. L27
    specialize gaussian_representation_integer_transport ((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))
  4. L28
    specialize gaussian_representation_integer_transport ((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) + (((((x2) * (x7))) + (((x3) * (x6))))))
  5. L29
    specialize gaussian_representation_integer_transport ((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) + (((((x2) * (x6))) + (((x3) * (x7))))))
  6. L30
    specialize gaussian_representation_integer_transport ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  7. L31
    specialize gaussian_representation_integer_transport ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  8. L32
    specialize gaussian_representation_integer_transport ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  9. L33
    specialize gaussian_representation_integer_transport ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  10. L34
    apply gaussian_representation_integer_transport
05Use earlier factsL35–44

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

  1. L35
    specialize eisenstein_product_integer_congruence x
  2. L36
    specialize eisenstein_product_integer_congruence x1
  3. L37
    specialize eisenstein_product_integer_congruence x2
  4. L38
    specialize eisenstein_product_integer_congruence x3
  5. L39
    specialize eisenstein_product_integer_congruence a
  6. L40
    specialize eisenstein_product_integer_congruence b
  7. L41
    specialize eisenstein_product_integer_congruence c
  8. L42
    specialize eisenstein_product_integer_congruence d
  9. L43
    specialize eisenstein_product_integer_congruence x4
  10. L44
    specialize eisenstein_product_integer_congruence x5
06Use earlier factsL45–54

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

  1. L45
    specialize eisenstein_product_integer_congruence x6
  2. L46
    specialize eisenstein_product_integer_congruence x7
  3. L47
    specialize eisenstein_product_integer_congruence e
  4. L48
    specialize eisenstein_product_integer_congruence f
  5. L49
    specialize eisenstein_product_integer_congruence g
  6. L50
    specialize eisenstein_product_integer_congruence h
  7. L51
    apply eisenstein_product_integer_congruence
  8. L52
    specialize gaussian_representation_equal ac
  9. L53
    specialize gaussian_representation_equal x
  10. L54
    specialize gaussian_representation_equal x1
07Use earlier factsL55–64

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

  1. L55
    specialize gaussian_representation_equal x2
  2. L56
    specialize gaussian_representation_equal x3
  3. L57
    specialize gaussian_representation_equal a
  4. L58
    specialize gaussian_representation_equal b
  5. L59
    specialize gaussian_representation_equal c
  6. L60
    specialize gaussian_representation_equal d
  7. L61
    apply gaussian_representation_equal
  8. L62
    exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_left
  9. L63
    exact hfirst
  10. L64
    specialize gaussian_representation_equal bc
08Use earlier factsL65–74

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

  1. L65
    specialize gaussian_representation_equal x4
  2. L66
    specialize gaussian_representation_equal x5
  3. L67
    specialize gaussian_representation_equal x6
  4. L68
    specialize gaussian_representation_equal x7
  5. L69
    specialize gaussian_representation_equal e
  6. L70
    specialize gaussian_representation_equal f
  7. L71
    specialize gaussian_representation_equal g
  8. L72
    specialize gaussian_representation_equal h
  9. L73
    apply gaussian_representation_equal
  10. L74
    exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right_left
09Use earlier factsL75–76

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

  1. L75
    exact hsecond
  2. L76
    exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 76 lines
  1. 0001intro ac
  2. 0002intro bc
  3. 0003intro cc
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro d
  8. 0008intro e
  9. 0009intro f
  10. 0010intro g
  11. 0011intro h
  12. 0012intro hfirst
  13. 0013intro hsecond
  14. 0014intro hoperation
  15. 0015cases hoperation
  16. 0016cases hoperation_witness
  17. 0017cases hoperation_witness_witness
  18. 0018cases hoperation_witness_witness_witness
  19. 0019cases hoperation_witness_witness_witness_witness
  20. 0020cases hoperation_witness_witness_witness_witness_witness
  21. 0021cases hoperation_witness_witness_witness_witness_witness_witness
  22. 0022cases hoperation_witness_witness_witness_witness_witness_witness_witness
  23. 0023cases hoperation_witness_witness_witness_witness_witness_witness_witness_witness
  24. 0024cases hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right
  25. 0025specialize gaussian_representation_integer_transport cc
  26. 0026specialize gaussian_representation_integer_transport ((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))
  27. 0027specialize gaussian_representation_integer_transport ((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))
  28. 0028specialize gaussian_representation_integer_transport ((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) + (((((x2) * (x7))) + (((x3) * (x6))))))
  29. 0029specialize gaussian_representation_integer_transport ((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) + (((((x2) * (x6))) + (((x3) * (x7))))))
  30. 0030specialize gaussian_representation_integer_transport ((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))
  31. 0031specialize gaussian_representation_integer_transport ((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))
  32. 0032specialize gaussian_representation_integer_transport ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))
  33. 0033specialize gaussian_representation_integer_transport ((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))
  34. 0034apply gaussian_representation_integer_transport
  35. 0035specialize eisenstein_product_integer_congruence x
  36. 0036specialize eisenstein_product_integer_congruence x1
  37. 0037specialize eisenstein_product_integer_congruence x2
  38. 0038specialize eisenstein_product_integer_congruence x3
  39. 0039specialize eisenstein_product_integer_congruence a
  40. 0040specialize eisenstein_product_integer_congruence b
  41. 0041specialize eisenstein_product_integer_congruence c
  42. 0042specialize eisenstein_product_integer_congruence d
  43. 0043specialize eisenstein_product_integer_congruence x4
  44. 0044specialize eisenstein_product_integer_congruence x5
  45. 0045specialize eisenstein_product_integer_congruence x6
  46. 0046specialize eisenstein_product_integer_congruence x7
  47. 0047specialize eisenstein_product_integer_congruence e
  48. 0048specialize eisenstein_product_integer_congruence f
  49. 0049specialize eisenstein_product_integer_congruence g
  50. 0050specialize eisenstein_product_integer_congruence h
  51. 0051apply eisenstein_product_integer_congruence
  52. 0052specialize gaussian_representation_equal ac
  53. 0053specialize gaussian_representation_equal x
  54. 0054specialize gaussian_representation_equal x1
  55. 0055specialize gaussian_representation_equal x2
  56. 0056specialize gaussian_representation_equal x3
  57. 0057specialize gaussian_representation_equal a
  58. 0058specialize gaussian_representation_equal b
  59. 0059specialize gaussian_representation_equal c
  60. 0060specialize gaussian_representation_equal d
  61. 0061apply gaussian_representation_equal
  62. 0062exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_left
  63. 0063exact hfirst
  64. 0064specialize gaussian_representation_equal bc
  65. 0065specialize gaussian_representation_equal x4
  66. 0066specialize gaussian_representation_equal x5
  67. 0067specialize gaussian_representation_equal x6
  68. 0068specialize gaussian_representation_equal x7
  69. 0069specialize gaussian_representation_equal e
  70. 0070specialize gaussian_representation_equal f
  71. 0071specialize gaussian_representation_equal g
  72. 0072specialize gaussian_representation_equal h
  73. 0073apply gaussian_representation_equal
  74. 0074exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  75. 0075exact hsecond
  76. 0076exact hoperation_witness_witness_witness_witness_witness_witness_witness_witness_right_right