PA0095

finite_inverse_choice_bounded_into

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

Every inverse-choice prefix is bounded into the source domain.

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 b c l z d n. (forall fom_value_bounded_choice. (exists fom_gap_bounded_choice_value_bound. fom_gap_bounded_choice_value_bound + S (fom_value_bounded_choice) = n) -> exists fom_index_bounded_choice. ((((exists fom_beta_height_bounded_choice_choice_entry. fom_beta_height_bounded_choice_choice_entry + S (fom_index_bounded_choice) = S ((S (fom_value_bounded_choice)) * d)) /\ exists fom_beta_quotient_bounded_choice_choice_entry. z = fom_beta_quotient_bounded_choice_choice_entry * S ((S (fom_value_bounded_choice)) * d) + (fom_index_bounded_choice))) /\ ((exists fom_gap_bounded_choice_index_bound. fom_gap_bounded_choice_index_bound + S (fom_index_bounded_choice) = l) /\ (((exists fom_beta_height_bounded_choice_source_entry. fom_beta_height_bounded_choice_source_entry + S (fom_value_bounded_choice) = S ((S (fom_index_bounded_choice)) * c)) /\ exists fom_beta_quotient_bounded_choice_source_entry. b = fom_beta_quotient_bounded_choice_source_entry * S ((S (fom_index_bounded_choice)) * c) + (fom_value_bounded_choice)))))) -> (forall fom_index_bounded_result. (exists fom_gap_bounded_result_index_bound. fom_gap_bounded_result_index_bound + S (fom_index_bounded_result) = n) -> exists fom_value_bounded_result. ((((exists fom_beta_height_bounded_result_entry. fom_beta_height_bounded_result_entry + S (fom_value_bounded_result) = S ((S (fom_index_bounded_result)) * d)) /\ exists fom_beta_quotient_bounded_result_entry. z = fom_beta_quotient_bounded_result_entry * S ((S (fom_index_bounded_result)) * d) + (fom_value_bounded_result))) /\ (exists fom_gap_bounded_result_value_bound. fom_gap_bounded_result_value_bound + S (fom_value_bounded_result) = l)))

Structural proof guide

Generated structural guide

Every inverse-choice prefix is bounded into the source domain.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

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

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA0097 finite_short_cover_impossible

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

20 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.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro z
  5. L5
    intro d
  6. L6
    intro n
  7. L7
    intro hchoice
  8. L8
    intro y
  9. L9
    intro hy
02Use earlier factsL10–10

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

  1. L10
    specialize hchoice y
03Establish hstoredL11–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hchoice.

  1. L11
    have hstored : exists i. (((exists h. h + S i = S ((S y) * d)) /\ exists q. z = q * S ((S y) * d) + i) /\ ((exists h. h + S i = l) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y)))
  2. L12
    apply hchoice
  3. L13
    exact hy
04Separate the logical casesL14–16

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

  1. L14
    cases hstored
  2. L15
    cases hstored_witness
  3. L16
    cases hstored_witness_right
05Construct an explicit witnessL17–17

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

  1. L17
    exists x
06Separate the logical casesL18–18

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

  1. L18
    split
07Use earlier factsL19–20

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

  1. L19
    exact hstored_witness_left
  2. L20
    exact hstored_witness_right_left

Library-wide reading audit

Original exact command ledger · 20 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro z
  5. 0005intro d
  6. 0006intro n
  7. 0007intro hchoice
  8. 0008intro y
  9. 0009intro hy
  10. 0010specialize hchoice y
  11. 0011have hstored : exists i. (((exists h. h + S i = S ((S y) * d)) /\ exists q. z = q * S ((S y) * d) + i) /\ ((exists h. h + S i = l) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y)))
  12. 0012apply hchoice
  13. 0013exact hy
  14. 0014cases hstored
  15. 0015cases hstored_witness
  16. 0016cases hstored_witness_right
  17. 0017exists x
  18. 0018split
  19. 0019exact hstored_witness_left
  20. 0020exact hstored_witness_right_left