GF008E

gaussian_product_result_valid

Every actual finite Gaussian product has a valid carrier code, including the empty product.

Alpha v34 checked-use · first admitted v30 · 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.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ l. ∀ b. ∀ c. ∀ P. GProduct(b,c,l,P) → ZPairValid(P)

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

Definition DAG

ZPairValid(z) · 1GMul(a,b,c) · 1GProduct(b,c,l,P) · 2BetaAt(b,c,i,x) · 1

Actual proof prerequisites

gaussian_product_empty_valuegaussian_one_validgaussian_product_successor_decomposegaussian_multiply_output_valid
Original expanded first-order statement 
forall l b c P. (exists gr_product_trace_product_result_valid gr_product_scale_product_result_valid. ((((exists ff_h_gprod_product_result_validstart. ff_h_gprod_product_result_validstart + S (6) = S ((S (0)) * gr_product_scale_product_result_valid)) /\ exists ff_q_gprod_product_result_validstart. gr_product_trace_product_result_valid = ff_q_gprod_product_result_validstart * S ((S (0)) * gr_product_scale_product_result_valid) + (6))) /\ ((((exists ff_h_gprod_product_result_validend. ff_h_gprod_product_result_validend + S (P) = S ((S (l)) * gr_product_scale_product_result_valid)) /\ exists ff_q_gprod_product_result_validend. gr_product_trace_product_result_valid = ff_q_gprod_product_result_validend * S ((S (l)) * gr_product_scale_product_result_valid) + (P))) /\ (forall gr_product_index_product_result_validsteps. (exists ge_gap_product_result_validstepsindex_bound. ge_gap_product_result_validstepsindex_bound + S (gr_product_index_product_result_validsteps) = (l)) -> exists gr_product_factor_product_result_validsteps gr_product_before_product_result_validsteps gr_product_after_product_result_validsteps. ((((exists ff_h_gprod_product_result_validstepsfactor. ff_h_gprod_product_result_validstepsfactor + S (gr_product_factor_product_result_validsteps) = S ((S (gr_product_index_product_result_validsteps)) * c)) /\ exists ff_q_gprod_product_result_validstepsfactor. b = ff_q_gprod_product_result_validstepsfactor * S ((S (gr_product_index_product_result_validsteps)) * c) + (gr_product_factor_product_result_validsteps))) /\ ((((exists ff_h_gprod_product_result_validstepsbefore. ff_h_gprod_product_result_validstepsbefore + S (gr_product_before_product_result_validsteps) = S ((S (gr_product_index_product_result_validsteps)) * gr_product_scale_product_result_valid)) /\ exists ff_q_gprod_product_result_validstepsbefore. gr_product_trace_product_result_valid = ff_q_gprod_product_result_validstepsbefore * S ((S (gr_product_index_product_result_validsteps)) * gr_product_scale_product_result_valid) + (gr_product_before_product_result_validsteps))) /\ ((((exists ff_h_gprod_product_result_validstepsafter. ff_h_gprod_product_result_validstepsafter + S (gr_product_after_product_result_validsteps) = S ((S (S (gr_product_index_product_result_validsteps))) * gr_product_scale_product_result_valid)) /\ exists ff_q_gprod_product_result_validstepsafter. gr_product_trace_product_result_valid = ff_q_gprod_product_result_validstepsafter * S ((S (S (gr_product_index_product_result_validsteps))) * gr_product_scale_product_result_valid) + (gr_product_after_product_result_validsteps))) /\ (exists ge_first_rp_product_result_validstepsmultiply ge_first_rn_product_result_validstepsmultiply ge_first_ip_product_result_validstepsmultiply ge_first_in_product_result_validstepsmultiply ge_second_rp_product_result_validstepsmultiply ge_second_rn_product_result_validstepsmultiply ge_second_ip_product_result_validstepsmultiply ge_second_in_product_result_validstepsmultiply. ((exists ge_representation_real_code_product_result_validstepsmultiplyfirst ge_representation_imaginary_code_product_result_validstepsmultiplyfirst. (((gr_product_before_product_result_validsteps) = ((ge_representation_real_code_product_result_validstepsmultiplyfirst) + (ge_representation_imaginary_code_product_result_validstepsmultiplyfirst)) * S ((ge_representation_real_code_product_result_validstepsmultiplyfirst) + (ge_representation_imaginary_code_product_result_validstepsmultiplyfirst)) + ((ge_representation_imaginary_code_product_result_validstepsmultiplyfirst) + (ge_representation_imaginary_code_product_result_validstepsmultiplyfirst))) /\ ((exists ge_balance_positive_product_result_validstepsmultiplyfirstreal ge_balance_negative_product_result_validstepsmultiplyfirstreal. (((((ge_representation_real_code_product_result_validstepsmultiplyfirst) = 2 * (ge_balance_positive_product_result_validstepsmultiplyfirstreal) /\ (ge_balance_negative_product_result_validstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplyfirstrealdecode. (((ge_representation_real_code_product_result_validstepsmultiplyfirst) = 2 * ge_signed_half_product_result_validstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplyfirstreal) = S ge_signed_half_product_result_validstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_product_result_validstepsmultiply) + ge_balance_negative_product_result_validstepsmultiplyfirstreal = (ge_first_rn_product_result_validstepsmultiply) + ge_balance_positive_product_result_validstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_product_result_validstepsmultiplyfirstimaginary ge_balance_negative_product_result_validstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_product_result_validstepsmultiplyfirst) = 2 * (ge_balance_positive_product_result_validstepsmultiplyfirstimaginary) /\ (ge_balance_negative_product_result_validstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_product_result_validstepsmultiplyfirst) = 2 * ge_signed_half_product_result_validstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplyfirstimaginary) = S ge_signed_half_product_result_validstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_product_result_validstepsmultiply) + ge_balance_negative_product_result_validstepsmultiplyfirstimaginary = (ge_first_in_product_result_validstepsmultiply) + ge_balance_positive_product_result_validstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_result_validstepsmultiplysecond ge_representation_imaginary_code_product_result_validstepsmultiplysecond. (((gr_product_factor_product_result_validsteps) = ((ge_representation_real_code_product_result_validstepsmultiplysecond) + (ge_representation_imaginary_code_product_result_validstepsmultiplysecond)) * S ((ge_representation_real_code_product_result_validstepsmultiplysecond) + (ge_representation_imaginary_code_product_result_validstepsmultiplysecond)) + ((ge_representation_imaginary_code_product_result_validstepsmultiplysecond) + (ge_representation_imaginary_code_product_result_validstepsmultiplysecond))) /\ ((exists ge_balance_positive_product_result_validstepsmultiplysecondreal ge_balance_negative_product_result_validstepsmultiplysecondreal. (((((ge_representation_real_code_product_result_validstepsmultiplysecond) = 2 * (ge_balance_positive_product_result_validstepsmultiplysecondreal) /\ (ge_balance_negative_product_result_validstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplysecondrealdecode. (((ge_representation_real_code_product_result_validstepsmultiplysecond) = 2 * ge_signed_half_product_result_validstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplysecondreal) = S ge_signed_half_product_result_validstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_product_result_validstepsmultiply) + ge_balance_negative_product_result_validstepsmultiplysecondreal = (ge_second_rn_product_result_validstepsmultiply) + ge_balance_positive_product_result_validstepsmultiplysecondreal))) /\ (exists ge_balance_positive_product_result_validstepsmultiplysecondimaginary ge_balance_negative_product_result_validstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_product_result_validstepsmultiplysecond) = 2 * (ge_balance_positive_product_result_validstepsmultiplysecondimaginary) /\ (ge_balance_negative_product_result_validstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_product_result_validstepsmultiplysecond) = 2 * ge_signed_half_product_result_validstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplysecondimaginary) = S ge_signed_half_product_result_validstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_product_result_validstepsmultiply) + ge_balance_negative_product_result_validstepsmultiplysecondimaginary = (ge_second_in_product_result_validstepsmultiply) + ge_balance_positive_product_result_validstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_product_result_validstepsmultiplyoutput ge_representation_imaginary_code_product_result_validstepsmultiplyoutput. (((gr_product_after_product_result_validsteps) = ((ge_representation_real_code_product_result_validstepsmultiplyoutput) + (ge_representation_imaginary_code_product_result_validstepsmultiplyoutput)) * S ((ge_representation_real_code_product_result_validstepsmultiplyoutput) + (ge_representation_imaginary_code_product_result_validstepsmultiplyoutput)) + ((ge_representation_imaginary_code_product_result_validstepsmultiplyoutput) + (ge_representation_imaginary_code_product_result_validstepsmultiplyoutput))) /\ ((exists ge_balance_positive_product_result_validstepsmultiplyoutputreal ge_balance_negative_product_result_validstepsmultiplyoutputreal. (((((ge_representation_real_code_product_result_validstepsmultiplyoutput) = 2 * (ge_balance_positive_product_result_validstepsmultiplyoutputreal) /\ (ge_balance_negative_product_result_validstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplyoutputrealdecode. (((ge_representation_real_code_product_result_validstepsmultiplyoutput) = 2 * ge_signed_half_product_result_validstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplyoutputreal) = S ge_signed_half_product_result_validstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_product_result_validstepsmultiply) * (ge_second_rp_product_result_validstepsmultiply))) + (((ge_first_rn_product_result_validstepsmultiply) * (ge_second_rn_product_result_validstepsmultiply))))) + (((((ge_first_ip_product_result_validstepsmultiply) * (ge_second_in_product_result_validstepsmultiply))) + (((ge_first_in_product_result_validstepsmultiply) * (ge_second_ip_product_result_validstepsmultiply))))))) + ge_balance_negative_product_result_validstepsmultiplyoutputreal = (((((((ge_first_rp_product_result_validstepsmultiply) * (ge_second_rn_product_result_validstepsmultiply))) + (((ge_first_rn_product_result_validstepsmultiply) * (ge_second_rp_product_result_validstepsmultiply))))) + (((((ge_first_ip_product_result_validstepsmultiply) * (ge_second_ip_product_result_validstepsmultiply))) + (((ge_first_in_product_result_validstepsmultiply) * (ge_second_in_product_result_validstepsmultiply))))))) + ge_balance_positive_product_result_validstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_product_result_validstepsmultiplyoutputimaginary ge_balance_negative_product_result_validstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_product_result_validstepsmultiplyoutput) = 2 * (ge_balance_positive_product_result_validstepsmultiplyoutputimaginary) /\ (ge_balance_negative_product_result_validstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_product_result_validstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_product_result_validstepsmultiplyoutput) = 2 * ge_signed_half_product_result_validstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_product_result_validstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_product_result_validstepsmultiplyoutputimaginary) = S ge_signed_half_product_result_validstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_result_validstepsmultiply) * (ge_second_ip_product_result_validstepsmultiply))) + (((ge_first_rn_product_result_validstepsmultiply) * (ge_second_in_product_result_validstepsmultiply))))) + (((((ge_first_ip_product_result_validstepsmultiply) * (ge_second_rp_product_result_validstepsmultiply))) + (((ge_first_in_product_result_validstepsmultiply) * (ge_second_rn_product_result_validstepsmultiply))))))) + ge_balance_negative_product_result_validstepsmultiplyoutputimaginary = (((((((ge_first_rp_product_result_validstepsmultiply) * (ge_second_in_product_result_validstepsmultiply))) + (((ge_first_rn_product_result_validstepsmultiply) * (ge_second_ip_product_result_validstepsmultiply))))) + (((((ge_first_ip_product_result_validstepsmultiply) * (ge_second_rn_product_result_validstepsmultiply))) + (((ge_first_in_product_result_validstepsmultiply) * (ge_second_rp_product_result_validstepsmultiply))))))) + ge_balance_positive_product_result_validstepsmultiplyoutputimaginary)))))))))))))))) -> (exists ge_real_positive_product_carrier ge_real_negative_product_carrier ge_imaginary_positive_product_carrier ge_imaginary_negative_product_carrier. (exists ge_real_code_product_carrierdecode ge_imaginary_code_product_carrierdecode. (((P) = ((ge_real_code_product_carrierdecode) + (ge_imaginary_code_product_carrierdecode)) * S ((ge_real_code_product_carrierdecode) + (ge_imaginary_code_product_carrierdecode)) + ((ge_imaginary_code_product_carrierdecode) + (ge_imaginary_code_product_carrierdecode))) /\ (((((ge_real_code_product_carrierdecode) = 2 * (ge_real_positive_product_carrier) /\ (ge_real_negative_product_carrier) = 0) \/ exists ge_signed_half_ge_product_carrierdecode_real. (((ge_real_code_product_carrierdecode) = 2 * ge_signed_half_ge_product_carrierdecode_real + 1 /\ (ge_real_positive_product_carrier) = 0) /\ (ge_real_negative_product_carrier) = S ge_signed_half_ge_product_carrierdecode_real))) /\ ((((ge_imaginary_code_product_carrierdecode) = 2 * (ge_imaginary_positive_product_carrier) /\ (ge_imaginary_negative_product_carrier) = 0) \/ exists ge_signed_half_ge_product_carrierdecode_imaginary. (((ge_imaginary_code_product_carrierdecode) = 2 * ge_signed_half_ge_product_carrierdecode_imaginary + 1 /\ (ge_imaginary_positive_product_carrier) = 0) /\ (ge_imaginary_negative_product_carrier) = S ge_signed_half_ge_product_carrierdecode_imaginary)))))))

Complete tactic proof in conservative notation

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

33 script commands · 6 reading checkpoints · 2 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 (4)
gaussian product empty valuegaussian one validgaussian product successor decomposegaussian multiply output valid
01Induction on lL1–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction l
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro P
  5. L5
    intro hp
02Establish heqL6–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product empty value.

  1. L6
    have heq : P=6
  2. L7
    specialize gaussian_product_empty_value (b)
  3. L8
    specialize gaussian_product_empty_value (c)
  4. L9
    specialize gaussian_product_empty_value (P)
  5. L10
    apply gaussian_product_empty_value
  6. L11
    exact hp
  7. L12
    rewrite heq
  8. L13
    exact gaussian_one_valid
  9. L14
    intro b
  10. L15
    intro c
03Fix variables and assumptionsL16–17

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

  1. L16
    intro P
  2. L17
    intro hp
04Establish hsL18–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product successor decompose.

  1. L18
    have hs : ∃ a. ∃ Q. BetaAt(b,c,l,a) ∧ (GProduct(b,c,l,Q) ∧ GMul(Q,a,P))Definitions: BetaAt(b,c,l,a)GProduct(b,c,l,Q)GMul(Q,a,P)Original native command in the exact edition
  2. L19
    specialize gaussian_product_successor_decompose (b)
  3. L20
    specialize gaussian_product_successor_decompose (c)
  4. L21
    specialize gaussian_product_successor_decompose (l)
  5. L22
    specialize gaussian_product_successor_decompose (P)
  6. L23
    apply gaussian_product_successor_decompose
  7. L24
    exact hp
05Separate the logical casesL25–28

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

  1. L25
    cases hs
  2. L26
    cases hs_witness
  3. L27
    cases hs_witness_witness
  4. L28
    cases hs_witness_witness_right
06Use earlier factsL29–33

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

  1. L29
    specialize gaussian_multiply_output_valid (x1)
  2. L30
    specialize gaussian_multiply_output_valid (x)
  3. L31
    specialize gaussian_multiply_output_valid (P)
  4. L32
    apply gaussian_multiply_output_valid
  5. L33
    exact hs_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001induction l
  2. 0002intro b
  3. 0003intro c
  4. 0004intro P
  5. 0005intro hp
  6. 0006have heq : P=6
  7. 0007specialize gaussian_product_empty_value (b)
  8. 0008specialize gaussian_product_empty_value (c)
  9. 0009specialize gaussian_product_empty_value (P)
  10. 0010apply gaussian_product_empty_value
  11. 0011exact hp
  12. 0012rewrite heq
  13. 0013exact gaussian_one_valid
  14. 0014intro b
  15. 0015intro c
  16. 0016intro P
  17. 0017intro hp
  18. 0018have hs : ∃ a. ∃ Q. BetaAt(b,c,l,a) ∧ (GProduct(b,c,l,Q) ∧ GMul(Q,a,P))
  19. 0019specialize gaussian_product_successor_decompose (b)
  20. 0020specialize gaussian_product_successor_decompose (c)
  21. 0021specialize gaussian_product_successor_decompose (l)
  22. 0022specialize gaussian_product_successor_decompose (P)
  23. 0023apply gaussian_product_successor_decompose
  24. 0024exact hp
  25. 0025cases hs
  26. 0026cases hs_witness
  27. 0027cases hs_witness_witness
  28. 0028cases hs_witness_witness_right
  29. 0029specialize gaussian_multiply_output_valid (x1)
  30. 0030specialize gaussian_multiply_output_valid (x)
  31. 0031specialize gaussian_multiply_output_valid (P)
  32. 0032apply gaussian_multiply_output_valid
  33. 0033exact hs_witness_witness_right_right