PA00B3 · theorem

beta_magnitude_predecessor_recode_surjective

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

The predecessor code covers every value 0,...,l-1 by constructive finite pigeonhole.

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

∀ mb. ∀ mc. ∀ rb. ∀ rc. ∀ l. (∀ x. Lt(x,l) → ∃ y. BetaAt(mb,mc,x,y) ∧ (Lt(0,y) ∧ Le(y,l))) → InjectivePrefix(mb,mc,l) → (∀ x. ∀ y. Lt(x,l) → BetaAt(mb,mc,x,S y) → BetaAt(rb,rc,x,y)) → SurjectivePrefix(rb,rc,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

PD0001 Le PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix PD0026 SurjectivePrefix

9 occurrences

In local proof propositions

PD0024 BoundedPrefix PD0025 InjectivePrefix

2 occurrences

Exact expanded native-PA statement
forall mb mc rb rc l. (forall gmp_index_predecessor_transport_finite_range. (exists gsp_lt_gap_predecessor_transport_finite_range_index_bound. gsp_lt_gap_predecessor_transport_finite_range_index_bound + S gmp_index_predecessor_transport_finite_range = l) -> exists gmp_magnitude_predecessor_transport_finite_range. ((((exists ff_h_gmp_predecessor_transport_finite_range_decoded. ff_h_gmp_predecessor_transport_finite_range_decoded + S (gmp_magnitude_predecessor_transport_finite_range) = S ((S (gmp_index_predecessor_transport_finite_range)) * mc)) /\ exists ff_q_gmp_predecessor_transport_finite_range_decoded. mb = ff_q_gmp_predecessor_transport_finite_range_decoded * S ((S (gmp_index_predecessor_transport_finite_range)) * mc) + (gmp_magnitude_predecessor_transport_finite_range))) /\ ((exists gsp_lt_gap_predecessor_transport_finite_range_positive. gsp_lt_gap_predecessor_transport_finite_range_positive + S 0 = gmp_magnitude_predecessor_transport_finite_range) /\ (exists gsp_le_gap_predecessor_transport_finite_range_bounded. gsp_le_gap_predecessor_transport_finite_range_bounded + gmp_magnitude_predecessor_transport_finite_range = l)))) -> (forall fp_i_predecessor_transport_magnitude_injective fp_j_predecessor_transport_magnitude_injective fp_value_predecessor_transport_magnitude_injective. (exists fp_gap_predecessor_transport_magnitude_injective_i. fp_gap_predecessor_transport_magnitude_injective_i + S fp_i_predecessor_transport_magnitude_injective = l) -> (exists fp_gap_predecessor_transport_magnitude_injective_j. fp_gap_predecessor_transport_magnitude_injective_j + S fp_j_predecessor_transport_magnitude_injective = l) -> (((exists ff_h_predecessor_transport_magnitude_injective_left. ff_h_predecessor_transport_magnitude_injective_left + S (fp_value_predecessor_transport_magnitude_injective) = S ((S (fp_i_predecessor_transport_magnitude_injective)) * mc)) /\ exists ff_q_predecessor_transport_magnitude_injective_left. mb = ff_q_predecessor_transport_magnitude_injective_left * S ((S (fp_i_predecessor_transport_magnitude_injective)) * mc) + (fp_value_predecessor_transport_magnitude_injective))) -> (((exists ff_h_predecessor_transport_magnitude_injective_right. ff_h_predecessor_transport_magnitude_injective_right + S (fp_value_predecessor_transport_magnitude_injective) = S ((S (fp_j_predecessor_transport_magnitude_injective)) * mc)) /\ exists ff_q_predecessor_transport_magnitude_injective_right. mb = ff_q_predecessor_transport_magnitude_injective_right * S ((S (fp_j_predecessor_transport_magnitude_injective)) * mc) + (fp_value_predecessor_transport_magnitude_injective))) -> fp_i_predecessor_transport_magnitude_injective = fp_j_predecessor_transport_magnitude_injective) -> (forall gmp_index_predecessor_transport_recode gmp_predecessor_predecessor_transport_recode. (exists gsp_lt_gap_predecessor_transport_recode_index_bound. gsp_lt_gap_predecessor_transport_recode_index_bound + S gmp_index_predecessor_transport_recode = l) -> (((exists gsp_beta_height_gmp_predecessor_transport_recode_source. gsp_beta_height_gmp_predecessor_transport_recode_source + S (S gmp_predecessor_predecessor_transport_recode) = S ((S (gmp_index_predecessor_transport_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_predecessor_transport_recode_source. mb = gsp_beta_quotient_gmp_predecessor_transport_recode_source * S ((S (gmp_index_predecessor_transport_recode)) * mc) + (S gmp_predecessor_predecessor_transport_recode))) -> (((exists ff_h_gmp_predecessor_transport_recode_target. ff_h_gmp_predecessor_transport_recode_target + S (gmp_predecessor_predecessor_transport_recode) = S ((S (gmp_index_predecessor_transport_recode)) * rc)) /\ exists ff_q_gmp_predecessor_transport_recode_target. rb = ff_q_gmp_predecessor_transport_recode_target * S ((S (gmp_index_predecessor_transport_recode)) * rc) + (gmp_predecessor_predecessor_transport_recode)))) -> (forall fp_value_predecessor_transport_target_surjective. (exists fp_gap_predecessor_transport_target_surjective_value. fp_gap_predecessor_transport_target_surjective_value + S fp_value_predecessor_transport_target_surjective = l) -> exists fp_i_predecessor_transport_target_surjective. ((exists fp_gap_predecessor_transport_target_surjective_index. fp_gap_predecessor_transport_target_surjective_index + S fp_i_predecessor_transport_target_surjective = l) /\ (((exists ff_h_predecessor_transport_target_surjective_entry. ff_h_predecessor_transport_target_surjective_entry + S (fp_value_predecessor_transport_target_surjective) = S ((S (fp_i_predecessor_transport_target_surjective)) * rc)) /\ exists ff_q_predecessor_transport_target_surjective_entry. rb = ff_q_predecessor_transport_target_surjective_entry * S ((S (fp_i_predecessor_transport_target_surjective)) * rc) + (fp_value_predecessor_transport_target_surjective)))))

Proof neighborhood

Direct theorem prerequisites

PA007S beta_magnitude_predecessor_recode_bounded PA007U beta_magnitude_predecessor_recode_injective PA004W finite_bounded_injective_surjective

Direct theorem dependents

PA00B4 finite_bounded_nonendpoint_injective_coverage

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

33 script commands · 4 reading checkpoints · 2 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)
beta magnitude predecessor recode boundedbeta magnitude predecessor recode injectivefinite bounded injective surjective
01Fix variables and assumptionsL1–8

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

  1. L1
    intro mb
  2. L2
    intro mc
  3. L3
    intro rb
  4. L4
    intro rc
  5. L5
    intro l
  6. L6
    intro hrange
  7. L7
    intro hsource_injective
  8. L8
    intro hrecode
02Establish hboundedL9–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode bounded.

  1. L9
    have hbounded : BoundedPrefix(rb,rc,l)Definitions: BoundedPrefix(rb,rc,l)Original native command in the exact edition
  2. L10
    specialize beta_magnitude_predecessor_recode_bounded mb
  3. L11
    specialize beta_magnitude_predecessor_recode_bounded mc
  4. L12
    specialize beta_magnitude_predecessor_recode_bounded rb
  5. L13
    specialize beta_magnitude_predecessor_recode_bounded rc
  6. L14
    specialize beta_magnitude_predecessor_recode_bounded l
  7. L15
    apply beta_magnitude_predecessor_recode_bounded
  8. L16
    exact hrange
  9. L17
    exact hrecode
03Establish hinjectiveL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode injective.

  1. L18
    have hinjective : InjectivePrefix(rb,rc,l)Definitions: InjectivePrefix(rb,rc,l)Original native command in the exact edition
  2. L19
    specialize beta_magnitude_predecessor_recode_injective mb
  3. L20
    specialize beta_magnitude_predecessor_recode_injective mc
  4. L21
    specialize beta_magnitude_predecessor_recode_injective rb
  5. L22
    specialize beta_magnitude_predecessor_recode_injective rc
  6. L23
    specialize beta_magnitude_predecessor_recode_injective l
  7. L24
    apply beta_magnitude_predecessor_recode_injective
  8. L25
    exact hrange
  9. L26
    exact hsource_injective
  10. L27
    exact hrecode
04Use earlier factsL28–33

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

  1. L28
    specialize finite_bounded_injective_surjective l
  2. L29
    specialize finite_bounded_injective_surjective rb
  3. L30
    specialize finite_bounded_injective_surjective rc
  4. L31
    apply finite_bounded_injective_surjective
  5. L32
    exact hbounded
  6. L33
    exact hinjective

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro l
  6. 0006intro hrange
  7. 0007intro hsource_injective
  8. 0008intro hrecode
  9. 0009have hbounded : BoundedPrefix(rb,rc,l)
    Exact native replay linehave hbounded : forall fp_i_predecessor_transport_bounded_result. (exists fp_gap_predecessor_transport_bounded_result_index. fp_gap_predecessor_transport_bounded_result_index + S fp_i_predecessor_transport_bounded_result = l) -> exists fp_value_predecessor_transport_bounded_result. ((((exists ff_h_predecessor_transport_bounded_result_entry. ff_h_predecessor_transport_bounded_result_entry + S (fp_value_predecessor_transport_bounded_result) = S ((S (fp_i_predecessor_transport_bounded_result)) * rc)) /\ exists ff_q_predecessor_transport_bounded_result_entry. rb = ff_q_predecessor_transport_bounded_result_entry * S ((S (fp_i_predecessor_transport_bounded_result)) * rc) + (fp_value_predecessor_transport_bounded_result))) /\ (exists fp_gap_predecessor_transport_bounded_result_value. fp_gap_predecessor_transport_bounded_result_value + S fp_value_predecessor_transport_bounded_result = l))
  10. 0010specialize beta_magnitude_predecessor_recode_bounded mb
  11. 0011specialize beta_magnitude_predecessor_recode_bounded mc
  12. 0012specialize beta_magnitude_predecessor_recode_bounded rb
  13. 0013specialize beta_magnitude_predecessor_recode_bounded rc
  14. 0014specialize beta_magnitude_predecessor_recode_bounded l
  15. 0015apply beta_magnitude_predecessor_recode_bounded
  16. 0016exact hrange
  17. 0017exact hrecode
  18. 0018have hinjective : InjectivePrefix(rb,rc,l)
    Exact native replay linehave hinjective : forall fp_i_predecessor_transport_target_injective fp_j_predecessor_transport_target_injective fp_value_predecessor_transport_target_injective. (exists fp_gap_predecessor_transport_target_injective_i. fp_gap_predecessor_transport_target_injective_i + S fp_i_predecessor_transport_target_injective = l) -> (exists fp_gap_predecessor_transport_target_injective_j. fp_gap_predecessor_transport_target_injective_j + S fp_j_predecessor_transport_target_injective = l) -> (((exists ff_h_predecessor_transport_target_injective_left. ff_h_predecessor_transport_target_injective_left + S (fp_value_predecessor_transport_target_injective) = S ((S (fp_i_predecessor_transport_target_injective)) * rc)) /\ exists ff_q_predecessor_transport_target_injective_left. rb = ff_q_predecessor_transport_target_injective_left * S ((S (fp_i_predecessor_transport_target_injective)) * rc) + (fp_value_predecessor_transport_target_injective))) -> (((exists ff_h_predecessor_transport_target_injective_right. ff_h_predecessor_transport_target_injective_right + S (fp_value_predecessor_transport_target_injective) = S ((S (fp_j_predecessor_transport_target_injective)) * rc)) /\ exists ff_q_predecessor_transport_target_injective_right. rb = ff_q_predecessor_transport_target_injective_right * S ((S (fp_j_predecessor_transport_target_injective)) * rc) + (fp_value_predecessor_transport_target_injective))) -> fp_i_predecessor_transport_target_injective = fp_j_predecessor_transport_target_injective
  19. 0019specialize beta_magnitude_predecessor_recode_injective mb
  20. 0020specialize beta_magnitude_predecessor_recode_injective mc
  21. 0021specialize beta_magnitude_predecessor_recode_injective rb
  22. 0022specialize beta_magnitude_predecessor_recode_injective rc
  23. 0023specialize beta_magnitude_predecessor_recode_injective l
  24. 0024apply beta_magnitude_predecessor_recode_injective
  25. 0025exact hrange
  26. 0026exact hsource_injective
  27. 0027exact hrecode
  28. 0028specialize finite_bounded_injective_surjective l
  29. 0029specialize finite_bounded_injective_surjective rb
  30. 0030specialize finite_bounded_injective_surjective rc
  31. 0031apply finite_bounded_injective_surjective
  32. 0032exact hbounded
  33. 0033exact hinjective