PA008X · theorem

scaled_pair_order_state_zero

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

Zero codes witness the empty shifted, bounded, injective state.

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

∀ u. ∀ v. ∀ n. ∃ b. ∃ c. (∀ x. ∀ y. ∀ z. Lt(x,0) → BetaAt(b,c,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(b,c,0,z)) ∧ ((∀ x. Lt(x,0) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(b,c,0))

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 PD0025 InjectivePrefix PD0027 ContainsPrefix

8 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall u v n. exists b c. (((forall espo_position_zero_state_closed espo_source_zero_state_closed espo_mate_zero_state_closed. (exists wpo_gap_zero_state_closed_position_bound. wpo_gap_zero_state_closed_position_bound + S (espo_position_zero_state_closed) = 0) -> (((exists wpo_beta_height_zero_state_closed_source_entry. wpo_beta_height_zero_state_closed_source_entry + S (espo_source_zero_state_closed) = S ((S (espo_position_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_zero_state_closed_source_entry. b = wpo_beta_quotient_zero_state_closed_source_entry * S ((S (espo_position_zero_state_closed)) * c) + (espo_source_zero_state_closed))) -> (((exists wpo_beta_height_zero_state_closed_scaled_entry. wpo_beta_height_zero_state_closed_scaled_entry + S (S espo_mate_zero_state_closed) = S ((S (espo_source_zero_state_closed)) * v)) /\ exists wpo_beta_quotient_zero_state_closed_scaled_entry. u = wpo_beta_quotient_zero_state_closed_scaled_entry * S ((S (espo_source_zero_state_closed)) * v) + (S espo_mate_zero_state_closed))) -> exists espo_mate_position_zero_state_closed. ((exists wpo_gap_zero_state_closed_mate_bound. wpo_gap_zero_state_closed_mate_bound + S (espo_mate_position_zero_state_closed) = 0) /\ (((exists wpo_beta_height_zero_state_closed_mate_entry. wpo_beta_height_zero_state_closed_mate_entry + S (espo_mate_zero_state_closed) = S ((S (espo_mate_position_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_zero_state_closed_mate_entry. b = wpo_beta_quotient_zero_state_closed_mate_entry * S ((S (espo_mate_position_zero_state_closed)) * c) + (espo_mate_zero_state_closed))))) /\ (((forall fom_index_zero_state_bounded. (exists fom_gap_zero_state_bounded_index_bound. fom_gap_zero_state_bounded_index_bound + S (fom_index_zero_state_bounded) = 0) -> exists fom_value_zero_state_bounded. ((((exists fom_beta_height_zero_state_bounded_entry. fom_beta_height_zero_state_bounded_entry + S (fom_value_zero_state_bounded) = S ((S (fom_index_zero_state_bounded)) * c)) /\ exists fom_beta_quotient_zero_state_bounded_entry. b = fom_beta_quotient_zero_state_bounded_entry * S ((S (fom_index_zero_state_bounded)) * c) + (fom_value_zero_state_bounded))) /\ (exists fom_gap_zero_state_bounded_value_bound. fom_gap_zero_state_bounded_value_bound + S (fom_value_zero_state_bounded) = n))) /\ (forall wpo_injective_left_zero_state_injective wpo_injective_right_zero_state_injective wpo_injective_value_zero_state_injective. (exists wpo_gap_zero_state_injective_left_bound. wpo_gap_zero_state_injective_left_bound + S (wpo_injective_left_zero_state_injective) = 0) -> (exists wpo_gap_zero_state_injective_right_bound. wpo_gap_zero_state_injective_right_bound + S (wpo_injective_right_zero_state_injective) = 0) -> (((exists wpo_beta_height_zero_state_injective_left_entry. wpo_beta_height_zero_state_injective_left_entry + S (wpo_injective_value_zero_state_injective) = S ((S (wpo_injective_left_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_zero_state_injective_left_entry. b = wpo_beta_quotient_zero_state_injective_left_entry * S ((S (wpo_injective_left_zero_state_injective)) * c) + (wpo_injective_value_zero_state_injective))) -> (((exists wpo_beta_height_zero_state_injective_right_entry. wpo_beta_height_zero_state_injective_right_entry + S (wpo_injective_value_zero_state_injective) = S ((S (wpo_injective_right_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_zero_state_injective_right_entry. b = wpo_beta_quotient_zero_state_injective_right_entry * S ((S (wpo_injective_right_zero_state_injective)) * c) + (wpo_injective_value_zero_state_injective))) -> wpo_injective_left_zero_state_injective = wpo_injective_right_zero_state_injective)))))

Proof neighborhood

Direct theorem prerequisites

PA008U scaled_orbit_closed_prefix_zero PA008V bounded_into_zero PA008W injective_prefix_zero

Direct theorem dependents

PA009V scaled_inverse_pair_order_paired_iteration

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

19 script commands · 6 reading checkpoints · 0 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.

Named ingredients (3)
scaled orbit closed prefix zerobounded into zeroinjective prefix zero
01Fix variables and assumptionsL1–3

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

  1. L1
    intro u
  2. L2
    intro v
  3. L3
    intro n
02Construct an explicit witnessL4–5

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

  1. L4
    exists 0
  2. L5
    exists 0
03Separate the logical casesL6–6

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

  1. L6
    split
04Use earlier factsL7–11

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

  1. L7
    specialize scaled_orbit_closed_prefix_zero u
  2. L8
    specialize scaled_orbit_closed_prefix_zero v
  3. L9
    specialize scaled_orbit_closed_prefix_zero 0
  4. L10
    specialize scaled_orbit_closed_prefix_zero 0
  5. L11
    exact scaled_orbit_closed_prefix_zero
05Separate the logical casesL12–12

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

  1. L12
    split
06Use earlier factsL13–19

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

  1. L13
    specialize bounded_into_zero 0
  2. L14
    specialize bounded_into_zero 0
  3. L15
    specialize bounded_into_zero n
  4. L16
    exact bounded_into_zero
  5. L17
    specialize injective_prefix_zero 0
  6. L18
    specialize injective_prefix_zero 0
  7. L19
    exact injective_prefix_zero

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro u
  2. 0002intro v
  3. 0003intro n
  4. 0004exists 0
  5. 0005exists 0
  6. 0006split
  7. 0007specialize scaled_orbit_closed_prefix_zero u
  8. 0008specialize scaled_orbit_closed_prefix_zero v
  9. 0009specialize scaled_orbit_closed_prefix_zero 0
  10. 0010specialize scaled_orbit_closed_prefix_zero 0
  11. 0011exact scaled_orbit_closed_prefix_zero
  12. 0012split
  13. 0013specialize bounded_into_zero 0
  14. 0014specialize bounded_into_zero 0
  15. 0015specialize bounded_into_zero n
  16. 0016exact bounded_into_zero
  17. 0017specialize injective_prefix_zero 0
  18. 0018specialize injective_prefix_zero 0
  19. 0019exact injective_prefix_zero