GI005B

gaussian_norm_multiply

The actual squared norm of a canonical Gaussian product equals the product of its actual natural squared norms.

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.

The natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

∀ ac. ∀ bc. ∀ cc. ∀ N. ∀ M. GNorm(ac,N) → GNorm(bc,M) → GMul(ac,bc,cc) → GNorm(cc,N · M)

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

Definition DAG

GNorm(z,n) · 3GMul(a,b,c) · 1

Actual proof prerequisites

gaussian_norm_of_representationgaussian_signed_norm_productgaussian_norm_for_representation
Original expanded first-order statement 
forall ac bc cc N M. (exists ge_norm_rp_norm_product_first ge_norm_rn_norm_product_first ge_norm_ip_norm_product_first ge_norm_in_norm_product_first. ((exists ge_representation_real_code_norm_product_firstrepresentation ge_representation_imaginary_code_norm_product_firstrepresentation. (((ac) = ((ge_representation_real_code_norm_product_firstrepresentation) + (ge_representation_imaginary_code_norm_product_firstrepresentation)) * S ((ge_representation_real_code_norm_product_firstrepresentation) + (ge_representation_imaginary_code_norm_product_firstrepresentation)) + ((ge_representation_imaginary_code_norm_product_firstrepresentation) + (ge_representation_imaginary_code_norm_product_firstrepresentation))) /\ ((exists ge_balance_positive_norm_product_firstrepresentationreal ge_balance_negative_norm_product_firstrepresentationreal. (((((ge_representation_real_code_norm_product_firstrepresentation) = 2 * (ge_balance_positive_norm_product_firstrepresentationreal) /\ (ge_balance_negative_norm_product_firstrepresentationreal) = 0) \/ exists ge_signed_half_norm_product_firstrepresentationrealdecode. (((ge_representation_real_code_norm_product_firstrepresentation) = 2 * ge_signed_half_norm_product_firstrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_product_firstrepresentationreal) = 0) /\ (ge_balance_negative_norm_product_firstrepresentationreal) = S ge_signed_half_norm_product_firstrepresentationrealdecode))) /\ ((ge_norm_rp_norm_product_first) + ge_balance_negative_norm_product_firstrepresentationreal = (ge_norm_rn_norm_product_first) + ge_balance_positive_norm_product_firstrepresentationreal))) /\ (exists ge_balance_positive_norm_product_firstrepresentationimaginary ge_balance_negative_norm_product_firstrepresentationimaginary. (((((ge_representation_imaginary_code_norm_product_firstrepresentation) = 2 * (ge_balance_positive_norm_product_firstrepresentationimaginary) /\ (ge_balance_negative_norm_product_firstrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_product_firstrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_product_firstrepresentation) = 2 * ge_signed_half_norm_product_firstrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_product_firstrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_product_firstrepresentationimaginary) = S ge_signed_half_norm_product_firstrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_product_first) + ge_balance_negative_norm_product_firstrepresentationimaginary = (ge_norm_in_norm_product_first) + ge_balance_positive_norm_product_firstrepresentationimaginary)))))) /\ (exists ge_real_square_norm_product_firstsquare ge_imaginary_square_norm_product_firstsquare. ((((((ge_norm_rp_norm_product_first) * (ge_norm_rp_norm_product_first))) + (((ge_norm_rn_norm_product_first) * (ge_norm_rn_norm_product_first)))) = ((ge_real_square_norm_product_firstsquare) + (((((ge_norm_rp_norm_product_first) * (ge_norm_rn_norm_product_first))) + (((ge_norm_rn_norm_product_first) * (ge_norm_rp_norm_product_first))))))) /\ ((((((ge_norm_ip_norm_product_first) * (ge_norm_ip_norm_product_first))) + (((ge_norm_in_norm_product_first) * (ge_norm_in_norm_product_first)))) = ((ge_imaginary_square_norm_product_firstsquare) + (((((ge_norm_ip_norm_product_first) * (ge_norm_in_norm_product_first))) + (((ge_norm_in_norm_product_first) * (ge_norm_ip_norm_product_first))))))) /\ ((N) = ge_real_square_norm_product_firstsquare + ge_imaginary_square_norm_product_firstsquare)))))) -> (exists ge_norm_rp_norm_product_second ge_norm_rn_norm_product_second ge_norm_ip_norm_product_second ge_norm_in_norm_product_second. ((exists ge_representation_real_code_norm_product_secondrepresentation ge_representation_imaginary_code_norm_product_secondrepresentation. (((bc) = ((ge_representation_real_code_norm_product_secondrepresentation) + (ge_representation_imaginary_code_norm_product_secondrepresentation)) * S ((ge_representation_real_code_norm_product_secondrepresentation) + (ge_representation_imaginary_code_norm_product_secondrepresentation)) + ((ge_representation_imaginary_code_norm_product_secondrepresentation) + (ge_representation_imaginary_code_norm_product_secondrepresentation))) /\ ((exists ge_balance_positive_norm_product_secondrepresentationreal ge_balance_negative_norm_product_secondrepresentationreal. (((((ge_representation_real_code_norm_product_secondrepresentation) = 2 * (ge_balance_positive_norm_product_secondrepresentationreal) /\ (ge_balance_negative_norm_product_secondrepresentationreal) = 0) \/ exists ge_signed_half_norm_product_secondrepresentationrealdecode. (((ge_representation_real_code_norm_product_secondrepresentation) = 2 * ge_signed_half_norm_product_secondrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_product_secondrepresentationreal) = 0) /\ (ge_balance_negative_norm_product_secondrepresentationreal) = S ge_signed_half_norm_product_secondrepresentationrealdecode))) /\ ((ge_norm_rp_norm_product_second) + ge_balance_negative_norm_product_secondrepresentationreal = (ge_norm_rn_norm_product_second) + ge_balance_positive_norm_product_secondrepresentationreal))) /\ (exists ge_balance_positive_norm_product_secondrepresentationimaginary ge_balance_negative_norm_product_secondrepresentationimaginary. (((((ge_representation_imaginary_code_norm_product_secondrepresentation) = 2 * (ge_balance_positive_norm_product_secondrepresentationimaginary) /\ (ge_balance_negative_norm_product_secondrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_product_secondrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_product_secondrepresentation) = 2 * ge_signed_half_norm_product_secondrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_product_secondrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_product_secondrepresentationimaginary) = S ge_signed_half_norm_product_secondrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_product_second) + ge_balance_negative_norm_product_secondrepresentationimaginary = (ge_norm_in_norm_product_second) + ge_balance_positive_norm_product_secondrepresentationimaginary)))))) /\ (exists ge_real_square_norm_product_secondsquare ge_imaginary_square_norm_product_secondsquare. ((((((ge_norm_rp_norm_product_second) * (ge_norm_rp_norm_product_second))) + (((ge_norm_rn_norm_product_second) * (ge_norm_rn_norm_product_second)))) = ((ge_real_square_norm_product_secondsquare) + (((((ge_norm_rp_norm_product_second) * (ge_norm_rn_norm_product_second))) + (((ge_norm_rn_norm_product_second) * (ge_norm_rp_norm_product_second))))))) /\ ((((((ge_norm_ip_norm_product_second) * (ge_norm_ip_norm_product_second))) + (((ge_norm_in_norm_product_second) * (ge_norm_in_norm_product_second)))) = ((ge_imaginary_square_norm_product_secondsquare) + (((((ge_norm_ip_norm_product_second) * (ge_norm_in_norm_product_second))) + (((ge_norm_in_norm_product_second) * (ge_norm_ip_norm_product_second))))))) /\ ((M) = ge_real_square_norm_product_secondsquare + ge_imaginary_square_norm_product_secondsquare)))))) -> (exists ge_first_rp_norm_product_operation ge_first_rn_norm_product_operation ge_first_ip_norm_product_operation ge_first_in_norm_product_operation ge_second_rp_norm_product_operation ge_second_rn_norm_product_operation ge_second_ip_norm_product_operation ge_second_in_norm_product_operation. ((exists ge_representation_real_code_norm_product_operationfirst ge_representation_imaginary_code_norm_product_operationfirst. (((ac) = ((ge_representation_real_code_norm_product_operationfirst) + (ge_representation_imaginary_code_norm_product_operationfirst)) * S ((ge_representation_real_code_norm_product_operationfirst) + (ge_representation_imaginary_code_norm_product_operationfirst)) + ((ge_representation_imaginary_code_norm_product_operationfirst) + (ge_representation_imaginary_code_norm_product_operationfirst))) /\ ((exists ge_balance_positive_norm_product_operationfirstreal ge_balance_negative_norm_product_operationfirstreal. (((((ge_representation_real_code_norm_product_operationfirst) = 2 * (ge_balance_positive_norm_product_operationfirstreal) /\ (ge_balance_negative_norm_product_operationfirstreal) = 0) \/ exists ge_signed_half_norm_product_operationfirstrealdecode. (((ge_representation_real_code_norm_product_operationfirst) = 2 * ge_signed_half_norm_product_operationfirstrealdecode + 1 /\ (ge_balance_positive_norm_product_operationfirstreal) = 0) /\ (ge_balance_negative_norm_product_operationfirstreal) = S ge_signed_half_norm_product_operationfirstrealdecode))) /\ ((ge_first_rp_norm_product_operation) + ge_balance_negative_norm_product_operationfirstreal = (ge_first_rn_norm_product_operation) + ge_balance_positive_norm_product_operationfirstreal))) /\ (exists ge_balance_positive_norm_product_operationfirstimaginary ge_balance_negative_norm_product_operationfirstimaginary. (((((ge_representation_imaginary_code_norm_product_operationfirst) = 2 * (ge_balance_positive_norm_product_operationfirstimaginary) /\ (ge_balance_negative_norm_product_operationfirstimaginary) = 0) \/ exists ge_signed_half_norm_product_operationfirstimaginarydecode. (((ge_representation_imaginary_code_norm_product_operationfirst) = 2 * ge_signed_half_norm_product_operationfirstimaginarydecode + 1 /\ (ge_balance_positive_norm_product_operationfirstimaginary) = 0) /\ (ge_balance_negative_norm_product_operationfirstimaginary) = S ge_signed_half_norm_product_operationfirstimaginarydecode))) /\ ((ge_first_ip_norm_product_operation) + ge_balance_negative_norm_product_operationfirstimaginary = (ge_first_in_norm_product_operation) + ge_balance_positive_norm_product_operationfirstimaginary)))))) /\ ((exists ge_representation_real_code_norm_product_operationsecond ge_representation_imaginary_code_norm_product_operationsecond. (((bc) = ((ge_representation_real_code_norm_product_operationsecond) + (ge_representation_imaginary_code_norm_product_operationsecond)) * S ((ge_representation_real_code_norm_product_operationsecond) + (ge_representation_imaginary_code_norm_product_operationsecond)) + ((ge_representation_imaginary_code_norm_product_operationsecond) + (ge_representation_imaginary_code_norm_product_operationsecond))) /\ ((exists ge_balance_positive_norm_product_operationsecondreal ge_balance_negative_norm_product_operationsecondreal. (((((ge_representation_real_code_norm_product_operationsecond) = 2 * (ge_balance_positive_norm_product_operationsecondreal) /\ (ge_balance_negative_norm_product_operationsecondreal) = 0) \/ exists ge_signed_half_norm_product_operationsecondrealdecode. (((ge_representation_real_code_norm_product_operationsecond) = 2 * ge_signed_half_norm_product_operationsecondrealdecode + 1 /\ (ge_balance_positive_norm_product_operationsecondreal) = 0) /\ (ge_balance_negative_norm_product_operationsecondreal) = S ge_signed_half_norm_product_operationsecondrealdecode))) /\ ((ge_second_rp_norm_product_operation) + ge_balance_negative_norm_product_operationsecondreal = (ge_second_rn_norm_product_operation) + ge_balance_positive_norm_product_operationsecondreal))) /\ (exists ge_balance_positive_norm_product_operationsecondimaginary ge_balance_negative_norm_product_operationsecondimaginary. (((((ge_representation_imaginary_code_norm_product_operationsecond) = 2 * (ge_balance_positive_norm_product_operationsecondimaginary) /\ (ge_balance_negative_norm_product_operationsecondimaginary) = 0) \/ exists ge_signed_half_norm_product_operationsecondimaginarydecode. (((ge_representation_imaginary_code_norm_product_operationsecond) = 2 * ge_signed_half_norm_product_operationsecondimaginarydecode + 1 /\ (ge_balance_positive_norm_product_operationsecondimaginary) = 0) /\ (ge_balance_negative_norm_product_operationsecondimaginary) = S ge_signed_half_norm_product_operationsecondimaginarydecode))) /\ ((ge_second_ip_norm_product_operation) + ge_balance_negative_norm_product_operationsecondimaginary = (ge_second_in_norm_product_operation) + ge_balance_positive_norm_product_operationsecondimaginary)))))) /\ (exists ge_representation_real_code_norm_product_operationoutput ge_representation_imaginary_code_norm_product_operationoutput. (((cc) = ((ge_representation_real_code_norm_product_operationoutput) + (ge_representation_imaginary_code_norm_product_operationoutput)) * S ((ge_representation_real_code_norm_product_operationoutput) + (ge_representation_imaginary_code_norm_product_operationoutput)) + ((ge_representation_imaginary_code_norm_product_operationoutput) + (ge_representation_imaginary_code_norm_product_operationoutput))) /\ ((exists ge_balance_positive_norm_product_operationoutputreal ge_balance_negative_norm_product_operationoutputreal. (((((ge_representation_real_code_norm_product_operationoutput) = 2 * (ge_balance_positive_norm_product_operationoutputreal) /\ (ge_balance_negative_norm_product_operationoutputreal) = 0) \/ exists ge_signed_half_norm_product_operationoutputrealdecode. (((ge_representation_real_code_norm_product_operationoutput) = 2 * ge_signed_half_norm_product_operationoutputrealdecode + 1 /\ (ge_balance_positive_norm_product_operationoutputreal) = 0) /\ (ge_balance_negative_norm_product_operationoutputreal) = S ge_signed_half_norm_product_operationoutputrealdecode))) /\ ((((((((ge_first_rp_norm_product_operation) * (ge_second_rp_norm_product_operation))) + (((ge_first_rn_norm_product_operation) * (ge_second_rn_norm_product_operation))))) + (((((ge_first_ip_norm_product_operation) * (ge_second_in_norm_product_operation))) + (((ge_first_in_norm_product_operation) * (ge_second_ip_norm_product_operation))))))) + ge_balance_negative_norm_product_operationoutputreal = (((((((ge_first_rp_norm_product_operation) * (ge_second_rn_norm_product_operation))) + (((ge_first_rn_norm_product_operation) * (ge_second_rp_norm_product_operation))))) + (((((ge_first_ip_norm_product_operation) * (ge_second_ip_norm_product_operation))) + (((ge_first_in_norm_product_operation) * (ge_second_in_norm_product_operation))))))) + ge_balance_positive_norm_product_operationoutputreal))) /\ (exists ge_balance_positive_norm_product_operationoutputimaginary ge_balance_negative_norm_product_operationoutputimaginary. (((((ge_representation_imaginary_code_norm_product_operationoutput) = 2 * (ge_balance_positive_norm_product_operationoutputimaginary) /\ (ge_balance_negative_norm_product_operationoutputimaginary) = 0) \/ exists ge_signed_half_norm_product_operationoutputimaginarydecode. (((ge_representation_imaginary_code_norm_product_operationoutput) = 2 * ge_signed_half_norm_product_operationoutputimaginarydecode + 1 /\ (ge_balance_positive_norm_product_operationoutputimaginary) = 0) /\ (ge_balance_negative_norm_product_operationoutputimaginary) = S ge_signed_half_norm_product_operationoutputimaginarydecode))) /\ ((((((((ge_first_rp_norm_product_operation) * (ge_second_ip_norm_product_operation))) + (((ge_first_rn_norm_product_operation) * (ge_second_in_norm_product_operation))))) + (((((ge_first_ip_norm_product_operation) * (ge_second_rp_norm_product_operation))) + (((ge_first_in_norm_product_operation) * (ge_second_rn_norm_product_operation))))))) + ge_balance_negative_norm_product_operationoutputimaginary = (((((((ge_first_rp_norm_product_operation) * (ge_second_in_norm_product_operation))) + (((ge_first_rn_norm_product_operation) * (ge_second_ip_norm_product_operation))))) + (((((ge_first_ip_norm_product_operation) * (ge_second_rn_norm_product_operation))) + (((ge_first_in_norm_product_operation) * (ge_second_rp_norm_product_operation))))))) + ge_balance_positive_norm_product_operationoutputimaginary))))))))) -> (exists ge_norm_rp_norm_product_output ge_norm_rn_norm_product_output ge_norm_ip_norm_product_output ge_norm_in_norm_product_output. ((exists ge_representation_real_code_norm_product_outputrepresentation ge_representation_imaginary_code_norm_product_outputrepresentation. (((cc) = ((ge_representation_real_code_norm_product_outputrepresentation) + (ge_representation_imaginary_code_norm_product_outputrepresentation)) * S ((ge_representation_real_code_norm_product_outputrepresentation) + (ge_representation_imaginary_code_norm_product_outputrepresentation)) + ((ge_representation_imaginary_code_norm_product_outputrepresentation) + (ge_representation_imaginary_code_norm_product_outputrepresentation))) /\ ((exists ge_balance_positive_norm_product_outputrepresentationreal ge_balance_negative_norm_product_outputrepresentationreal. (((((ge_representation_real_code_norm_product_outputrepresentation) = 2 * (ge_balance_positive_norm_product_outputrepresentationreal) /\ (ge_balance_negative_norm_product_outputrepresentationreal) = 0) \/ exists ge_signed_half_norm_product_outputrepresentationrealdecode. (((ge_representation_real_code_norm_product_outputrepresentation) = 2 * ge_signed_half_norm_product_outputrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_product_outputrepresentationreal) = 0) /\ (ge_balance_negative_norm_product_outputrepresentationreal) = S ge_signed_half_norm_product_outputrepresentationrealdecode))) /\ ((ge_norm_rp_norm_product_output) + ge_balance_negative_norm_product_outputrepresentationreal = (ge_norm_rn_norm_product_output) + ge_balance_positive_norm_product_outputrepresentationreal))) /\ (exists ge_balance_positive_norm_product_outputrepresentationimaginary ge_balance_negative_norm_product_outputrepresentationimaginary. (((((ge_representation_imaginary_code_norm_product_outputrepresentation) = 2 * (ge_balance_positive_norm_product_outputrepresentationimaginary) /\ (ge_balance_negative_norm_product_outputrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_product_outputrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_product_outputrepresentation) = 2 * ge_signed_half_norm_product_outputrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_product_outputrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_product_outputrepresentationimaginary) = S ge_signed_half_norm_product_outputrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_product_output) + ge_balance_negative_norm_product_outputrepresentationimaginary = (ge_norm_in_norm_product_output) + ge_balance_positive_norm_product_outputrepresentationimaginary)))))) /\ (exists ge_real_square_norm_product_outputsquare ge_imaginary_square_norm_product_outputsquare. ((((((ge_norm_rp_norm_product_output) * (ge_norm_rp_norm_product_output))) + (((ge_norm_rn_norm_product_output) * (ge_norm_rn_norm_product_output)))) = ((ge_real_square_norm_product_outputsquare) + (((((ge_norm_rp_norm_product_output) * (ge_norm_rn_norm_product_output))) + (((ge_norm_rn_norm_product_output) * (ge_norm_rp_norm_product_output))))))) /\ ((((((ge_norm_ip_norm_product_output) * (ge_norm_ip_norm_product_output))) + (((ge_norm_in_norm_product_output) * (ge_norm_in_norm_product_output)))) = ((ge_imaginary_square_norm_product_outputsquare) + (((((ge_norm_ip_norm_product_output) * (ge_norm_in_norm_product_output))) + (((ge_norm_in_norm_product_output) * (ge_norm_ip_norm_product_output))))))) /\ ((N * M) = ge_real_square_norm_product_outputsquare + ge_imaginary_square_norm_product_outputsquare))))))

Complete tactic proof in conservative notation

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

55 script commands · 6 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.

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 (3)
gaussian norm of representationgaussian signed norm productgaussian norm for representation
01Fix variables and assumptionsL1–8

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 N
  5. L5
    intro M
  6. L6
    intro hfirst
  7. L7
    intro hsecond
  8. L8
    intro hproduct
02Separate the logical casesL9–18

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

  1. L9
    cases hproduct
  2. L10
    cases hproduct_witness
  3. L11
    cases hproduct_witness_witness
  4. L12
    cases hproduct_witness_witness_witness
  5. L13
    cases hproduct_witness_witness_witness_witness
  6. L14
    cases hproduct_witness_witness_witness_witness_witness
  7. L15
    cases hproduct_witness_witness_witness_witness_witness_witness
  8. L16
    cases hproduct_witness_witness_witness_witness_witness_witness_witness
  9. L17
    cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness
  10. L18
    cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right
03Use earlier factsL19–28

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

  1. L19
    specialize gaussian_norm_of_representation cc
  2. L20
    specialize gaussian_norm_of_representation ((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))
  3. L21
    specialize gaussian_norm_of_representation ((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))
  4. L22
    specialize gaussian_norm_of_representation ((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))
  5. L23
    specialize gaussian_norm_of_representation ((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))
  6. L24
    specialize gaussian_norm_of_representation N * M
  7. L25
    apply gaussian_norm_of_representation
  8. L26
    exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  9. L27
    specialize gaussian_signed_norm_product x
  10. L28
    specialize gaussian_signed_norm_product x1
04Use earlier factsL29–38

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

  1. L29
    specialize gaussian_signed_norm_product x2
  2. L30
    specialize gaussian_signed_norm_product x3
  3. L31
    specialize gaussian_signed_norm_product x4
  4. L32
    specialize gaussian_signed_norm_product x5
  5. L33
    specialize gaussian_signed_norm_product x6
  6. L34
    specialize gaussian_signed_norm_product x7
  7. L35
    specialize gaussian_signed_norm_product N
  8. L36
    specialize gaussian_signed_norm_product M
  9. L37
    apply gaussian_signed_norm_product
  10. L38
    specialize gaussian_norm_for_representation ac
05Use earlier factsL39–48

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

  1. L39
    specialize gaussian_norm_for_representation x
  2. L40
    specialize gaussian_norm_for_representation x1
  3. L41
    specialize gaussian_norm_for_representation x2
  4. L42
    specialize gaussian_norm_for_representation x3
  5. L43
    specialize gaussian_norm_for_representation N
  6. L44
    apply gaussian_norm_for_representation
  7. L45
    exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_left
  8. L46
    exact hfirst
  9. L47
    specialize gaussian_norm_for_representation bc
  10. L48
    specialize gaussian_norm_for_representation x4
06Use earlier factsL49–55

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

  1. L49
    specialize gaussian_norm_for_representation x5
  2. L50
    specialize gaussian_norm_for_representation x6
  3. L51
    specialize gaussian_norm_for_representation x7
  4. L52
    specialize gaussian_norm_for_representation M
  5. L53
    apply gaussian_norm_for_representation
  6. L54
    exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  7. L55
    exact hsecond

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro ac
  2. 0002intro bc
  3. 0003intro cc
  4. 0004intro N
  5. 0005intro M
  6. 0006intro hfirst
  7. 0007intro hsecond
  8. 0008intro hproduct
  9. 0009cases hproduct
  10. 0010cases hproduct_witness
  11. 0011cases hproduct_witness_witness
  12. 0012cases hproduct_witness_witness_witness
  13. 0013cases hproduct_witness_witness_witness_witness
  14. 0014cases hproduct_witness_witness_witness_witness_witness
  15. 0015cases hproduct_witness_witness_witness_witness_witness_witness
  16. 0016cases hproduct_witness_witness_witness_witness_witness_witness_witness
  17. 0017cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness
  18. 0018cases hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right
  19. 0019specialize gaussian_norm_of_representation cc
  20. 0020specialize gaussian_norm_of_representation ((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))
  21. 0021specialize gaussian_norm_of_representation ((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))
  22. 0022specialize gaussian_norm_of_representation ((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))
  23. 0023specialize gaussian_norm_of_representation ((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))
  24. 0024specialize gaussian_norm_of_representation N * M
  25. 0025apply gaussian_norm_of_representation
  26. 0026exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  27. 0027specialize gaussian_signed_norm_product x
  28. 0028specialize gaussian_signed_norm_product x1
  29. 0029specialize gaussian_signed_norm_product x2
  30. 0030specialize gaussian_signed_norm_product x3
  31. 0031specialize gaussian_signed_norm_product x4
  32. 0032specialize gaussian_signed_norm_product x5
  33. 0033specialize gaussian_signed_norm_product x6
  34. 0034specialize gaussian_signed_norm_product x7
  35. 0035specialize gaussian_signed_norm_product N
  36. 0036specialize gaussian_signed_norm_product M
  37. 0037apply gaussian_signed_norm_product
  38. 0038specialize gaussian_norm_for_representation ac
  39. 0039specialize gaussian_norm_for_representation x
  40. 0040specialize gaussian_norm_for_representation x1
  41. 0041specialize gaussian_norm_for_representation x2
  42. 0042specialize gaussian_norm_for_representation x3
  43. 0043specialize gaussian_norm_for_representation N
  44. 0044apply gaussian_norm_for_representation
  45. 0045exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_left
  46. 0046exact hfirst
  47. 0047specialize gaussian_norm_for_representation bc
  48. 0048specialize gaussian_norm_for_representation x4
  49. 0049specialize gaussian_norm_for_representation x5
  50. 0050specialize gaussian_norm_for_representation x6
  51. 0051specialize gaussian_norm_for_representation x7
  52. 0052specialize gaussian_norm_for_representation M
  53. 0053apply gaussian_norm_for_representation
  54. 0054exact hproduct_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  55. 0055exact hsecond