PA00CY · theorem

beta_magnitude_sum_permutation_exact

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

A positive magnitude permutation has exactly the canonical half-range 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.

Statement with defined notation

∀ b. ∀ c. ∀ mb. ∀ mc. ∀ rb. ∀ rc. ∀ h. ∀ X. ∀ M. Range(b,c,1,h) → (∀ x. Lt(x,h) → ∃ y. BetaAt(mb,mc,x,y) ∧ (Lt(0,y) ∧ Le(y,h))) → InjectivePrefix(mb,mc,h) → (∀ x. ∀ y. Lt(x,h) → BetaAt(mb,mc,x,S y) → BetaAt(rb,rc,x,y)) → Sum(b,c,h,X) → Sum(mb,mc,h,M) → X = M

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0013 BetaAt PD0015 Sum PD0018 Range PD0025 InjectivePrefix

11 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0024 BoundedPrefix PD0025 InjectivePrefix

6 occurrences

Exact expanded native-PA statement
forall b c mb mc rb rc h X M. (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 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)))) -> (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) -> (forall gmp_index_ges_recode gmp_predecessor_ges_recode. (exists gsp_lt_gap_ges_recode_index_bound. gsp_lt_gap_ges_recode_index_bound + S gmp_index_ges_recode = h) -> (((exists gsp_beta_height_gmp_ges_recode_source. gsp_beta_height_gmp_ges_recode_source + S (S gmp_predecessor_ges_recode) = S ((S (gmp_index_ges_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_ges_recode_source. mb = gsp_beta_quotient_gmp_ges_recode_source * S ((S (gmp_index_ges_recode)) * mc) + (S gmp_predecessor_ges_recode))) -> (((exists ff_h_gmp_ges_recode_target. ff_h_gmp_ges_recode_target + S (gmp_predecessor_ges_recode) = S ((S (gmp_index_ges_recode)) * rc)) /\ exists ff_q_gmp_ges_recode_target. rb = ff_q_gmp_ges_recode_target * S ((S (gmp_index_ges_recode)) * rc) + (gmp_predecessor_ges_recode)))) -> (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

Proof neighborhood

Direct theorem prerequisites

PA007S beta_magnitude_predecessor_recode_bounded PA007U beta_magnitude_predecessor_recode_injective PA00CS beta_magnitude_predecessor_recode_aligned_half_range PA00CX beta_sum_permutation_invariant

Direct theorem dependents

PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

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

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)
beta magnitude predecessor recode boundedbeta magnitude predecessor recode injectivebeta magnitude predecessor recode aligned half rangebeta sum permutation invariant
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro mb
  4. L4
    intro mc
  5. L5
    intro rb
  6. L6
    intro rc
  7. L7
    intro h
  8. L8
    intro X
  9. L9
    intro M
  10. L10
    intro hhalf
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hrange
  2. L12
    intro hinjective
  3. L13
    intro hrecode
  4. L14
    intro hhalf_sum
  5. L15
    intro hmagnitude_sum
03Establish hboundedL16–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode bounded.

  1. L16
    have hbounded : BoundedPrefix(rb,rc,h)Definitions: BoundedPrefix(rb,rc,h)Original native command in the exact edition
  2. L17
    specialize beta_magnitude_predecessor_recode_bounded mb
  3. L18
    specialize beta_magnitude_predecessor_recode_bounded mc
  4. L19
    specialize beta_magnitude_predecessor_recode_bounded rb
  5. L20
    specialize beta_magnitude_predecessor_recode_bounded rc
  6. L21
    specialize beta_magnitude_predecessor_recode_bounded h
  7. L22
    apply beta_magnitude_predecessor_recode_bounded
  8. L23
    exact hrange
  9. L24
    exact hrecode
04Establish hrecode_injectiveL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode injective.

  1. L25
    have hrecode_injective : InjectivePrefix(rb,rc,h)Definitions: InjectivePrefix(rb,rc,h)Original native command in the exact edition
  2. L26
    specialize beta_magnitude_predecessor_recode_injective mb
  3. L27
    specialize beta_magnitude_predecessor_recode_injective mc
  4. L28
    specialize beta_magnitude_predecessor_recode_injective rb
  5. L29
    specialize beta_magnitude_predecessor_recode_injective rc
  6. L30
    specialize beta_magnitude_predecessor_recode_injective h
  7. L31
    apply beta_magnitude_predecessor_recode_injective
  8. L32
    exact hrange
  9. L33
    exact hinjective
  10. L34
    exact hrecode
05Establish halignedL35–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode aligned half range.

  1. L35
    have haligned : ∀ fpr_i_ges_alignment. ∀ fpr_j_ges_alignment. ∀ fpr_x_ges_alignment. Lt(fpr_i_ges_alignment,h) → BetaAt(rb,rc,fpr_i_ges_alignment,fpr_j_ges_alignment) → BetaAt(b,c,fpr_j_ges_alignment,fpr_x_ges_alignment) → BetaAt(mb,mc,fpr_i_ges_alignment,fpr_x_ges_alignment)Definitions: Lt(fpr_i_ges_alignment,h)BetaAt(rb,rc,fpr_i_ges_alignment,fpr_j_ges_alignment)BetaAt(b,c,fpr_j_ges_alignment,fpr_x_ges_alignment)BetaAt(mb,mc,fpr_i_ges_alignment,fpr_x_ges_alignment)Original native command in the exact edition
  2. L36
    specialize beta_magnitude_predecessor_recode_aligned_half_range b
  3. L37
    specialize beta_magnitude_predecessor_recode_aligned_half_range c
  4. L38
    specialize beta_magnitude_predecessor_recode_aligned_half_range mb
  5. L39
    specialize beta_magnitude_predecessor_recode_aligned_half_range mc
  6. L40
    specialize beta_magnitude_predecessor_recode_aligned_half_range rb
  7. L41
    specialize beta_magnitude_predecessor_recode_aligned_half_range rc
  8. L42
    specialize beta_magnitude_predecessor_recode_aligned_half_range h
  9. L43
    apply beta_magnitude_predecessor_recode_aligned_half_range
  10. L44
    exact hhalf
06Use earlier factsL45–54

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

  1. L45
    exact hrange
  2. L46
    exact hrecode
  3. L47
    specialize beta_sum_permutation_invariant h
  4. L48
    specialize beta_sum_permutation_invariant rb
  5. L49
    specialize beta_sum_permutation_invariant rc
  6. L50
    specialize beta_sum_permutation_invariant b
  7. L51
    specialize beta_sum_permutation_invariant c
  8. L52
    specialize beta_sum_permutation_invariant mb
  9. L53
    specialize beta_sum_permutation_invariant mc
  10. L54
    specialize beta_sum_permutation_invariant X
07Use earlier factsL55–61

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

  1. L55
    specialize beta_sum_permutation_invariant M
  2. L56
    apply beta_sum_permutation_invariant
  3. L57
    exact hbounded
  4. L58
    exact hrecode_injective
  5. L59
    exact haligned
  6. L60
    exact hhalf_sum
  7. L61
    exact hmagnitude_sum

Library-wide reading audit

Original defined command ledger · 61 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro mb
  4. 0004intro mc
  5. 0005intro rb
  6. 0006intro rc
  7. 0007intro h
  8. 0008intro X
  9. 0009intro M
  10. 0010intro hhalf
  11. 0011intro hrange
  12. 0012intro hinjective
  13. 0013intro hrecode
  14. 0014intro hhalf_sum
  15. 0015intro hmagnitude_sum
  16. 0016have hbounded : BoundedPrefix(rb,rc,h)
    Exact native replay linehave hbounded : forall fp_i_ges_recode_bounded. (exists fp_gap_ges_recode_bounded_index. fp_gap_ges_recode_bounded_index + S fp_i_ges_recode_bounded = h) -> exists fp_value_ges_recode_bounded. ((((exists ff_h_ges_recode_bounded_entry. ff_h_ges_recode_bounded_entry + S (fp_value_ges_recode_bounded) = S ((S (fp_i_ges_recode_bounded)) * rc)) /\ exists ff_q_ges_recode_bounded_entry. rb = ff_q_ges_recode_bounded_entry * S ((S (fp_i_ges_recode_bounded)) * rc) + (fp_value_ges_recode_bounded))) /\ (exists fp_gap_ges_recode_bounded_value. fp_gap_ges_recode_bounded_value + S fp_value_ges_recode_bounded = h))
  17. 0017specialize beta_magnitude_predecessor_recode_bounded mb
  18. 0018specialize beta_magnitude_predecessor_recode_bounded mc
  19. 0019specialize beta_magnitude_predecessor_recode_bounded rb
  20. 0020specialize beta_magnitude_predecessor_recode_bounded rc
  21. 0021specialize beta_magnitude_predecessor_recode_bounded h
  22. 0022apply beta_magnitude_predecessor_recode_bounded
  23. 0023exact hrange
  24. 0024exact hrecode
  25. 0025have hrecode_injective : InjectivePrefix(rb,rc,h)
    Exact native replay linehave hrecode_injective : forall fp_i_ges_recode_injective fp_j_ges_recode_injective fp_value_ges_recode_injective. (exists fp_gap_ges_recode_injective_i. fp_gap_ges_recode_injective_i + S fp_i_ges_recode_injective = h) -> (exists fp_gap_ges_recode_injective_j. fp_gap_ges_recode_injective_j + S fp_j_ges_recode_injective = h) -> (((exists ff_h_ges_recode_injective_left. ff_h_ges_recode_injective_left + S (fp_value_ges_recode_injective) = S ((S (fp_i_ges_recode_injective)) * rc)) /\ exists ff_q_ges_recode_injective_left. rb = ff_q_ges_recode_injective_left * S ((S (fp_i_ges_recode_injective)) * rc) + (fp_value_ges_recode_injective))) -> (((exists ff_h_ges_recode_injective_right. ff_h_ges_recode_injective_right + S (fp_value_ges_recode_injective) = S ((S (fp_j_ges_recode_injective)) * rc)) /\ exists ff_q_ges_recode_injective_right. rb = ff_q_ges_recode_injective_right * S ((S (fp_j_ges_recode_injective)) * rc) + (fp_value_ges_recode_injective))) -> fp_i_ges_recode_injective = fp_j_ges_recode_injective
  26. 0026specialize beta_magnitude_predecessor_recode_injective mb
  27. 0027specialize beta_magnitude_predecessor_recode_injective mc
  28. 0028specialize beta_magnitude_predecessor_recode_injective rb
  29. 0029specialize beta_magnitude_predecessor_recode_injective rc
  30. 0030specialize beta_magnitude_predecessor_recode_injective h
  31. 0031apply beta_magnitude_predecessor_recode_injective
  32. 0032exact hrange
  33. 0033exact hinjective
  34. 0034exact hrecode
  35. 0035have haligned : ∀ fpr_i_ges_alignment. ∀ fpr_j_ges_alignment. ∀ fpr_x_ges_alignment. Lt(fpr_i_ges_alignment,h) → BetaAt(rb,rc,fpr_i_ges_alignment,fpr_j_ges_alignment) → BetaAt(b,c,fpr_j_ges_alignment,fpr_x_ges_alignment) → BetaAt(mb,mc,fpr_i_ges_alignment,fpr_x_ges_alignment)
    Exact native replay linehave haligned : forall fpr_i_ges_alignment fpr_j_ges_alignment fpr_x_ges_alignment. (exists fpr_h_ges_alignment. fpr_h_ges_alignment + S fpr_i_ges_alignment = h) -> (((exists ff_h_ges_alignment_map. ff_h_ges_alignment_map + S (fpr_j_ges_alignment) = S ((S (fpr_i_ges_alignment)) * rc)) /\ exists ff_q_ges_alignment_map. rb = ff_q_ges_alignment_map * S ((S (fpr_i_ges_alignment)) * rc) + (fpr_j_ges_alignment))) -> (((exists ff_h_ges_alignment_source. ff_h_ges_alignment_source + S (fpr_x_ges_alignment) = S ((S (fpr_j_ges_alignment)) * c)) /\ exists ff_q_ges_alignment_source. b = ff_q_ges_alignment_source * S ((S (fpr_j_ges_alignment)) * c) + (fpr_x_ges_alignment))) -> (((exists ff_h_ges_alignment_target. ff_h_ges_alignment_target + S (fpr_x_ges_alignment) = S ((S (fpr_i_ges_alignment)) * mc)) /\ exists ff_q_ges_alignment_target. mb = ff_q_ges_alignment_target * S ((S (fpr_i_ges_alignment)) * mc) + (fpr_x_ges_alignment)))
  36. 0036specialize beta_magnitude_predecessor_recode_aligned_half_range b
  37. 0037specialize beta_magnitude_predecessor_recode_aligned_half_range c
  38. 0038specialize beta_magnitude_predecessor_recode_aligned_half_range mb
  39. 0039specialize beta_magnitude_predecessor_recode_aligned_half_range mc
  40. 0040specialize beta_magnitude_predecessor_recode_aligned_half_range rb
  41. 0041specialize beta_magnitude_predecessor_recode_aligned_half_range rc
  42. 0042specialize beta_magnitude_predecessor_recode_aligned_half_range h
  43. 0043apply beta_magnitude_predecessor_recode_aligned_half_range
  44. 0044exact hhalf
  45. 0045exact hrange
  46. 0046exact hrecode
  47. 0047specialize beta_sum_permutation_invariant h
  48. 0048specialize beta_sum_permutation_invariant rb
  49. 0049specialize beta_sum_permutation_invariant rc
  50. 0050specialize beta_sum_permutation_invariant b
  51. 0051specialize beta_sum_permutation_invariant c
  52. 0052specialize beta_sum_permutation_invariant mb
  53. 0053specialize beta_sum_permutation_invariant mc
  54. 0054specialize beta_sum_permutation_invariant X
  55. 0055specialize beta_sum_permutation_invariant M
  56. 0056apply beta_sum_permutation_invariant
  57. 0057exact hbounded
  58. 0058exact hrecode_injective
  59. 0059exact haligned
  60. 0060exact hhalf_sum
  61. 0061exact hmagnitude_sum