PA0098

finite_short_prefix_omits

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

Every beta-coded prefix shorter than n explicitly omits a value below n.

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 n. (exists h. h + S l = n) -> (exists fom_value_short_omit. ((exists fom_gap_short_omit_value_bound. fom_gap_short_omit_value_bound + S (fom_value_short_omit) = n) /\ ~(exists fom_index_short_omit. ((exists fom_gap_short_omit_index_bound. fom_gap_short_omit_index_bound + S (fom_index_short_omit) = l) /\ (((exists fom_beta_height_short_omit_entry. fom_beta_height_short_omit_entry + S (fom_value_short_omit) = S ((S (fom_index_short_omit)) * c)) /\ exists fom_beta_quotient_short_omit_entry. b = fom_beta_quotient_short_omit_entry * S ((S (fom_index_short_omit)) * c) + (fom_value_short_omit)))))))

Structural proof guide

Generated structural guide

Every beta-coded prefix shorter than n explicitly omits a value below n.

Use the direct prerequisites finite_covers_into_or_omits, finite_short_cover_impossible as previously established PA formulas.

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

Referenced ingredients

PA0092 finite_covers_into_or_omits PA0097 finite_short_cover_impossible

Proof neighborhood

Direct dependencies

PA0092 finite_covers_into_or_omits PA0097 finite_short_cover_impossible

Direct dependents

PA009I scaled_inverse_prefix_choose_omitted_orbit PA00AE finite_prefix_choose_unused_nonendpoint

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

21 script commands · 4 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)
finite covers into or omitsfinite short cover impossible

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–5

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 n
  5. L5
    intro hln
02Establish hsearchL6–11

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

  1. L6
    have hsearch : (∀ x. Lt(x,n) → ContainsPrefix(b,c,l,x)) ∨ (∃ x. Lt(x,n) ∧ ¬ContainsPrefix(b,c,l,x))Definitions: LtContainsPrefix
  2. L7
    specialize finite_covers_into_or_omits b
  3. L8
    specialize finite_covers_into_or_omits c
  4. L9
    specialize finite_covers_into_or_omits l
  5. L10
    specialize finite_covers_into_or_omits n
  6. L11
    exact finite_covers_into_or_omits
03Separate the logical casesL12–13

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

  1. L12
    cases hsearch
  2. L13
    exfalso
04Use earlier factsL14–21

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

  1. L14
    specialize finite_short_cover_impossible b
  2. L15
    specialize finite_short_cover_impossible c
  3. L16
    specialize finite_short_cover_impossible l
  4. L17
    specialize finite_short_cover_impossible n
  5. L18
    apply finite_short_cover_impossible
  6. L19
    exact hln
  7. L20
    exact hsearch_left
  8. L21
    exact hsearch_right

Library-wide reading audit

Original exact command ledger · 21 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro hln
  6. 0006have hsearch : ((forall fom_value_short_cover. (exists fom_gap_short_cover_value_bound. fom_gap_short_cover_value_bound + S (fom_value_short_cover) = n) -> exists fom_index_short_cover. ((exists fom_gap_short_cover_index_bound. fom_gap_short_cover_index_bound + S (fom_index_short_cover) = l) /\ (((exists fom_beta_height_short_cover_entry. fom_beta_height_short_cover_entry + S (fom_value_short_cover) = S ((S (fom_index_short_cover)) * c)) /\ exists fom_beta_quotient_short_cover_entry. b = fom_beta_quotient_short_cover_entry * S ((S (fom_index_short_cover)) * c) + (fom_value_short_cover))))) \/ (exists fom_value_short_omit. ((exists fom_gap_short_omit_value_bound. fom_gap_short_omit_value_bound + S (fom_value_short_omit) = n) /\ ~(exists fom_index_short_omit. ((exists fom_gap_short_omit_index_bound. fom_gap_short_omit_index_bound + S (fom_index_short_omit) = l) /\ (((exists fom_beta_height_short_omit_entry. fom_beta_height_short_omit_entry + S (fom_value_short_omit) = S ((S (fom_index_short_omit)) * c)) /\ exists fom_beta_quotient_short_omit_entry. b = fom_beta_quotient_short_omit_entry * S ((S (fom_index_short_omit)) * c) + (fom_value_short_omit))))))))
  7. 0007specialize finite_covers_into_or_omits b
  8. 0008specialize finite_covers_into_or_omits c
  9. 0009specialize finite_covers_into_or_omits l
  10. 0010specialize finite_covers_into_or_omits n
  11. 0011exact finite_covers_into_or_omits
  12. 0012cases hsearch
  13. 0013exfalso
  14. 0014specialize finite_short_cover_impossible b
  15. 0015specialize finite_short_cover_impossible c
  16. 0016specialize finite_short_cover_impossible l
  17. 0017specialize finite_short_cover_impossible n
  18. 0018apply finite_short_cover_impossible
  19. 0019exact hln
  20. 0020exact hsearch_left
  21. 0021exact hsearch_right