PA007Y · theorem

gauss_magnitude_product_eq_half_range

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

A magnitude permutation has exactly the product of the canonical half range.

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

∀ mb. ∀ mc. ∀ rb. ∀ rc. ∀ b. ∀ c. ∀ h. ∀ P. ∀ Q. (∀ 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)) → Range(b,c,1,h) → Product(b,c,h,P) → Product(mb,mc,h,Q) → P = Q

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 PD0014 Product 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 mb mc rb rc b c h P Q. (forall gmp_index_product_magnitude_range. (exists gsp_lt_gap_product_magnitude_range_index_bound. gsp_lt_gap_product_magnitude_range_index_bound + S gmp_index_product_magnitude_range = h) -> exists gmp_magnitude_product_magnitude_range. ((((exists ff_h_gmp_product_magnitude_range_decoded. ff_h_gmp_product_magnitude_range_decoded + S (gmp_magnitude_product_magnitude_range) = S ((S (gmp_index_product_magnitude_range)) * mc)) /\ exists ff_q_gmp_product_magnitude_range_decoded. mb = ff_q_gmp_product_magnitude_range_decoded * S ((S (gmp_index_product_magnitude_range)) * mc) + (gmp_magnitude_product_magnitude_range))) /\ ((exists gsp_lt_gap_product_magnitude_range_positive. gsp_lt_gap_product_magnitude_range_positive + S 0 = gmp_magnitude_product_magnitude_range) /\ (exists gsp_le_gap_product_magnitude_range_bounded. gsp_le_gap_product_magnitude_range_bounded + gmp_magnitude_product_magnitude_range = h)))) -> (forall fp_i_product_magnitude_injective fp_j_product_magnitude_injective fp_value_product_magnitude_injective. (exists fp_gap_product_magnitude_injective_i. fp_gap_product_magnitude_injective_i + S fp_i_product_magnitude_injective = h) -> (exists fp_gap_product_magnitude_injective_j. fp_gap_product_magnitude_injective_j + S fp_j_product_magnitude_injective = h) -> (((exists ff_h_product_magnitude_injective_left. ff_h_product_magnitude_injective_left + S (fp_value_product_magnitude_injective) = S ((S (fp_i_product_magnitude_injective)) * mc)) /\ exists ff_q_product_magnitude_injective_left. mb = ff_q_product_magnitude_injective_left * S ((S (fp_i_product_magnitude_injective)) * mc) + (fp_value_product_magnitude_injective))) -> (((exists ff_h_product_magnitude_injective_right. ff_h_product_magnitude_injective_right + S (fp_value_product_magnitude_injective) = S ((S (fp_j_product_magnitude_injective)) * mc)) /\ exists ff_q_product_magnitude_injective_right. mb = ff_q_product_magnitude_injective_right * S ((S (fp_j_product_magnitude_injective)) * mc) + (fp_value_product_magnitude_injective))) -> fp_i_product_magnitude_injective = fp_j_product_magnitude_injective) -> (forall gmp_index_product_predecessor_recode gmp_predecessor_product_predecessor_recode. (exists gsp_lt_gap_product_predecessor_recode_index_bound. gsp_lt_gap_product_predecessor_recode_index_bound + S gmp_index_product_predecessor_recode = h) -> (((exists gsp_beta_height_gmp_product_predecessor_recode_source. gsp_beta_height_gmp_product_predecessor_recode_source + S (S gmp_predecessor_product_predecessor_recode) = S ((S (gmp_index_product_predecessor_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_product_predecessor_recode_source. mb = gsp_beta_quotient_gmp_product_predecessor_recode_source * S ((S (gmp_index_product_predecessor_recode)) * mc) + (S gmp_predecessor_product_predecessor_recode))) -> (((exists ff_h_gmp_product_predecessor_recode_target. ff_h_gmp_product_predecessor_recode_target + S (gmp_predecessor_product_predecessor_recode) = S ((S (gmp_index_product_predecessor_recode)) * rc)) /\ exists ff_q_gmp_product_predecessor_recode_target. rb = ff_q_gmp_product_predecessor_recode_target * S ((S (gmp_index_product_predecessor_recode)) * rc) + (gmp_predecessor_product_predecessor_recode)))) -> (forall gsp_range_index_product_canonical_half_range. (exists gsp_lt_gap_product_canonical_half_range_range_bound. gsp_lt_gap_product_canonical_half_range_range_bound + S gsp_range_index_product_canonical_half_range = h) -> (((exists gsp_beta_height_product_canonical_half_range_range_entry. gsp_beta_height_product_canonical_half_range_range_entry + S (1 + gsp_range_index_product_canonical_half_range) = S ((S (gsp_range_index_product_canonical_half_range)) * c)) /\ exists gsp_beta_quotient_product_canonical_half_range_range_entry. b = gsp_beta_quotient_product_canonical_half_range_range_entry * S ((S (gsp_range_index_product_canonical_half_range)) * c) + (1 + gsp_range_index_product_canonical_half_range)))) -> (exists ff_u_product_canonical_product ff_v_product_canonical_product. ((((exists ff_h_product_canonical_product_start. ff_h_product_canonical_product_start + S (1) = S ((S (0)) * ff_v_product_canonical_product)) /\ exists ff_q_product_canonical_product_start. ff_u_product_canonical_product = ff_q_product_canonical_product_start * S ((S (0)) * ff_v_product_canonical_product) + (1))) /\ ((((exists ff_h_product_canonical_product_terminal. ff_h_product_canonical_product_terminal + S (P) = S ((S (h)) * ff_v_product_canonical_product)) /\ exists ff_q_product_canonical_product_terminal. ff_u_product_canonical_product = ff_q_product_canonical_product_terminal * S ((S (h)) * ff_v_product_canonical_product) + (P))) /\ forall ff_i_product_canonical_product. (exists ff_lt_product_canonical_product_bound. ff_lt_product_canonical_product_bound + S ff_i_product_canonical_product = h) -> exists ff_p_product_canonical_product ff_r_product_canonical_product ff_s_product_canonical_product. ((((exists ff_h_product_canonical_product_factor. ff_h_product_canonical_product_factor + S (ff_p_product_canonical_product) = S ((S (ff_i_product_canonical_product)) * c)) /\ exists ff_q_product_canonical_product_factor. b = ff_q_product_canonical_product_factor * S ((S (ff_i_product_canonical_product)) * c) + (ff_p_product_canonical_product))) /\ ((((exists ff_h_product_canonical_product_partial. ff_h_product_canonical_product_partial + S (ff_r_product_canonical_product) = S ((S (ff_i_product_canonical_product)) * ff_v_product_canonical_product)) /\ exists ff_q_product_canonical_product_partial. ff_u_product_canonical_product = ff_q_product_canonical_product_partial * S ((S (ff_i_product_canonical_product)) * ff_v_product_canonical_product) + (ff_r_product_canonical_product))) /\ ((((exists ff_h_product_canonical_product_successor. ff_h_product_canonical_product_successor + S (ff_s_product_canonical_product) = S ((S (S ff_i_product_canonical_product)) * ff_v_product_canonical_product)) /\ exists ff_q_product_canonical_product_successor. ff_u_product_canonical_product = ff_q_product_canonical_product_successor * S ((S (S ff_i_product_canonical_product)) * ff_v_product_canonical_product) + (ff_s_product_canonical_product))) /\ ff_s_product_canonical_product = ff_r_product_canonical_product * ff_p_product_canonical_product)))))) -> (exists ff_u_product_magnitude_product ff_v_product_magnitude_product. ((((exists ff_h_product_magnitude_product_start. ff_h_product_magnitude_product_start + S (1) = S ((S (0)) * ff_v_product_magnitude_product)) /\ exists ff_q_product_magnitude_product_start. ff_u_product_magnitude_product = ff_q_product_magnitude_product_start * S ((S (0)) * ff_v_product_magnitude_product) + (1))) /\ ((((exists ff_h_product_magnitude_product_terminal. ff_h_product_magnitude_product_terminal + S (Q) = S ((S (h)) * ff_v_product_magnitude_product)) /\ exists ff_q_product_magnitude_product_terminal. ff_u_product_magnitude_product = ff_q_product_magnitude_product_terminal * S ((S (h)) * ff_v_product_magnitude_product) + (Q))) /\ forall ff_i_product_magnitude_product. (exists ff_lt_product_magnitude_product_bound. ff_lt_product_magnitude_product_bound + S ff_i_product_magnitude_product = h) -> exists ff_p_product_magnitude_product ff_r_product_magnitude_product ff_s_product_magnitude_product. ((((exists ff_h_product_magnitude_product_factor. ff_h_product_magnitude_product_factor + S (ff_p_product_magnitude_product) = S ((S (ff_i_product_magnitude_product)) * mc)) /\ exists ff_q_product_magnitude_product_factor. mb = ff_q_product_magnitude_product_factor * S ((S (ff_i_product_magnitude_product)) * mc) + (ff_p_product_magnitude_product))) /\ ((((exists ff_h_product_magnitude_product_partial. ff_h_product_magnitude_product_partial + S (ff_r_product_magnitude_product) = S ((S (ff_i_product_magnitude_product)) * ff_v_product_magnitude_product)) /\ exists ff_q_product_magnitude_product_partial. ff_u_product_magnitude_product = ff_q_product_magnitude_product_partial * S ((S (ff_i_product_magnitude_product)) * ff_v_product_magnitude_product) + (ff_r_product_magnitude_product))) /\ ((((exists ff_h_product_magnitude_product_successor. ff_h_product_magnitude_product_successor + S (ff_s_product_magnitude_product) = S ((S (S ff_i_product_magnitude_product)) * ff_v_product_magnitude_product)) /\ exists ff_q_product_magnitude_product_successor. ff_u_product_magnitude_product = ff_q_product_magnitude_product_successor * S ((S (S ff_i_product_magnitude_product)) * ff_v_product_magnitude_product) + (ff_s_product_magnitude_product))) /\ ff_s_product_magnitude_product = ff_r_product_magnitude_product * ff_p_product_magnitude_product)))))) -> P = Q

Proof neighborhood

Direct theorem prerequisites

PA007S beta_magnitude_predecessor_recode_bounded PA007U beta_magnitude_predecessor_recode_injective PA007V gauss_predecessor_half_range_aligned PA007X beta_product_permutation_invariant

Direct theorem dependents

PA0080 gauss_signed_products_balance_mod

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 injectivegauss predecessor half range alignedbeta product permutation invariant
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro hmagnitude_injective
  2. L12
    intro hrecode
  3. L13
    intro hhalf
  4. L14
    intro hcanonical_product
  5. L15
    intro hmagnitude_product
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 hinjectiveL25–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 hinjective : 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 hmagnitude_injective
  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 gauss predecessor half range aligned.

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

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

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

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

  1. L55
    specialize beta_product_permutation_invariant Q
  2. L56
    apply beta_product_permutation_invariant
  3. L57
    exact hbounded
  4. L58
    exact hinjective
  5. L59
    exact haligned
  6. L60
    exact hcanonical_product
  7. L61
    exact hmagnitude_product

Library-wide reading audit

Original defined command ledger · 61 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro b
  6. 0006intro c
  7. 0007intro h
  8. 0008intro P
  9. 0009intro Q
  10. 0010intro hrange
  11. 0011intro hmagnitude_injective
  12. 0012intro hrecode
  13. 0013intro hhalf
  14. 0014intro hcanonical_product
  15. 0015intro hmagnitude_product
  16. 0016have hbounded : BoundedPrefix(rb,rc,h)
    Exact native replay linehave hbounded : forall fp_i_product_predecessor_bounded. (exists fp_gap_product_predecessor_bounded_index. fp_gap_product_predecessor_bounded_index + S fp_i_product_predecessor_bounded = h) -> exists fp_value_product_predecessor_bounded. ((((exists ff_h_product_predecessor_bounded_entry. ff_h_product_predecessor_bounded_entry + S (fp_value_product_predecessor_bounded) = S ((S (fp_i_product_predecessor_bounded)) * rc)) /\ exists ff_q_product_predecessor_bounded_entry. rb = ff_q_product_predecessor_bounded_entry * S ((S (fp_i_product_predecessor_bounded)) * rc) + (fp_value_product_predecessor_bounded))) /\ (exists fp_gap_product_predecessor_bounded_value. fp_gap_product_predecessor_bounded_value + S fp_value_product_predecessor_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 hinjective : InjectivePrefix(rb,rc,h)
    Exact native replay linehave hinjective : forall fp_i_product_predecessor_injective fp_j_product_predecessor_injective fp_value_product_predecessor_injective. (exists fp_gap_product_predecessor_injective_i. fp_gap_product_predecessor_injective_i + S fp_i_product_predecessor_injective = h) -> (exists fp_gap_product_predecessor_injective_j. fp_gap_product_predecessor_injective_j + S fp_j_product_predecessor_injective = h) -> (((exists ff_h_product_predecessor_injective_left. ff_h_product_predecessor_injective_left + S (fp_value_product_predecessor_injective) = S ((S (fp_i_product_predecessor_injective)) * rc)) /\ exists ff_q_product_predecessor_injective_left. rb = ff_q_product_predecessor_injective_left * S ((S (fp_i_product_predecessor_injective)) * rc) + (fp_value_product_predecessor_injective))) -> (((exists ff_h_product_predecessor_injective_right. ff_h_product_predecessor_injective_right + S (fp_value_product_predecessor_injective) = S ((S (fp_j_product_predecessor_injective)) * rc)) /\ exists ff_q_product_predecessor_injective_right. rb = ff_q_product_predecessor_injective_right * S ((S (fp_j_product_predecessor_injective)) * rc) + (fp_value_product_predecessor_injective))) -> fp_i_product_predecessor_injective = fp_j_product_predecessor_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 hmagnitude_injective
  34. 0034exact hrecode
  35. 0035have haligned : ∀ fpr_i_product_alignment. ∀ fpr_j_product_alignment. ∀ fpr_x_product_alignment. Lt(fpr_i_product_alignment,h) → BetaAt(rb,rc,fpr_i_product_alignment,fpr_j_product_alignment) → BetaAt(b,c,fpr_j_product_alignment,fpr_x_product_alignment) → BetaAt(mb,mc,fpr_i_product_alignment,fpr_x_product_alignment)
    Exact native replay linehave haligned : forall fpr_i_product_alignment fpr_j_product_alignment fpr_x_product_alignment. (exists fpr_h_product_alignment. fpr_h_product_alignment + S fpr_i_product_alignment = h) -> (((exists ff_h_product_alignment_map. ff_h_product_alignment_map + S (fpr_j_product_alignment) = S ((S (fpr_i_product_alignment)) * rc)) /\ exists ff_q_product_alignment_map. rb = ff_q_product_alignment_map * S ((S (fpr_i_product_alignment)) * rc) + (fpr_j_product_alignment))) -> (((exists ff_h_product_alignment_source. ff_h_product_alignment_source + S (fpr_x_product_alignment) = S ((S (fpr_j_product_alignment)) * c)) /\ exists ff_q_product_alignment_source. b = ff_q_product_alignment_source * S ((S (fpr_j_product_alignment)) * c) + (fpr_x_product_alignment))) -> (((exists ff_h_product_alignment_target. ff_h_product_alignment_target + S (fpr_x_product_alignment) = S ((S (fpr_i_product_alignment)) * mc)) /\ exists ff_q_product_alignment_target. mb = ff_q_product_alignment_target * S ((S (fpr_i_product_alignment)) * mc) + (fpr_x_product_alignment)))
  36. 0036specialize gauss_predecessor_half_range_aligned mb
  37. 0037specialize gauss_predecessor_half_range_aligned mc
  38. 0038specialize gauss_predecessor_half_range_aligned rb
  39. 0039specialize gauss_predecessor_half_range_aligned rc
  40. 0040specialize gauss_predecessor_half_range_aligned b
  41. 0041specialize gauss_predecessor_half_range_aligned c
  42. 0042specialize gauss_predecessor_half_range_aligned h
  43. 0043apply gauss_predecessor_half_range_aligned
  44. 0044exact hrange
  45. 0045exact hrecode
  46. 0046exact hhalf
  47. 0047specialize beta_product_permutation_invariant h
  48. 0048specialize beta_product_permutation_invariant rb
  49. 0049specialize beta_product_permutation_invariant rc
  50. 0050specialize beta_product_permutation_invariant b
  51. 0051specialize beta_product_permutation_invariant c
  52. 0052specialize beta_product_permutation_invariant mb
  53. 0053specialize beta_product_permutation_invariant mc
  54. 0054specialize beta_product_permutation_invariant P
  55. 0055specialize beta_product_permutation_invariant Q
  56. 0056apply beta_product_permutation_invariant
  57. 0057exact hbounded
  58. 0058exact hinjective
  59. 0059exact haligned
  60. 0060exact hcanonical_product
  61. 0061exact hmagnitude_product