PA0095 · theorem

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.

Statement with defined notation

∀ b. ∀ c. ∀ l. ∀ z. ∀ d. ∀ n. (∀ x. Lt(x,n) → ∃ y. BetaAt(z,d,x,y) ∧ (Lt(y,l) ∧ BetaAt(b,c,y,x))) → ∀ x. Lt(x,n) → ∃ y. BetaAt(z,d,x,y) ∧ Lt(y,l)

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

PD0002 Lt PD0013 BetaAt

7 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

3 occurrences

Exact expanded native-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)))

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

PA0097 finite_short_cover_impossible

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ∃ i. BetaAt(z,d,y,i) ∧ (Lt(i,l) ∧ BetaAt(b,c,i,y))Definitions: BetaAt(z,d,y,i)Lt(i,l)BetaAt(b,c,i,y)Original native command in the exact edition
  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 defined 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 : ∃ i. BetaAt(z,d,y,i) ∧ (Lt(i,l) ∧ BetaAt(b,c,i,y))
    Exact native replay linehave 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