GF0087

gaussian_product_empty_value

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

Functionality of the zero-th trace entry forces the actual empty product to be the Gaussian identity code.

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 b c P. (exists gr_product_trace_empty_product_value gr_product_scale_empty_product_value. ((((exists ff_h_gprod_empty_product_valuestart. ff_h_gprod_empty_product_valuestart + S (6) = S ((S (0)) * gr_product_scale_empty_product_value)) /\ exists ff_q_gprod_empty_product_valuestart. gr_product_trace_empty_product_value = ff_q_gprod_empty_product_valuestart * S ((S (0)) * gr_product_scale_empty_product_value) + (6))) /\ ((((exists ff_h_gprod_empty_product_valueend. ff_h_gprod_empty_product_valueend + S (P) = S ((S (0)) * gr_product_scale_empty_product_value)) /\ exists ff_q_gprod_empty_product_valueend. gr_product_trace_empty_product_value = ff_q_gprod_empty_product_valueend * S ((S (0)) * gr_product_scale_empty_product_value) + (P))) /\ (forall gr_product_index_empty_product_valuesteps. (exists ge_gap_empty_product_valuestepsindex_bound. ge_gap_empty_product_valuestepsindex_bound + S (gr_product_index_empty_product_valuesteps) = (0)) -> exists gr_product_factor_empty_product_valuesteps gr_product_before_empty_product_valuesteps gr_product_after_empty_product_valuesteps. ((((exists ff_h_gprod_empty_product_valuestepsfactor. ff_h_gprod_empty_product_valuestepsfactor + S (gr_product_factor_empty_product_valuesteps) = S ((S (gr_product_index_empty_product_valuesteps)) * c)) /\ exists ff_q_gprod_empty_product_valuestepsfactor. b = ff_q_gprod_empty_product_valuestepsfactor * S ((S (gr_product_index_empty_product_valuesteps)) * c) + (gr_product_factor_empty_product_valuesteps))) /\ ((((exists ff_h_gprod_empty_product_valuestepsbefore. ff_h_gprod_empty_product_valuestepsbefore + S (gr_product_before_empty_product_valuesteps) = S ((S (gr_product_index_empty_product_valuesteps)) * gr_product_scale_empty_product_value)) /\ exists ff_q_gprod_empty_product_valuestepsbefore. gr_product_trace_empty_product_value = ff_q_gprod_empty_product_valuestepsbefore * S ((S (gr_product_index_empty_product_valuesteps)) * gr_product_scale_empty_product_value) + (gr_product_before_empty_product_valuesteps))) /\ ((((exists ff_h_gprod_empty_product_valuestepsafter. ff_h_gprod_empty_product_valuestepsafter + S (gr_product_after_empty_product_valuesteps) = S ((S (S (gr_product_index_empty_product_valuesteps))) * gr_product_scale_empty_product_value)) /\ exists ff_q_gprod_empty_product_valuestepsafter. gr_product_trace_empty_product_value = ff_q_gprod_empty_product_valuestepsafter * S ((S (S (gr_product_index_empty_product_valuesteps))) * gr_product_scale_empty_product_value) + (gr_product_after_empty_product_valuesteps))) /\ (exists ge_first_rp_empty_product_valuestepsmultiply ge_first_rn_empty_product_valuestepsmultiply ge_first_ip_empty_product_valuestepsmultiply ge_first_in_empty_product_valuestepsmultiply ge_second_rp_empty_product_valuestepsmultiply ge_second_rn_empty_product_valuestepsmultiply ge_second_ip_empty_product_valuestepsmultiply ge_second_in_empty_product_valuestepsmultiply. ((exists ge_representation_real_code_empty_product_valuestepsmultiplyfirst ge_representation_imaginary_code_empty_product_valuestepsmultiplyfirst. (((gr_product_before_empty_product_valuesteps) = ((ge_representation_real_code_empty_product_valuestepsmultiplyfirst) + (ge_representation_imaginary_code_empty_product_valuestepsmultiplyfirst)) * S ((ge_representation_real_code_empty_product_valuestepsmultiplyfirst) + (ge_representation_imaginary_code_empty_product_valuestepsmultiplyfirst)) + ((ge_representation_imaginary_code_empty_product_valuestepsmultiplyfirst) + (ge_representation_imaginary_code_empty_product_valuestepsmultiplyfirst))) /\ ((exists ge_balance_positive_empty_product_valuestepsmultiplyfirstreal ge_balance_negative_empty_product_valuestepsmultiplyfirstreal. (((((ge_representation_real_code_empty_product_valuestepsmultiplyfirst) = 2 * (ge_balance_positive_empty_product_valuestepsmultiplyfirstreal) /\ (ge_balance_negative_empty_product_valuestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_empty_product_valuestepsmultiplyfirstrealdecode. (((ge_representation_real_code_empty_product_valuestepsmultiplyfirst) = 2 * ge_signed_half_empty_product_valuestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_empty_product_valuestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_empty_product_valuestepsmultiplyfirstreal) = S ge_signed_half_empty_product_valuestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_empty_product_valuestepsmultiply) + ge_balance_negative_empty_product_valuestepsmultiplyfirstreal = (ge_first_rn_empty_product_valuestepsmultiply) + ge_balance_positive_empty_product_valuestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_empty_product_valuestepsmultiplyfirstimaginary ge_balance_negative_empty_product_valuestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_empty_product_valuestepsmultiplyfirst) = 2 * (ge_balance_positive_empty_product_valuestepsmultiplyfirstimaginary) /\ (ge_balance_negative_empty_product_valuestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_empty_product_valuestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_empty_product_valuestepsmultiplyfirst) = 2 * ge_signed_half_empty_product_valuestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_empty_product_valuestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_empty_product_valuestepsmultiplyfirstimaginary) = S ge_signed_half_empty_product_valuestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_empty_product_valuestepsmultiply) + ge_balance_negative_empty_product_valuestepsmultiplyfirstimaginary = (ge_first_in_empty_product_valuestepsmultiply) + ge_balance_positive_empty_product_valuestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_empty_product_valuestepsmultiplysecond ge_representation_imaginary_code_empty_product_valuestepsmultiplysecond. (((gr_product_factor_empty_product_valuesteps) = ((ge_representation_real_code_empty_product_valuestepsmultiplysecond) + (ge_representation_imaginary_code_empty_product_valuestepsmultiplysecond)) * S ((ge_representation_real_code_empty_product_valuestepsmultiplysecond) + (ge_representation_imaginary_code_empty_product_valuestepsmultiplysecond)) + ((ge_representation_imaginary_code_empty_product_valuestepsmultiplysecond) + (ge_representation_imaginary_code_empty_product_valuestepsmultiplysecond))) /\ ((exists ge_balance_positive_empty_product_valuestepsmultiplysecondreal ge_balance_negative_empty_product_valuestepsmultiplysecondreal. (((((ge_representation_real_code_empty_product_valuestepsmultiplysecond) = 2 * (ge_balance_positive_empty_product_valuestepsmultiplysecondreal) /\ (ge_balance_negative_empty_product_valuestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_empty_product_valuestepsmultiplysecondrealdecode. (((ge_representation_real_code_empty_product_valuestepsmultiplysecond) = 2 * ge_signed_half_empty_product_valuestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_empty_product_valuestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_empty_product_valuestepsmultiplysecondreal) = S ge_signed_half_empty_product_valuestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_empty_product_valuestepsmultiply) + ge_balance_negative_empty_product_valuestepsmultiplysecondreal = (ge_second_rn_empty_product_valuestepsmultiply) + ge_balance_positive_empty_product_valuestepsmultiplysecondreal))) /\ (exists ge_balance_positive_empty_product_valuestepsmultiplysecondimaginary ge_balance_negative_empty_product_valuestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_empty_product_valuestepsmultiplysecond) = 2 * (ge_balance_positive_empty_product_valuestepsmultiplysecondimaginary) /\ (ge_balance_negative_empty_product_valuestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_empty_product_valuestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_empty_product_valuestepsmultiplysecond) = 2 * ge_signed_half_empty_product_valuestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_empty_product_valuestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_empty_product_valuestepsmultiplysecondimaginary) = S ge_signed_half_empty_product_valuestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_empty_product_valuestepsmultiply) + ge_balance_negative_empty_product_valuestepsmultiplysecondimaginary = (ge_second_in_empty_product_valuestepsmultiply) + ge_balance_positive_empty_product_valuestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_empty_product_valuestepsmultiplyoutput ge_representation_imaginary_code_empty_product_valuestepsmultiplyoutput. (((gr_product_after_empty_product_valuesteps) = ((ge_representation_real_code_empty_product_valuestepsmultiplyoutput) + (ge_representation_imaginary_code_empty_product_valuestepsmultiplyoutput)) * S ((ge_representation_real_code_empty_product_valuestepsmultiplyoutput) + (ge_representation_imaginary_code_empty_product_valuestepsmultiplyoutput)) + ((ge_representation_imaginary_code_empty_product_valuestepsmultiplyoutput) + (ge_representation_imaginary_code_empty_product_valuestepsmultiplyoutput))) /\ ((exists ge_balance_positive_empty_product_valuestepsmultiplyoutputreal ge_balance_negative_empty_product_valuestepsmultiplyoutputreal. (((((ge_representation_real_code_empty_product_valuestepsmultiplyoutput) = 2 * (ge_balance_positive_empty_product_valuestepsmultiplyoutputreal) /\ (ge_balance_negative_empty_product_valuestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_empty_product_valuestepsmultiplyoutputrealdecode. (((ge_representation_real_code_empty_product_valuestepsmultiplyoutput) = 2 * ge_signed_half_empty_product_valuestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_empty_product_valuestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_empty_product_valuestepsmultiplyoutputreal) = S ge_signed_half_empty_product_valuestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_empty_product_valuestepsmultiply) * (ge_second_rp_empty_product_valuestepsmultiply))) + (((ge_first_rn_empty_product_valuestepsmultiply) * (ge_second_rn_empty_product_valuestepsmultiply))))) + (((((ge_first_ip_empty_product_valuestepsmultiply) * (ge_second_in_empty_product_valuestepsmultiply))) + (((ge_first_in_empty_product_valuestepsmultiply) * (ge_second_ip_empty_product_valuestepsmultiply))))))) + ge_balance_negative_empty_product_valuestepsmultiplyoutputreal = (((((((ge_first_rp_empty_product_valuestepsmultiply) * (ge_second_rn_empty_product_valuestepsmultiply))) + (((ge_first_rn_empty_product_valuestepsmultiply) * (ge_second_rp_empty_product_valuestepsmultiply))))) + (((((ge_first_ip_empty_product_valuestepsmultiply) * (ge_second_ip_empty_product_valuestepsmultiply))) + (((ge_first_in_empty_product_valuestepsmultiply) * (ge_second_in_empty_product_valuestepsmultiply))))))) + ge_balance_positive_empty_product_valuestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_empty_product_valuestepsmultiplyoutputimaginary ge_balance_negative_empty_product_valuestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_empty_product_valuestepsmultiplyoutput) = 2 * (ge_balance_positive_empty_product_valuestepsmultiplyoutputimaginary) /\ (ge_balance_negative_empty_product_valuestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_empty_product_valuestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_empty_product_valuestepsmultiplyoutput) = 2 * ge_signed_half_empty_product_valuestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_empty_product_valuestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_empty_product_valuestepsmultiplyoutputimaginary) = S ge_signed_half_empty_product_valuestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_empty_product_valuestepsmultiply) * (ge_second_ip_empty_product_valuestepsmultiply))) + (((ge_first_rn_empty_product_valuestepsmultiply) * (ge_second_in_empty_product_valuestepsmultiply))))) + (((((ge_first_ip_empty_product_valuestepsmultiply) * (ge_second_rp_empty_product_valuestepsmultiply))) + (((ge_first_in_empty_product_valuestepsmultiply) * (ge_second_rn_empty_product_valuestepsmultiply))))))) + ge_balance_negative_empty_product_valuestepsmultiplyoutputimaginary = (((((((ge_first_rp_empty_product_valuestepsmultiply) * (ge_second_in_empty_product_valuestepsmultiply))) + (((ge_first_rn_empty_product_valuestepsmultiply) * (ge_second_ip_empty_product_valuestepsmultiply))))) + (((((ge_first_ip_empty_product_valuestepsmultiply) * (ge_second_rn_empty_product_valuestepsmultiply))) + (((ge_first_in_empty_product_valuestepsmultiply) * (ge_second_rp_empty_product_valuestepsmultiply))))))) + ge_balance_positive_empty_product_valuestepsmultiplyoutputimaginary)))))))))))))))) -> P=6

Constructive proof overview

Generated structural guide

Functionality of the zero-th trace entry forces the actual empty product to be the Gaussian identity code.

The unchanged tactic script uses 1 declared prerequisite and contains 16 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized

Direct dependents

GF008D gaussian_product_functional GF008E gaussian_product_result_valid GF009B gaussian_all_irreducible_product_nonzero GF009F gaussian_irreducible_divisor_product_member GF00AF gaussian_irreducible_products_associate_unique

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

16 script commands · 3 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.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro P
  4. L4
    intro hp
02Separate the logical casesL5–8

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

  1. L5
    cases hp
  2. L6
    cases hp_witness
  3. L7
    cases hp_witness_witness
  4. L8
    cases hp_witness_witness_right
03Use earlier factsL9–16

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

  1. L9
    specialize beta_at_unique (x)
  2. L10
    specialize beta_at_unique (x1)
  3. L11
    specialize beta_at_unique (0)
  4. L12
    specialize beta_at_unique (P)
  5. L13
    specialize beta_at_unique (6)
  6. L14
    apply beta_at_unique
  7. L15
    exact hp_witness_witness_right_left
  8. L16
    exact hp_witness_witness_left

Library-wide reading audit

Original exact command ledger · 16 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro P
  4. 0004intro hp
  5. 0005cases hp
  6. 0006cases hp_witness
  7. 0007cases hp_witness_witness
  8. 0008cases hp_witness_witness_right
  9. 0009specialize beta_at_unique (x)
  10. 0010specialize beta_at_unique (x1)
  11. 0011specialize beta_at_unique (0)
  12. 0012specialize beta_at_unique (P)
  13. 0013specialize beta_at_unique (6)
  14. 0014apply beta_at_unique
  15. 0015exact hp_witness_witness_right_left
  16. 0016exact hp_witness_witness_left