PA00D0

gauss_signed_half_magnitude_sum_equals_half_sum

Alpha v34 checked-use theorem · independently closed; not Stable

Gauss signed-half data makes the magnitude Sum equal the canonical half Sum.

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 PA statement

forall p h a b c mb mc sb sc X M. p = 2 * h + 1 -> ((~(p = 1) /\ forall gsp_prime_left_ges_prime gsp_prime_right_ges_prime. p = gsp_prime_left_ges_prime * gsp_prime_right_ges_prime -> gsp_prime_left_ges_prime = 1 \/ gsp_prime_right_ges_prime = 1)) -> (~(exists gsp_divisor_factor_ges_nondivisor. a = p * gsp_divisor_factor_ges_nondivisor)) -> (forall gsp_range_index_ges_half. (exists gsp_lt_gap_ges_half_range_bound. gsp_lt_gap_ges_half_range_bound + S gsp_range_index_ges_half = h) -> (((exists gsp_beta_height_ges_half_range_entry. gsp_beta_height_ges_half_range_entry + S (1 + gsp_range_index_ges_half) = S ((S (gsp_range_index_ges_half)) * c)) /\ exists gsp_beta_quotient_ges_half_range_entry. b = gsp_beta_quotient_ges_half_range_entry * S ((S (gsp_range_index_ges_half)) * c) + (1 + gsp_range_index_ges_half)))) -> (forall gsp_index_ges_signed. (exists gsp_lt_gap_ges_signed_index_bound. gsp_lt_gap_ges_signed_index_bound + S gsp_index_ges_signed = h) -> (exists gsp_value_ges_signed_entry gsp_magnitude_ges_signed_entry gsp_sign_ges_signed_entry. (((exists ff_h_gsp_ges_signed_entry_source. ff_h_gsp_ges_signed_entry_source + S (gsp_value_ges_signed_entry) = S ((S (gsp_index_ges_signed)) * c)) /\ exists ff_q_gsp_ges_signed_entry_source. b = ff_q_gsp_ges_signed_entry_source * S ((S (gsp_index_ges_signed)) * c) + (gsp_value_ges_signed_entry))) /\ ((((exists ff_h_gsp_ges_signed_entry_magnitude. ff_h_gsp_ges_signed_entry_magnitude + S (gsp_magnitude_ges_signed_entry) = S ((S (gsp_index_ges_signed)) * mc)) /\ exists ff_q_gsp_ges_signed_entry_magnitude. mb = ff_q_gsp_ges_signed_entry_magnitude * S ((S (gsp_index_ges_signed)) * mc) + (gsp_magnitude_ges_signed_entry))) /\ ((((exists ff_h_gsp_ges_signed_entry_sign. ff_h_gsp_ges_signed_entry_sign + S (gsp_sign_ges_signed_entry) = S ((S (gsp_index_ges_signed)) * sc)) /\ exists ff_q_gsp_ges_signed_entry_sign. sb = ff_q_gsp_ges_signed_entry_sign * S ((S (gsp_index_ges_signed)) * sc) + (gsp_sign_ges_signed_entry))) /\ ((exists gsp_lt_gap_ges_signed_entry_positive. gsp_lt_gap_ges_signed_entry_positive + S 0 = gsp_magnitude_ges_signed_entry) /\ ((exists gsp_le_gap_ges_signed_entry_bounded. gsp_le_gap_ges_signed_entry_bounded + gsp_magnitude_ges_signed_entry = h) /\ ((gsp_sign_ges_signed_entry = 0 \/ gsp_sign_ges_signed_entry = 1) /\ (((gsp_sign_ges_signed_entry = 0 /\ (exists gsp_mod_left_ges_signed_entry_lower gsp_mod_right_ges_signed_entry_lower. (a * gsp_value_ges_signed_entry) + p * gsp_mod_left_ges_signed_entry_lower = (gsp_magnitude_ges_signed_entry) + p * gsp_mod_right_ges_signed_entry_lower)) \/ (gsp_sign_ges_signed_entry = 1 /\ (exists gsp_mod_left_ges_signed_entry_reflected gsp_mod_right_ges_signed_entry_reflected. (a * gsp_value_ges_signed_entry) + p * gsp_mod_left_ges_signed_entry_reflected = ((2 * h) * gsp_magnitude_ges_signed_entry) + p * gsp_mod_right_ges_signed_entry_reflected))))))))))) -> (exists ff_u_ges_half_sum ff_v_ges_half_sum. ((((exists ff_h_ges_half_sum_start. ff_h_ges_half_sum_start + S (0) = S ((S (0)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_start. ff_u_ges_half_sum = ff_q_ges_half_sum_start * S ((S (0)) * ff_v_ges_half_sum) + (0))) /\ ((((exists ff_h_ges_half_sum_terminal. ff_h_ges_half_sum_terminal + S (X) = S ((S (h)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_terminal. ff_u_ges_half_sum = ff_q_ges_half_sum_terminal * S ((S (h)) * ff_v_ges_half_sum) + (X))) /\ forall ff_i_ges_half_sum. (exists ff_lt_ges_half_sum_bound. ff_lt_ges_half_sum_bound + S ff_i_ges_half_sum = h) -> exists ff_a_ges_half_sum ff_r_ges_half_sum ff_s_ges_half_sum. ((((exists ff_h_ges_half_sum_summand. ff_h_ges_half_sum_summand + S (ff_a_ges_half_sum) = S ((S (ff_i_ges_half_sum)) * c)) /\ exists ff_q_ges_half_sum_summand. b = ff_q_ges_half_sum_summand * S ((S (ff_i_ges_half_sum)) * c) + (ff_a_ges_half_sum))) /\ ((((exists ff_h_ges_half_sum_partial. ff_h_ges_half_sum_partial + S (ff_r_ges_half_sum) = S ((S (ff_i_ges_half_sum)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_partial. ff_u_ges_half_sum = ff_q_ges_half_sum_partial * S ((S (ff_i_ges_half_sum)) * ff_v_ges_half_sum) + (ff_r_ges_half_sum))) /\ ((((exists ff_h_ges_half_sum_successor. ff_h_ges_half_sum_successor + S (ff_s_ges_half_sum) = S ((S (S ff_i_ges_half_sum)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_successor. ff_u_ges_half_sum = ff_q_ges_half_sum_successor * S ((S (S ff_i_ges_half_sum)) * ff_v_ges_half_sum) + (ff_s_ges_half_sum))) /\ ff_s_ges_half_sum = ff_r_ges_half_sum + ff_a_ges_half_sum)))))) -> (exists ff_u_ges_magnitude_sum ff_v_ges_magnitude_sum. ((((exists ff_h_ges_magnitude_sum_start. ff_h_ges_magnitude_sum_start + S (0) = S ((S (0)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_start. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_start * S ((S (0)) * ff_v_ges_magnitude_sum) + (0))) /\ ((((exists ff_h_ges_magnitude_sum_terminal. ff_h_ges_magnitude_sum_terminal + S (M) = S ((S (h)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_terminal. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_terminal * S ((S (h)) * ff_v_ges_magnitude_sum) + (M))) /\ forall ff_i_ges_magnitude_sum. (exists ff_lt_ges_magnitude_sum_bound. ff_lt_ges_magnitude_sum_bound + S ff_i_ges_magnitude_sum = h) -> exists ff_a_ges_magnitude_sum ff_r_ges_magnitude_sum ff_s_ges_magnitude_sum. ((((exists ff_h_ges_magnitude_sum_summand. ff_h_ges_magnitude_sum_summand + S (ff_a_ges_magnitude_sum) = S ((S (ff_i_ges_magnitude_sum)) * mc)) /\ exists ff_q_ges_magnitude_sum_summand. mb = ff_q_ges_magnitude_sum_summand * S ((S (ff_i_ges_magnitude_sum)) * mc) + (ff_a_ges_magnitude_sum))) /\ ((((exists ff_h_ges_magnitude_sum_partial. ff_h_ges_magnitude_sum_partial + S (ff_r_ges_magnitude_sum) = S ((S (ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_partial. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_partial * S ((S (ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum) + (ff_r_ges_magnitude_sum))) /\ ((((exists ff_h_ges_magnitude_sum_successor. ff_h_ges_magnitude_sum_successor + S (ff_s_ges_magnitude_sum) = S ((S (S ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_successor. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_successor * S ((S (S ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum) + (ff_s_ges_magnitude_sum))) /\ ff_s_ges_magnitude_sum = ff_r_ges_magnitude_sum + ff_a_ges_magnitude_sum)))))) -> X = M

Structural proof guide

Generated structural guide

Gauss signed-half data makes the magnitude Sum equal the canonical half Sum.

Use the direct prerequisites gauss_signed_half_magnitude_range, gauss_signed_half_magnitude_injective, gauss_signed_half_predecessor_recode_exists, beta_magnitude_sum_permutation_exact as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (3).

Referenced ingredients

PA0078 gauss_signed_half_magnitude_range PA007C gauss_signed_half_magnitude_injective PA007E gauss_signed_half_predecessor_recode_exists PA00CY beta_magnitude_sum_permutation_exact

Proof neighborhood

Direct dependencies

PA0078 gauss_signed_half_magnitude_range PA007C gauss_signed_half_magnitude_injective PA007E gauss_signed_half_predecessor_recode_exists PA00CY beta_magnitude_sum_permutation_exact

Direct dependents

PA00D3 gauss_eisenstein_terminal_cancel_magnitude_mod_two

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

77 script commands · 11 reading checkpoints · 3 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 (4)
gauss signed half magnitude rangegauss signed half magnitude injectivegauss signed half predecessor recode existsbeta magnitude sum permutation exact

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro mb
  7. L7
    intro mc
  8. L8
    intro sb
  9. L9
    intro sc
  10. L10
    intro X
02Fix variables and assumptionsL11–18

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

  1. L11
    intro M
  2. L12
    intro hp
  3. L13
    intro hprime
  4. L14
    intro hnondiv
  5. L15
    intro hhalf
  6. L16
    intro hsigned
  7. L17
    intro hhalf_sum
  8. L18
    intro hmagnitude_sum
03Establish hrangeL19–28

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

  1. L19
    have hrange : ∀ gmp_index_ges_magnitude_range. Lt(gmp_index_ges_magnitude_range,h) → ∃ x. BetaAt(mb,mc,gmp_index_ges_magnitude_range,x) ∧ (Lt(0,x) ∧ Le(x,h))Definitions: LeLtBetaAt
  2. L20
    specialize gauss_signed_half_magnitude_range p
  3. L21
    specialize gauss_signed_half_magnitude_range h
  4. L22
    specialize gauss_signed_half_magnitude_range a
  5. L23
    specialize gauss_signed_half_magnitude_range b
  6. L24
    specialize gauss_signed_half_magnitude_range c
  7. L25
    specialize gauss_signed_half_magnitude_range mb
  8. L26
    specialize gauss_signed_half_magnitude_range mc
  9. L27
    specialize gauss_signed_half_magnitude_range sb
  10. L28
    specialize gauss_signed_half_magnitude_range sc
04Use earlier factsL29–31

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

  1. L29
    specialize gauss_signed_half_magnitude_range h
  2. L30
    apply gauss_signed_half_magnitude_range
  3. L31
    exact hsigned
05Establish hinjectiveL32–41

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

  1. L32
    have hinjective : InjectivePrefix(mb,mc,h)Definitions: InjectivePrefix
  2. L33
    specialize gauss_signed_half_magnitude_injective p
  3. L34
    specialize gauss_signed_half_magnitude_injective h
  4. L35
    specialize gauss_signed_half_magnitude_injective a
  5. L36
    specialize gauss_signed_half_magnitude_injective b
  6. L37
    specialize gauss_signed_half_magnitude_injective c
  7. L38
    specialize gauss_signed_half_magnitude_injective mb
  8. L39
    specialize gauss_signed_half_magnitude_injective mc
  9. L40
    specialize gauss_signed_half_magnitude_injective sb
  10. L41
    specialize gauss_signed_half_magnitude_injective sc
06Use earlier factsL42–47

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

  1. L42
    apply gauss_signed_half_magnitude_injective
  2. L43
    exact hp
  3. L44
    exact hprime
  4. L45
    exact hnondiv
  5. L46
    exact hhalf
  6. L47
    exact hsigned
07Establish hrecode_existsL48–57

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

  1. L48
    have hrecode_exists : ∃ rb. ∃ rc. ∀ x. ∀ y. Lt(x,h) → BetaAt(mb,mc,x,S y) → BetaAt(rb,rc,x,y)Definitions: LtBetaAt
  2. L49
    specialize gauss_signed_half_predecessor_recode_exists p
  3. L50
    specialize gauss_signed_half_predecessor_recode_exists h
  4. L51
    specialize gauss_signed_half_predecessor_recode_exists a
  5. L52
    specialize gauss_signed_half_predecessor_recode_exists b
  6. L53
    specialize gauss_signed_half_predecessor_recode_exists c
  7. L54
    specialize gauss_signed_half_predecessor_recode_exists mb
  8. L55
    specialize gauss_signed_half_predecessor_recode_exists mc
  9. L56
    specialize gauss_signed_half_predecessor_recode_exists sb
  10. L57
    specialize gauss_signed_half_predecessor_recode_exists sc
08Use earlier factsL58–59

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

  1. L58
    apply gauss_signed_half_predecessor_recode_exists
  2. L59
    exact hsigned
09Separate the logical casesL60–61

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

  1. L60
    cases hrecode_exists
  2. L61
    cases hrecode_exists_witness
10Use earlier factsL62–71

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

  1. L62
    specialize beta_magnitude_sum_permutation_exact b
  2. L63
    specialize beta_magnitude_sum_permutation_exact c
  3. L64
    specialize beta_magnitude_sum_permutation_exact mb
  4. L65
    specialize beta_magnitude_sum_permutation_exact mc
  5. L66
    specialize beta_magnitude_sum_permutation_exact x
  6. L67
    specialize beta_magnitude_sum_permutation_exact x1
  7. L68
    specialize beta_magnitude_sum_permutation_exact h
  8. L69
    specialize beta_magnitude_sum_permutation_exact X
  9. L70
    specialize beta_magnitude_sum_permutation_exact M
  10. L71
    apply beta_magnitude_sum_permutation_exact
11Use earlier factsL72–77

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

  1. L72
    exact hhalf
  2. L73
    exact hrange
  3. L74
    exact hinjective
  4. L75
    exact hrecode_exists_witness_witness
  5. L76
    exact hhalf_sum
  6. L77
    exact hmagnitude_sum

Library-wide reading audit

Original exact command ledger · 77 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro mb
  7. 0007intro mc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010intro X
  11. 0011intro M
  12. 0012intro hp
  13. 0013intro hprime
  14. 0014intro hnondiv
  15. 0015intro hhalf
  16. 0016intro hsigned
  17. 0017intro hhalf_sum
  18. 0018intro hmagnitude_sum
  19. 0019have hrange : forall gmp_index_ges_magnitude_range. (exists gsp_lt_gap_ges_magnitude_range_index_bound. gsp_lt_gap_ges_magnitude_range_index_bound + S gmp_index_ges_magnitude_range = h) -> exists gmp_magnitude_ges_magnitude_range. ((((exists ff_h_gmp_ges_magnitude_range_decoded. ff_h_gmp_ges_magnitude_range_decoded + S (gmp_magnitude_ges_magnitude_range) = S ((S (gmp_index_ges_magnitude_range)) * mc)) /\ exists ff_q_gmp_ges_magnitude_range_decoded. mb = ff_q_gmp_ges_magnitude_range_decoded * S ((S (gmp_index_ges_magnitude_range)) * mc) + (gmp_magnitude_ges_magnitude_range))) /\ ((exists gsp_lt_gap_ges_magnitude_range_positive. gsp_lt_gap_ges_magnitude_range_positive + S 0 = gmp_magnitude_ges_magnitude_range) /\ (exists gsp_le_gap_ges_magnitude_range_bounded. gsp_le_gap_ges_magnitude_range_bounded + gmp_magnitude_ges_magnitude_range = h)))
  20. 0020specialize gauss_signed_half_magnitude_range p
  21. 0021specialize gauss_signed_half_magnitude_range h
  22. 0022specialize gauss_signed_half_magnitude_range a
  23. 0023specialize gauss_signed_half_magnitude_range b
  24. 0024specialize gauss_signed_half_magnitude_range c
  25. 0025specialize gauss_signed_half_magnitude_range mb
  26. 0026specialize gauss_signed_half_magnitude_range mc
  27. 0027specialize gauss_signed_half_magnitude_range sb
  28. 0028specialize gauss_signed_half_magnitude_range sc
  29. 0029specialize gauss_signed_half_magnitude_range h
  30. 0030apply gauss_signed_half_magnitude_range
  31. 0031exact hsigned
  32. 0032have hinjective : forall fp_i_ges_magnitude_injective fp_j_ges_magnitude_injective fp_value_ges_magnitude_injective. (exists fp_gap_ges_magnitude_injective_i. fp_gap_ges_magnitude_injective_i + S fp_i_ges_magnitude_injective = h) -> (exists fp_gap_ges_magnitude_injective_j. fp_gap_ges_magnitude_injective_j + S fp_j_ges_magnitude_injective = h) -> (((exists ff_h_ges_magnitude_injective_left. ff_h_ges_magnitude_injective_left + S (fp_value_ges_magnitude_injective) = S ((S (fp_i_ges_magnitude_injective)) * mc)) /\ exists ff_q_ges_magnitude_injective_left. mb = ff_q_ges_magnitude_injective_left * S ((S (fp_i_ges_magnitude_injective)) * mc) + (fp_value_ges_magnitude_injective))) -> (((exists ff_h_ges_magnitude_injective_right. ff_h_ges_magnitude_injective_right + S (fp_value_ges_magnitude_injective) = S ((S (fp_j_ges_magnitude_injective)) * mc)) /\ exists ff_q_ges_magnitude_injective_right. mb = ff_q_ges_magnitude_injective_right * S ((S (fp_j_ges_magnitude_injective)) * mc) + (fp_value_ges_magnitude_injective))) -> fp_i_ges_magnitude_injective = fp_j_ges_magnitude_injective
  33. 0033specialize gauss_signed_half_magnitude_injective p
  34. 0034specialize gauss_signed_half_magnitude_injective h
  35. 0035specialize gauss_signed_half_magnitude_injective a
  36. 0036specialize gauss_signed_half_magnitude_injective b
  37. 0037specialize gauss_signed_half_magnitude_injective c
  38. 0038specialize gauss_signed_half_magnitude_injective mb
  39. 0039specialize gauss_signed_half_magnitude_injective mc
  40. 0040specialize gauss_signed_half_magnitude_injective sb
  41. 0041specialize gauss_signed_half_magnitude_injective sc
  42. 0042apply gauss_signed_half_magnitude_injective
  43. 0043exact hp
  44. 0044exact hprime
  45. 0045exact hnondiv
  46. 0046exact hhalf
  47. 0047exact hsigned
  48. 0048have hrecode_exists : exists rb rc. (forall gmp_index_ges_recode_exists gmp_predecessor_ges_recode_exists. (exists gsp_lt_gap_ges_recode_exists_index_bound. gsp_lt_gap_ges_recode_exists_index_bound + S gmp_index_ges_recode_exists = h) -> (((exists gsp_beta_height_gmp_ges_recode_exists_source. gsp_beta_height_gmp_ges_recode_exists_source + S (S gmp_predecessor_ges_recode_exists) = S ((S (gmp_index_ges_recode_exists)) * mc)) /\ exists gsp_beta_quotient_gmp_ges_recode_exists_source. mb = gsp_beta_quotient_gmp_ges_recode_exists_source * S ((S (gmp_index_ges_recode_exists)) * mc) + (S gmp_predecessor_ges_recode_exists))) -> (((exists ff_h_gmp_ges_recode_exists_target. ff_h_gmp_ges_recode_exists_target + S (gmp_predecessor_ges_recode_exists) = S ((S (gmp_index_ges_recode_exists)) * rc)) /\ exists ff_q_gmp_ges_recode_exists_target. rb = ff_q_gmp_ges_recode_exists_target * S ((S (gmp_index_ges_recode_exists)) * rc) + (gmp_predecessor_ges_recode_exists))))
  49. 0049specialize gauss_signed_half_predecessor_recode_exists p
  50. 0050specialize gauss_signed_half_predecessor_recode_exists h
  51. 0051specialize gauss_signed_half_predecessor_recode_exists a
  52. 0052specialize gauss_signed_half_predecessor_recode_exists b
  53. 0053specialize gauss_signed_half_predecessor_recode_exists c
  54. 0054specialize gauss_signed_half_predecessor_recode_exists mb
  55. 0055specialize gauss_signed_half_predecessor_recode_exists mc
  56. 0056specialize gauss_signed_half_predecessor_recode_exists sb
  57. 0057specialize gauss_signed_half_predecessor_recode_exists sc
  58. 0058apply gauss_signed_half_predecessor_recode_exists
  59. 0059exact hsigned
  60. 0060cases hrecode_exists
  61. 0061cases hrecode_exists_witness
  62. 0062specialize beta_magnitude_sum_permutation_exact b
  63. 0063specialize beta_magnitude_sum_permutation_exact c
  64. 0064specialize beta_magnitude_sum_permutation_exact mb
  65. 0065specialize beta_magnitude_sum_permutation_exact mc
  66. 0066specialize beta_magnitude_sum_permutation_exact x
  67. 0067specialize beta_magnitude_sum_permutation_exact x1
  68. 0068specialize beta_magnitude_sum_permutation_exact h
  69. 0069specialize beta_magnitude_sum_permutation_exact X
  70. 0070specialize beta_magnitude_sum_permutation_exact M
  71. 0071apply beta_magnitude_sum_permutation_exact
  72. 0072exact hhalf
  73. 0073exact hrange
  74. 0074exact hinjective
  75. 0075exact hrecode_exists_witness_witness
  76. 0076exact hhalf_sum
  77. 0077exact hmagnitude_sum