FS0014

four_square_cross_covered_prefix_bounded

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 first-order arithmetic 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))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 69 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized

Direct dependents

FS0015 four_square_cross_pigeonhole

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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–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 : 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))
  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: LtBetaAt
  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 : 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)))
  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 : 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)))
  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 exact 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 : 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 : ((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 : 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 : 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