PA00B8

paired_pair_order_factor_code_exists

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

Package a successor-valued factor code with adjacent unit pairs.

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 n u v b c m. (forall wip_index_wsl_inverse. (exists wip_gap_wsl_inverse_prefix_bound. wip_gap_wsl_inverse_prefix_bound + S wip_index_wsl_inverse = n) -> exists wip_mate_wsl_inverse. ((((exists wip_beta_height_wsl_inverse_decoded. wip_beta_height_wsl_inverse_decoded + S (wip_mate_wsl_inverse) = S ((S (wip_index_wsl_inverse)) * v)) /\ exists wip_beta_quotient_wsl_inverse_decoded. u = wip_beta_quotient_wsl_inverse_decoded * S ((S (wip_index_wsl_inverse)) * v) + (wip_mate_wsl_inverse))) /\ ((exists wip_gap_wsl_inverse_inverse_index_bound. wip_gap_wsl_inverse_inverse_index_bound + S wip_index_wsl_inverse = n) /\ ((exists wip_gap_wsl_inverse_inverse_mate_bound. wip_gap_wsl_inverse_inverse_mate_bound + S wip_mate_wsl_inverse = n) /\ (exists wip_mod_left_wsl_inverse_inverse_mod wip_mod_right_wsl_inverse_inverse_mod. ((S wip_index_wsl_inverse) * S wip_mate_wsl_inverse) + p * wip_mod_left_wsl_inverse_inverse_mod = 1 + p * wip_mod_right_wsl_inverse_inverse_mod))))) -> (forall fom_index_wsl_bounded. (exists fom_gap_wsl_bounded_index_bound. fom_gap_wsl_bounded_index_bound + S (fom_index_wsl_bounded) = m + m) -> exists fom_value_wsl_bounded. ((((exists fom_beta_height_wsl_bounded_entry. fom_beta_height_wsl_bounded_entry + S (fom_value_wsl_bounded) = S ((S (fom_index_wsl_bounded)) * c)) /\ exists fom_beta_quotient_wsl_bounded_entry. b = fom_beta_quotient_wsl_bounded_entry * S ((S (fom_index_wsl_bounded)) * c) + (fom_value_wsl_bounded))) /\ (exists fom_gap_wsl_bounded_value_bound. fom_gap_wsl_bounded_value_bound + S (fom_value_wsl_bounded) = n))) -> (forall wpop_pair_wsl_pairs. (exists wpo_gap_wsl_pairs_pair_bound. wpo_gap_wsl_pairs_pair_bound + S (wpop_pair_wsl_pairs) = m) -> exists wpop_left_wsl_pairs wpop_right_wsl_pairs. ((((exists wpo_beta_height_wsl_pairs_left_entry. wpo_beta_height_wsl_pairs_left_entry + S (wpop_left_wsl_pairs) = S ((S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs)) * c)) /\ exists wpo_beta_quotient_wsl_pairs_left_entry. b = wpo_beta_quotient_wsl_pairs_left_entry * S ((S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs)) * c) + (wpop_left_wsl_pairs))) /\ ((((exists wpo_beta_height_wsl_pairs_right_entry. wpo_beta_height_wsl_pairs_right_entry + S (wpop_right_wsl_pairs) = S ((S (S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs))) * c)) /\ exists wpo_beta_quotient_wsl_pairs_right_entry. b = wpo_beta_quotient_wsl_pairs_right_entry * S ((S (S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs))) * c) + (wpop_right_wsl_pairs))) /\ (((exists wpo_beta_height_wsl_pairs_inverse_entry. wpo_beta_height_wsl_pairs_inverse_entry + S (wpop_right_wsl_pairs) = S ((S (wpop_left_wsl_pairs)) * v)) /\ exists wpo_beta_quotient_wsl_pairs_inverse_entry. u = wpo_beta_quotient_wsl_pairs_inverse_entry * S ((S (wpop_left_wsl_pairs)) * v) + (wpop_right_wsl_pairs)))))) -> (exists f g. ((forall wsl_index_wsl_lift wsl_value_wsl_lift. (exists wpo_gap_wsl_lift_bound. wpo_gap_wsl_lift_bound + S (wsl_index_wsl_lift) = m + m) -> (((exists wpo_beta_height_wsl_lift_source. wpo_beta_height_wsl_lift_source + S (wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * c)) /\ exists wpo_beta_quotient_wsl_lift_source. b = wpo_beta_quotient_wsl_lift_source * S ((S (wsl_index_wsl_lift)) * c) + (wsl_value_wsl_lift))) -> (((exists wpo_beta_height_wsl_lift_target. wpo_beta_height_wsl_lift_target + S (S wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * g)) /\ exists wpo_beta_quotient_wsl_lift_target. f = wpo_beta_quotient_wsl_lift_target * S ((S (wsl_index_wsl_lift)) * g) + (S wsl_value_wsl_lift)))) /\ (forall wpp_pair_wsl_adjacent wpp_left_wsl_adjacent wpp_right_wsl_adjacent. (exists wpp_gap_wsl_adjacent_pair_bound. wpp_gap_wsl_adjacent_pair_bound + S (wpp_pair_wsl_adjacent) = m) -> (((exists wpp_beta_height_wsl_adjacent_left_entry. wpp_beta_height_wsl_adjacent_left_entry + S (wpp_left_wsl_adjacent) = S ((S ((wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g)) /\ exists wpp_beta_quotient_wsl_adjacent_left_entry. f = wpp_beta_quotient_wsl_adjacent_left_entry * S ((S ((wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g) + (wpp_left_wsl_adjacent))) -> (((exists wpp_beta_height_wsl_adjacent_right_entry. wpp_beta_height_wsl_adjacent_right_entry + S (wpp_right_wsl_adjacent) = S ((S (S (wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g)) /\ exists wpp_beta_quotient_wsl_adjacent_right_entry. f = wpp_beta_quotient_wsl_adjacent_right_entry * S ((S (S (wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g) + (wpp_right_wsl_adjacent))) -> (exists wpp_mod_left_wsl_adjacent_pair_mod wpp_mod_right_wsl_adjacent_pair_mod. (wpp_left_wsl_adjacent * wpp_right_wsl_adjacent) + p * wpp_mod_left_wsl_adjacent_pair_mod = (1) + p * wpp_mod_right_wsl_adjacent_pair_mod))))

Structural proof guide

Generated structural guide

Package a successor-valued factor code with adjacent unit pairs.

Use the direct prerequisites pair_order_successor_lift_exists, paired_successor_lift_adjacent_units as previously established PA formulas.

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

Referenced ingredients

PA00B6 pair_order_successor_lift_exists PA00B7 paired_successor_lift_adjacent_units

Proof neighborhood

Direct dependencies

PA00B6 pair_order_successor_lift_exists PA00B7 paired_successor_lift_adjacent_units

Direct dependents

PA00BA paired_pair_order_product_one_exists

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

35 script commands · 7 reading checkpoints · 1 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 (2)
pair order successor lift existspaired successor lift adjacent units

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 n
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro m
  8. L8
    intro hinverse
  9. L9
    intro hbounded
  10. L10
    intro hpairs
02Establish hlift_existsL11–15

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

  1. L11
    have hlift_exists : ∃ f. ∃ g. ∀ x. ∀ y. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(f,g,x,S y)Definitions: LtBetaAt
  2. L12
    specialize pair_order_successor_lift_exists b
  3. L13
    specialize pair_order_successor_lift_exists c
  4. L14
    specialize pair_order_successor_lift_exists m
  5. L15
    exact pair_order_successor_lift_exists
03Separate the logical casesL16–17

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

  1. L16
    cases hlift_exists
  2. L17
    cases hlift_exists_witness
04Construct an explicit witnessL18–19

Supply the displayed value, then prove that it has the required property.

  1. L18
    exists x
  2. L19
    exists x1
05Separate the logical casesL20–20

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

  1. L20
    split
06Use earlier factsL21–30

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

  1. L21
    exact hlift_exists_witness_witness
  2. L22
    specialize paired_successor_lift_adjacent_units p
  3. L23
    specialize paired_successor_lift_adjacent_units n
  4. L24
    specialize paired_successor_lift_adjacent_units u
  5. L25
    specialize paired_successor_lift_adjacent_units v
  6. L26
    specialize paired_successor_lift_adjacent_units b
  7. L27
    specialize paired_successor_lift_adjacent_units c
  8. L28
    specialize paired_successor_lift_adjacent_units x
  9. L29
    specialize paired_successor_lift_adjacent_units x1
  10. L30
    specialize paired_successor_lift_adjacent_units m
07Use earlier factsL31–35

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

  1. L31
    apply paired_successor_lift_adjacent_units
  2. L32
    exact hinverse
  3. L33
    exact hbounded
  4. L34
    exact hpairs
  5. L35
    exact hlift_exists_witness_witness

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro u
  4. 0004intro v
  5. 0005intro b
  6. 0006intro c
  7. 0007intro m
  8. 0008intro hinverse
  9. 0009intro hbounded
  10. 0010intro hpairs
  11. 0011have hlift_exists : exists f g. (forall wsl_index_wsl_lift wsl_value_wsl_lift. (exists wpo_gap_wsl_lift_bound. wpo_gap_wsl_lift_bound + S (wsl_index_wsl_lift) = m + m) -> (((exists wpo_beta_height_wsl_lift_source. wpo_beta_height_wsl_lift_source + S (wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * c)) /\ exists wpo_beta_quotient_wsl_lift_source. b = wpo_beta_quotient_wsl_lift_source * S ((S (wsl_index_wsl_lift)) * c) + (wsl_value_wsl_lift))) -> (((exists wpo_beta_height_wsl_lift_target. wpo_beta_height_wsl_lift_target + S (S wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * g)) /\ exists wpo_beta_quotient_wsl_lift_target. f = wpo_beta_quotient_wsl_lift_target * S ((S (wsl_index_wsl_lift)) * g) + (S wsl_value_wsl_lift))))
  12. 0012specialize pair_order_successor_lift_exists b
  13. 0013specialize pair_order_successor_lift_exists c
  14. 0014specialize pair_order_successor_lift_exists m
  15. 0015exact pair_order_successor_lift_exists
  16. 0016cases hlift_exists
  17. 0017cases hlift_exists_witness
  18. 0018exists x
  19. 0019exists x1
  20. 0020split
  21. 0021exact hlift_exists_witness_witness
  22. 0022specialize paired_successor_lift_adjacent_units p
  23. 0023specialize paired_successor_lift_adjacent_units n
  24. 0024specialize paired_successor_lift_adjacent_units u
  25. 0025specialize paired_successor_lift_adjacent_units v
  26. 0026specialize paired_successor_lift_adjacent_units b
  27. 0027specialize paired_successor_lift_adjacent_units c
  28. 0028specialize paired_successor_lift_adjacent_units x
  29. 0029specialize paired_successor_lift_adjacent_units x1
  30. 0030specialize paired_successor_lift_adjacent_units m
  31. 0031apply paired_successor_lift_adjacent_units
  32. 0032exact hinverse
  33. 0033exact hbounded
  34. 0034exact hpairs
  35. 0035exact hlift_exists_witness_witness