BT00UW

primorial_interval_factor_prefix_shift

Alpha body-checked · checked-use disabled

Align a full Primorial mask with an independent offset interval.

Exact expanded PA statement

forall a b c d e l. (forall bpr_index_bpifps_source. (exists bpr_gap_bpifps_source_bound. bpr_gap_bpifps_source_bound + S (bpr_index_bpifps_source) = a + l) -> exists bpr_value_bpifps_source. ((((exists bpr_height_bpifps_source_decoded. bpr_height_bpifps_source_decoded + S (bpr_value_bpifps_source) = S ((S (bpr_index_bpifps_source)) * c)) /\ exists bpr_quotient_bpifps_source_decoded. b = bpr_quotient_bpifps_source_decoded * S ((S (bpr_index_bpifps_source)) * c) + (bpr_value_bpifps_source))) /\ (((((~(S (bpr_index_bpifps_source) = 1) /\ forall bpr_left_bpifps_source_choice_prime bpr_right_bpifps_source_choice_prime. S (bpr_index_bpifps_source) = bpr_left_bpifps_source_choice_prime * bpr_right_bpifps_source_choice_prime -> bpr_left_bpifps_source_choice_prime = 1 \/ bpr_right_bpifps_source_choice_prime = 1)) /\ bpr_value_bpifps_source = S (bpr_index_bpifps_source)) \/ (~((~(S (bpr_index_bpifps_source) = 1) /\ forall bpr_left_bpifps_source_choice_prime bpr_right_bpifps_source_choice_prime. S (bpr_index_bpifps_source) = bpr_left_bpifps_source_choice_prime * bpr_right_bpifps_source_choice_prime -> bpr_left_bpifps_source_choice_prime = 1 \/ bpr_right_bpifps_source_choice_prime = 1)) /\ bpr_value_bpifps_source = 1))))) -> (forall bpr_index_bpifps_interval. (exists bpr_gap_bpifps_interval_bound. bpr_gap_bpifps_interval_bound + S (bpr_index_bpifps_interval) = l) -> exists bpr_value_bpifps_interval. ((((exists bpr_height_bpifps_interval_decoded. bpr_height_bpifps_interval_decoded + S (bpr_value_bpifps_interval) = S ((S (bpr_index_bpifps_interval)) * e)) /\ exists bpr_quotient_bpifps_interval_decoded. d = bpr_quotient_bpifps_interval_decoded * S ((S (bpr_index_bpifps_interval)) * e) + (bpr_value_bpifps_interval))) /\ (((((~(S (a + bpr_index_bpifps_interval) = 1) /\ forall bpr_left_bpifps_interval_choice_prime bpr_right_bpifps_interval_choice_prime. S (a + bpr_index_bpifps_interval) = bpr_left_bpifps_interval_choice_prime * bpr_right_bpifps_interval_choice_prime -> bpr_left_bpifps_interval_choice_prime = 1 \/ bpr_right_bpifps_interval_choice_prime = 1)) /\ bpr_value_bpifps_interval = S (a + bpr_index_bpifps_interval)) \/ (~((~(S (a + bpr_index_bpifps_interval) = 1) /\ forall bpr_left_bpifps_interval_choice_prime bpr_right_bpifps_interval_choice_prime. S (a + bpr_index_bpifps_interval) = bpr_left_bpifps_interval_choice_prime * bpr_right_bpifps_interval_choice_prime -> bpr_left_bpifps_interval_choice_prime = 1 \/ bpr_right_bpifps_interval_choice_prime = 1)) /\ bpr_value_bpifps_interval = 1))))) -> forall i p. (exists bpr_gap_bpifps_bound. bpr_gap_bpifps_bound + S (i) = l) -> (((exists bpr_height_bpifps_source_entry. bpr_height_bpifps_source_entry + S (p) = S ((S (a + i)) * c)) /\ exists bpr_quotient_bpifps_source_entry. b = bpr_quotient_bpifps_source_entry * S ((S (a + i)) * c) + (p))) -> (((exists bpr_height_bpifps_target_entry. bpr_height_bpifps_target_entry + S (p) = S ((S (i)) * e)) /\ exists bpr_quotient_bpifps_target_entry. d = bpr_quotient_bpifps_target_entry * S ((S (i)) * e) + (p)))

Structural proof guide

Align a full Primorial mask with an independent offset interval.

Direct prerequisites: add_le_add_left, beta_at_unique, primorial_factor_choice_functional. The authored body proceeds by case analysis (4), intermediate claims (8), equality transport (3).

Proof neighborhood

Direct dependencies

BT0015 add_le_add_left BT0042 beta_at_unique BT00U6 primorial_factor_choice_functional

Direct dependents

BT00UY primorial_prefix_interval_split

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro l
  7. 0007intro hsource
  8. 0008intro hinterval
  9. 0009intro i
  10. 0010intro p
  11. 0011intro hi
  12. 0012intro hp
  13. 0013have hsource_bound_raw : exists bpr_gap_bpifps_shifted_bound. bpr_gap_bpifps_shifted_bound + (a + S i) = a + l
  14. 0014specialize add_le_add_left (S i)
  15. 0015specialize add_le_add_left l
  16. 0016specialize add_le_add_left a
  17. 0017apply add_le_add_left
  18. 0018exact hi
  19. 0019have hadd_succ : a + S i = S (a + i)
  20. 0020apply PA4
  21. 0021rewrite hadd_succ at hsource_bound_raw
  22. 0022have hsource_bound : exists bpr_gap_bpifps_source_bound. bpr_gap_bpifps_source_bound + S (a + i) = a + l
  23. 0023exact hsource_bound_raw
  24. 0024have hsource_entry : exists q. ((((exists bpr_height_bpifps_source_local. bpr_height_bpifps_source_local + S (q) = S ((S (a + i)) * c)) /\ exists bpr_quotient_bpifps_source_local. b = bpr_quotient_bpifps_source_local * S ((S (a + i)) * c) + (q))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpifps_source_choice_prime bpr_right_bpifps_source_choice_prime. S (a + i) = bpr_left_bpifps_source_choice_prime * bpr_right_bpifps_source_choice_prime -> bpr_left_bpifps_source_choice_prime = 1 \/ bpr_right_bpifps_source_choice_prime = 1)) /\ q = S (a + i)) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpifps_source_choice_prime bpr_right_bpifps_source_choice_prime. S (a + i) = bpr_left_bpifps_source_choice_prime * bpr_right_bpifps_source_choice_prime -> bpr_left_bpifps_source_choice_prime = 1 \/ bpr_right_bpifps_source_choice_prime = 1)) /\ q = 1))))
  25. 0025apply hsource
  26. 0026exact hsource_bound
  27. 0027cases hsource_entry
  28. 0028cases hsource_entry_witness
  29. 0029have hinterval_entry : exists r. ((((exists bpr_height_bpifps_interval_local. bpr_height_bpifps_interval_local + S (r) = S ((S (i)) * e)) /\ exists bpr_quotient_bpifps_interval_local. d = bpr_quotient_bpifps_interval_local * S ((S (i)) * e) + (r))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpifps_interval_choice_prime bpr_right_bpifps_interval_choice_prime. S (a + i) = bpr_left_bpifps_interval_choice_prime * bpr_right_bpifps_interval_choice_prime -> bpr_left_bpifps_interval_choice_prime = 1 \/ bpr_right_bpifps_interval_choice_prime = 1)) /\ r = S (a + i)) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpifps_interval_choice_prime bpr_right_bpifps_interval_choice_prime. S (a + i) = bpr_left_bpifps_interval_choice_prime * bpr_right_bpifps_interval_choice_prime -> bpr_left_bpifps_interval_choice_prime = 1 \/ bpr_right_bpifps_interval_choice_prime = 1)) /\ r = 1))))
  30. 0030apply hinterval
  31. 0031exact hi
  32. 0032cases hinterval_entry
  33. 0033cases hinterval_entry_witness
  34. 0034have hpq : p = x
  35. 0035apply beta_at_unique
  36. 0036exact hp
  37. 0037exact hsource_entry_witness_left
  38. 0038have hqr : x = x1
  39. 0039apply primorial_factor_choice_functional
  40. 0040exact hsource_entry_witness_right
  41. 0041exact hinterval_entry_witness_right
  42. 0042have hpr : p = x1
  43. 0043trans x
  44. 0044exact hpq
  45. 0045exact hqr
  46. 0046rewrite hpr
  47. 0047rewrite hpr
  48. 0048exact hinterval_entry_witness_left