FS0014 · theorem body

four_square_cross_covered_prefix_bounded

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

A genuinely covered interleaving of two bounded decoded beta prefixes remains bounded in their common finite codomain.

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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. ∀ d. ∀ e. ∀ z. ∀ t. ∀ l. ∀ p. (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,p)) → (∀ x. Lt(x,l) → ∃ y. BetaAt(d,e,x,y) ∧ Lt(y,p)) → (∀ x. ∀ y. Lt(x,l + l) → BetaAt(z,t,x,y) → (∃ n. Lt(n,l) ∧ (BetaAt(b,c,n,y) ∧ x = n + n)) ∨ (∃ n. Lt(n,l) ∧ (BetaAt(d,e,n,y) ∧ x = S (n + n)))) → ∀ x. Lt(x,l + l) → ∃ y. BetaAt(z,t,x,y) ∧ Lt(y,p)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt

In local proof propositions

PD0002 Lt PD0013 BetaAt
Exact expanded first-order statement
forall b c d e z t l p. (forall fscp_index_left. (exists fscp_gap_left_index. fscp_gap_left_index + S (fscp_index_left) = (l)) -> exists fscp_value_left. ((((exists ff_h_fscp_left_entry. ff_h_fscp_left_entry + S (fscp_value_left) = S ((S (fscp_index_left)) * c)) /\ exists ff_q_fscp_left_entry. b = ff_q_fscp_left_entry * S ((S (fscp_index_left)) * c) + (fscp_value_left))) /\ (exists fscp_gap_left_value. fscp_gap_left_value + S (fscp_value_left) = (p)))) -> (forall fscp_index_right. (exists fscp_gap_right_index. fscp_gap_right_index + S (fscp_index_right) = (l)) -> exists fscp_value_right. ((((exists ff_h_fscp_right_entry. ff_h_fscp_right_entry + S (fscp_value_right) = S ((S (fscp_index_right)) * e)) /\ exists ff_q_fscp_right_entry. d = ff_q_fscp_right_entry * S ((S (fscp_index_right)) * e) + (fscp_value_right))) /\ (exists fscp_gap_right_value. fscp_gap_right_value + S (fscp_value_right) = (p)))) -> (forall fscp_index_merged fscp_value_merged. (exists fscp_gap_merged_index. fscp_gap_merged_index + S (fscp_index_merged) = (l + l)) -> (((exists ff_h_fscp_merged_source. ff_h_fscp_merged_source + S (fscp_value_merged) = S ((S (fscp_index_merged)) * t)) /\ exists ff_q_fscp_merged_source. z = ff_q_fscp_merged_source * S ((S (fscp_index_merged)) * t) + (fscp_value_merged))) -> (((exists fscp_left_merged. ((exists fscp_gap_merged_left_bound. fscp_gap_merged_left_bound + S (fscp_left_merged) = (l)) /\ ((((exists ff_h_fscp_merged_left. ff_h_fscp_merged_left + S (fscp_value_merged) = S ((S (fscp_left_merged)) * c)) /\ exists ff_q_fscp_merged_left. b = ff_q_fscp_merged_left * S ((S (fscp_left_merged)) * c) + (fscp_value_merged))) /\ fscp_index_merged = fscp_left_merged + fscp_left_merged))) \/ (exists fscp_right_merged. ((exists fscp_gap_merged_right_bound. fscp_gap_merged_right_bound + S (fscp_right_merged) = (l)) /\ ((((exists ff_h_fscp_merged_right. ff_h_fscp_merged_right + S (fscp_value_merged) = S ((S (fscp_right_merged)) * e)) /\ exists ff_q_fscp_merged_right. d = ff_q_fscp_merged_right * S ((S (fscp_right_merged)) * e) + (fscp_value_merged))) /\ fscp_index_merged = S (fscp_right_merged + fscp_right_merged))))))) -> (forall fscp_index_merged. (exists fscp_gap_merged_index. fscp_gap_merged_index + S (fscp_index_merged) = (l + l)) -> exists fscp_value_merged. ((((exists ff_h_fscp_merged_entry. ff_h_fscp_merged_entry + S (fscp_value_merged) = S ((S (fscp_index_merged)) * t)) /\ exists ff_q_fscp_merged_entry. z = ff_q_fscp_merged_entry * S ((S (fscp_index_merged)) * t) + (fscp_value_merged))) /\ (exists fscp_gap_merged_value. fscp_gap_merged_value + S (fscp_value_merged) = (p))))

Proof neighborhood

Direct theorem prerequisites

beta_at_exists · Stable closed beta_at_unique · Stable closed

Direct theorem dependents

FS0015 four_square_cross_pigeonhole

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

69 script commands · 23 reading checkpoints · 6 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–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro z
  6. L6
    intro t
  7. L7
    intro l
  8. L8
    intro p
  9. L9
    intro hleft
  10. L10
    intro hright
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hcover
  2. L12
    intro i
  3. L13
    intro hibound
03Establish hvalueL14–15

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

  1. L14
    have hvalue : ∃ v. BetaAt(z,t,i,v)Definitions: BetaAt(z,t,i,v)Original native command in the exact edition
  2. L15
    apply beta_at_exists
04Separate the logical casesL16–16

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

  1. L16
    cases hvalue
05Establish hcaseL17–22

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

  1. L17
    have hcase : (∃ y. Lt(y,l) ∧ (BetaAt(b,c,y,x) ∧ i = y + y)) ∨ (∃ y. Lt(y,l) ∧ (BetaAt(d,e,y,x) ∧ i = S (y + y)))Definitions: Lt(y,l)BetaAt(b,c,y,x)BetaAt(d,e,y,x)Original native command in the exact edition
  2. L18
    specialize hcover i
  3. L19
    specialize hcover x
  4. L20
    apply hcover
  5. L21
    exact hibound
  6. L22
    exact hvalue_witness
06Separate the logical casesL23–26

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

  1. L23
    cases hcase
  2. L24
    cases hcase_left
  3. L25
    cases hcase_left_witness
  4. L26
    cases hcase_left_witness_right
07Establish hboundL27–30

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

  1. L27
    have hbound : ∃ v. BetaAt(b,c,x1,v) ∧ Lt(v,p)Definitions: BetaAt(b,c,x1,v)Lt(v,p)Original native command in the exact edition
  2. L28
    specialize hleft x1
  3. L29
    apply hleft
  4. L30
    exact hcase_left_witness_left
08Separate the logical casesL31–32

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

  1. L31
    cases hbound
  2. L32
    cases hbound_witness
09Establish hequalL33–41

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

  1. L33
    have hequal : x = x2
  2. L34
    specialize beta_at_unique b
  3. L35
    specialize beta_at_unique c
  4. L36
    specialize beta_at_unique x1
  5. L37
    specialize beta_at_unique x
  6. L38
    specialize beta_at_unique x2
  7. L39
    apply beta_at_unique
  8. L40
    exact hcase_left_witness_right_left
  9. L41
    exact hbound_witness_left
10Construct an explicit witnessL42–42

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

  1. L42
    exists x
11Separate the logical casesL43–43

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

  1. L43
    split
12Use earlier factsL44–44

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

  1. L44
    exact hvalue_witness
13Calculate and transport equalitiesL45–45

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L45
    rewrite hequal
14Use earlier factsL46–46

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

  1. L46
    exact hbound_witness_right
15Separate the logical casesL47–49

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

  1. L47
    cases hcase_right
  2. L48
    cases hcase_right_witness
  3. L49
    cases hcase_right_witness_right
16Establish hboundL50–53

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

  1. L50
    have hbound : ∃ v. BetaAt(d,e,x1,v) ∧ Lt(v,p)Definitions: BetaAt(d,e,x1,v)Lt(v,p)Original native command in the exact edition
  2. L51
    specialize hright x1
  3. L52
    apply hright
  4. L53
    exact hcase_right_witness_left
17Separate the logical casesL54–55

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

  1. L54
    cases hbound
  2. L55
    cases hbound_witness
18Establish hequalL56–64

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

  1. L56
    have hequal : x = x2
  2. L57
    specialize beta_at_unique d
  3. L58
    specialize beta_at_unique e
  4. L59
    specialize beta_at_unique x1
  5. L60
    specialize beta_at_unique x
  6. L61
    specialize beta_at_unique x2
  7. L62
    apply beta_at_unique
  8. L63
    exact hcase_right_witness_right_left
  9. L64
    exact hbound_witness_left
19Construct an explicit witnessL65–65

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

  1. L65
    exists x
20Separate the logical casesL66–66

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

  1. L66
    split
21Use earlier factsL67–67

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

  1. L67
    exact hvalue_witness
22Calculate and transport equalitiesL68–68

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L68
    rewrite hequal
23Use earlier factsL69–69

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

  1. L69
    exact hbound_witness_right

Library-wide reading audit

Original defined command ledger · 69 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro z
  6. 0006intro t
  7. 0007intro l
  8. 0008intro p
  9. 0009intro hleft
  10. 0010intro hright
  11. 0011intro hcover
  12. 0012intro i
  13. 0013intro hibound
  14. 0014have hvalue : ∃ v. BetaAt(z,t,i,v)
    Exact native replay linehave hvalue : exists v. ((exists ff_h_fscp_bounded_value. ff_h_fscp_bounded_value + S (v) = S ((S (i)) * t)) /\ exists ff_q_fscp_bounded_value. z = ff_q_fscp_bounded_value * S ((S (i)) * t) + (v))
  15. 0015apply beta_at_exists
  16. 0016cases hvalue
  17. 0017have hcase : (∃ y. Lt(y,l) ∧ (BetaAt(b,c,y,x) ∧ i = y + y)) ∨ (∃ y. Lt(y,l) ∧ (BetaAt(d,e,y,x) ∧ i = S (y + y)))
    Exact native replay linehave hcase : ((exists fscp_left_bounded_case. ((exists fscp_gap_bounded_case_left_bound. fscp_gap_bounded_case_left_bound + S (fscp_left_bounded_case) = (l)) /\ ((((exists ff_h_fscp_bounded_case_left. ff_h_fscp_bounded_case_left + S (x) = S ((S (fscp_left_bounded_case)) * c)) /\ exists ff_q_fscp_bounded_case_left. b = ff_q_fscp_bounded_case_left * S ((S (fscp_left_bounded_case)) * c) + (x))) /\ i = fscp_left_bounded_case + fscp_left_bounded_case))) \/ (exists fscp_right_bounded_case. ((exists fscp_gap_bounded_case_right_bound. fscp_gap_bounded_case_right_bound + S (fscp_right_bounded_case) = (l)) /\ ((((exists ff_h_fscp_bounded_case_right. ff_h_fscp_bounded_case_right + S (x) = S ((S (fscp_right_bounded_case)) * e)) /\ exists ff_q_fscp_bounded_case_right. d = ff_q_fscp_bounded_case_right * S ((S (fscp_right_bounded_case)) * e) + (x))) /\ i = S (fscp_right_bounded_case + fscp_right_bounded_case)))))
  18. 0018specialize hcover i
  19. 0019specialize hcover x
  20. 0020apply hcover
  21. 0021exact hibound
  22. 0022exact hvalue_witness
  23. 0023cases hcase
  24. 0024cases hcase_left
  25. 0025cases hcase_left_witness
  26. 0026cases hcase_left_witness_right
  27. 0027have hbound : ∃ v. BetaAt(b,c,x1,v) ∧ Lt(v,p)
    Exact native replay linehave hbound : exists v. ((((exists ff_h_fscp_bounded_first_lookup. ff_h_fscp_bounded_first_lookup + S (v) = S ((S (x1)) * c)) /\ exists ff_q_fscp_bounded_first_lookup. b = ff_q_fscp_bounded_first_lookup * S ((S (x1)) * c) + (v))) /\ (exists fscp_gap_bounded_first_limit. fscp_gap_bounded_first_limit + S (v) = (p)))
  28. 0028specialize hleft x1
  29. 0029apply hleft
  30. 0030exact hcase_left_witness_left
  31. 0031cases hbound
  32. 0032cases hbound_witness
  33. 0033have hequal : x = x2
  34. 0034specialize beta_at_unique b
  35. 0035specialize beta_at_unique c
  36. 0036specialize beta_at_unique x1
  37. 0037specialize beta_at_unique x
  38. 0038specialize beta_at_unique x2
  39. 0039apply beta_at_unique
  40. 0040exact hcase_left_witness_right_left
  41. 0041exact hbound_witness_left
  42. 0042exists x
  43. 0043split
  44. 0044exact hvalue_witness
  45. 0045rewrite hequal
  46. 0046exact hbound_witness_right
  47. 0047cases hcase_right
  48. 0048cases hcase_right_witness
  49. 0049cases hcase_right_witness_right
  50. 0050have hbound : ∃ v. BetaAt(d,e,x1,v) ∧ Lt(v,p)
    Exact native replay linehave hbound : exists v. ((((exists ff_h_fscp_bounded_second_lookup. ff_h_fscp_bounded_second_lookup + S (v) = S ((S (x1)) * e)) /\ exists ff_q_fscp_bounded_second_lookup. d = ff_q_fscp_bounded_second_lookup * S ((S (x1)) * e) + (v))) /\ (exists fscp_gap_bounded_second_limit. fscp_gap_bounded_second_limit + S (v) = (p)))
  51. 0051specialize hright x1
  52. 0052apply hright
  53. 0053exact hcase_right_witness_left
  54. 0054cases hbound
  55. 0055cases hbound_witness
  56. 0056have hequal : x = x2
  57. 0057specialize beta_at_unique d
  58. 0058specialize beta_at_unique e
  59. 0059specialize beta_at_unique x1
  60. 0060specialize beta_at_unique x
  61. 0061specialize beta_at_unique x2
  62. 0062apply beta_at_unique
  63. 0063exact hcase_right_witness_right_left
  64. 0064exact hbound_witness_left
  65. 0065exists x
  66. 0066split
  67. 0067exact hvalue_witness
  68. 0068rewrite hequal
  69. 0069exact hbound_witness_right