TS002T · theorem body

beta_product_adjacent_equal_pair_decomposes_as_square

dependency-curried kernel-checked candidate body; not enrolled in Alpha or Stable

Two equal adjacent decoded suffix factors collapse constructively to one explicit square times the shorter beta-coded prefix product.

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. ∀ l. ∀ n. ∀ q. Product(b,c,S S l,n) → BetaAt(b,c,l,q) → BetaAt(b,c,S l,q) → ∃ x. Product(b,c,l,x) ∧ n = x · (q · q)

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

PD0013 BetaAt PD0014 Product

In local proof propositions

PD0013 BetaAt PD0014 Product
Exact expanded first-order statement
forall b c l n q. (exists ff_u_ftsf_pair_product ff_v_ftsf_pair_product. ((((exists ff_h_ftsf_pair_product_start. ff_h_ftsf_pair_product_start + S (1) = S ((S (0)) * ff_v_ftsf_pair_product)) /\ exists ff_q_ftsf_pair_product_start. ff_u_ftsf_pair_product = ff_q_ftsf_pair_product_start * S ((S (0)) * ff_v_ftsf_pair_product) + (1))) /\ ((((exists ff_h_ftsf_pair_product_terminal. ff_h_ftsf_pair_product_terminal + S (n) = S ((S (S S l)) * ff_v_ftsf_pair_product)) /\ exists ff_q_ftsf_pair_product_terminal. ff_u_ftsf_pair_product = ff_q_ftsf_pair_product_terminal * S ((S (S S l)) * ff_v_ftsf_pair_product) + (n))) /\ forall ff_i_ftsf_pair_product. (exists ff_lt_ftsf_pair_product_bound. ff_lt_ftsf_pair_product_bound + S ff_i_ftsf_pair_product = S S l) -> exists ff_p_ftsf_pair_product ff_r_ftsf_pair_product ff_s_ftsf_pair_product. ((((exists ff_h_ftsf_pair_product_factor. ff_h_ftsf_pair_product_factor + S (ff_p_ftsf_pair_product) = S ((S (ff_i_ftsf_pair_product)) * c)) /\ exists ff_q_ftsf_pair_product_factor. b = ff_q_ftsf_pair_product_factor * S ((S (ff_i_ftsf_pair_product)) * c) + (ff_p_ftsf_pair_product))) /\ ((((exists ff_h_ftsf_pair_product_partial. ff_h_ftsf_pair_product_partial + S (ff_r_ftsf_pair_product) = S ((S (ff_i_ftsf_pair_product)) * ff_v_ftsf_pair_product)) /\ exists ff_q_ftsf_pair_product_partial. ff_u_ftsf_pair_product = ff_q_ftsf_pair_product_partial * S ((S (ff_i_ftsf_pair_product)) * ff_v_ftsf_pair_product) + (ff_r_ftsf_pair_product))) /\ ((((exists ff_h_ftsf_pair_product_successor. ff_h_ftsf_pair_product_successor + S (ff_s_ftsf_pair_product) = S ((S (S ff_i_ftsf_pair_product)) * ff_v_ftsf_pair_product)) /\ exists ff_q_ftsf_pair_product_successor. ff_u_ftsf_pair_product = ff_q_ftsf_pair_product_successor * S ((S (S ff_i_ftsf_pair_product)) * ff_v_ftsf_pair_product) + (ff_s_ftsf_pair_product))) /\ ff_s_ftsf_pair_product = ff_r_ftsf_pair_product * ff_p_ftsf_pair_product)))))) -> (((exists ff_h_ftsf_pair_first. ff_h_ftsf_pair_first + S (q) = S ((S (l)) * c)) /\ exists ff_q_ftsf_pair_first. b = ff_q_ftsf_pair_first * S ((S (l)) * c) + (q))) -> (((exists ff_h_ftsf_pair_second. ff_h_ftsf_pair_second + S (q) = S ((S (S l)) * c)) /\ exists ff_q_ftsf_pair_second. b = ff_q_ftsf_pair_second * S ((S (S l)) * c) + (q))) -> exists r. ((exists ff_u_ftsf_pair_local ff_v_ftsf_pair_local. ((((exists ff_h_ftsf_pair_local_start. ff_h_ftsf_pair_local_start + S (1) = S ((S (0)) * ff_v_ftsf_pair_local)) /\ exists ff_q_ftsf_pair_local_start. ff_u_ftsf_pair_local = ff_q_ftsf_pair_local_start * S ((S (0)) * ff_v_ftsf_pair_local) + (1))) /\ ((((exists ff_h_ftsf_pair_local_terminal. ff_h_ftsf_pair_local_terminal + S (r) = S ((S (l)) * ff_v_ftsf_pair_local)) /\ exists ff_q_ftsf_pair_local_terminal. ff_u_ftsf_pair_local = ff_q_ftsf_pair_local_terminal * S ((S (l)) * ff_v_ftsf_pair_local) + (r))) /\ forall ff_i_ftsf_pair_local. (exists ff_lt_ftsf_pair_local_bound. ff_lt_ftsf_pair_local_bound + S ff_i_ftsf_pair_local = l) -> exists ff_p_ftsf_pair_local ff_r_ftsf_pair_local ff_s_ftsf_pair_local. ((((exists ff_h_ftsf_pair_local_factor. ff_h_ftsf_pair_local_factor + S (ff_p_ftsf_pair_local) = S ((S (ff_i_ftsf_pair_local)) * c)) /\ exists ff_q_ftsf_pair_local_factor. b = ff_q_ftsf_pair_local_factor * S ((S (ff_i_ftsf_pair_local)) * c) + (ff_p_ftsf_pair_local))) /\ ((((exists ff_h_ftsf_pair_local_partial. ff_h_ftsf_pair_local_partial + S (ff_r_ftsf_pair_local) = S ((S (ff_i_ftsf_pair_local)) * ff_v_ftsf_pair_local)) /\ exists ff_q_ftsf_pair_local_partial. ff_u_ftsf_pair_local = ff_q_ftsf_pair_local_partial * S ((S (ff_i_ftsf_pair_local)) * ff_v_ftsf_pair_local) + (ff_r_ftsf_pair_local))) /\ ((((exists ff_h_ftsf_pair_local_successor. ff_h_ftsf_pair_local_successor + S (ff_s_ftsf_pair_local) = S ((S (S ff_i_ftsf_pair_local)) * ff_v_ftsf_pair_local)) /\ exists ff_q_ftsf_pair_local_successor. ff_u_ftsf_pair_local = ff_q_ftsf_pair_local_successor * S ((S (S ff_i_ftsf_pair_local)) * ff_v_ftsf_pair_local) + (ff_s_ftsf_pair_local))) /\ ff_s_ftsf_pair_local = ff_r_ftsf_pair_local * ff_p_ftsf_pair_local)))))) /\ n = r * (q * q))

Proof neighborhood

Direct theorem prerequisites

beta_product_succ_decompose · Stable closed beta_at_unique · Stable closed mul_assoc · Stable closed

Direct theorem dependents

TS002U beta_two_square_prefix_append_equal_pair

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

60 script commands · 16 reading checkpoints · 4 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–8

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 q
  6. L6
    intro hproduct
  7. L7
    intro hfirst
  8. L8
    intro hsecond
02Establish houterL9–15

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

  1. L9
    have houter : ∃ a. ∃ t. BetaAt(b,c,S l,a) ∧ (Product(b,c,S l,t) ∧ n = t · a)Definitions: BetaAt(b,c,S l,a)Product(b,c,S l,t)Original native command in the exact edition
  2. L10
    specialize beta_product_succ_decompose b
  3. L11
    specialize beta_product_succ_decompose c
  4. L12
    specialize beta_product_succ_decompose (S l)
  5. L13
    specialize beta_product_succ_decompose n
  6. L14
    apply beta_product_succ_decompose
  7. L15
    exact hproduct
03Separate the logical casesL16–19

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

  1. L16
    cases houter
  2. L17
    cases houter_witness
  3. L18
    cases houter_witness_witness
  4. L19
    cases houter_witness_witness_right
04Establish hinnerL20–26

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

  1. L20
    have hinner : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Product(b,c,l,r) ∧ x1 = r · a)Definitions: BetaAt(b,c,l,a)Product(b,c,l,r)Original native command in the exact edition
  2. L21
    specialize beta_product_succ_decompose b
  3. L22
    specialize beta_product_succ_decompose c
  4. L23
    specialize beta_product_succ_decompose l
  5. L24
    specialize beta_product_succ_decompose x1
  6. L25
    apply beta_product_succ_decompose
  7. L26
    exact houter_witness_witness_right_left
05Separate the logical casesL27–30

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

  1. L27
    cases hinner
  2. L28
    cases hinner_witness
  3. L29
    cases hinner_witness_witness
  4. L30
    cases hinner_witness_witness_right
06Establish hlast_equalL31–39

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

  1. L31
    have hlast_equal : x = q
  2. L32
    specialize beta_at_unique b
  3. L33
    specialize beta_at_unique c
  4. L34
    specialize beta_at_unique (S l)
  5. L35
    specialize beta_at_unique x
  6. L36
    specialize beta_at_unique q
  7. L37
    apply beta_at_unique
  8. L38
    exact houter_witness_witness_left
  9. L39
    exact hsecond
07Establish hfirst_equalL40–48

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

  1. L40
    have hfirst_equal : x2 = q
  2. L41
    specialize beta_at_unique b
  3. L42
    specialize beta_at_unique c
  4. L43
    specialize beta_at_unique l
  5. L44
    specialize beta_at_unique x2
  6. L45
    specialize beta_at_unique q
  7. L46
    apply beta_at_unique
  8. L47
    exact hinner_witness_witness_left
  9. L48
    exact hfirst
08Construct an explicit witnessL49–49

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

  1. L49
    exists x3
09Separate the logical casesL50–50

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

  1. L50
    split
10Use earlier factsL51–51

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

  1. L51
    exact hinner_witness_witness_right_left
11Calculate and transport equalitiesL52–52

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

  1. L52
    trans x1 * x
12Use earlier factsL53–53

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

  1. L53
    exact houter_witness_witness_right_right
13Calculate and transport equalitiesL54–55

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

  1. L54
    trans (x3 * x2) * x
  2. L55
    congr
14Use earlier factsL56–56

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

  1. L56
    exact hinner_witness_witness_right_right
15Calculate and transport equalitiesL57–59

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

  1. L57
    refl
  2. L58
    rewrite hfirst_equal
  3. L59
    rewrite hlast_equal
16Use earlier factsL60–60

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

  1. L60
    apply mul_assoc

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro q
  6. 0006intro hproduct
  7. 0007intro hfirst
  8. 0008intro hsecond
  9. 0009have houter : ∃ a. ∃ t. BetaAt(b,c,S l,a) ∧ (Product(b,c,S l,t) ∧ n = t · a)
    Exact native replay linehave houter : exists a t. ((((exists ff_h_ftsf_pair_outer. ff_h_ftsf_pair_outer + S (a) = S ((S (S l)) * c)) /\ exists ff_q_ftsf_pair_outer. b = ff_q_ftsf_pair_outer * S ((S (S l)) * c) + (a))) /\ ((exists ff_u_ftsf_pair_outer_product ff_v_ftsf_pair_outer_product. ((((exists ff_h_ftsf_pair_outer_product_start. ff_h_ftsf_pair_outer_product_start + S (1) = S ((S (0)) * ff_v_ftsf_pair_outer_product)) /\ exists ff_q_ftsf_pair_outer_product_start. ff_u_ftsf_pair_outer_product = ff_q_ftsf_pair_outer_product_start * S ((S (0)) * ff_v_ftsf_pair_outer_product) + (1))) /\ ((((exists ff_h_ftsf_pair_outer_product_terminal. ff_h_ftsf_pair_outer_product_terminal + S (t) = S ((S (S l)) * ff_v_ftsf_pair_outer_product)) /\ exists ff_q_ftsf_pair_outer_product_terminal. ff_u_ftsf_pair_outer_product = ff_q_ftsf_pair_outer_product_terminal * S ((S (S l)) * ff_v_ftsf_pair_outer_product) + (t))) /\ forall ff_i_ftsf_pair_outer_product. (exists ff_lt_ftsf_pair_outer_product_bound. ff_lt_ftsf_pair_outer_product_bound + S ff_i_ftsf_pair_outer_product = S l) -> exists ff_p_ftsf_pair_outer_product ff_r_ftsf_pair_outer_product ff_s_ftsf_pair_outer_product. ((((exists ff_h_ftsf_pair_outer_product_factor. ff_h_ftsf_pair_outer_product_factor + S (ff_p_ftsf_pair_outer_product) = S ((S (ff_i_ftsf_pair_outer_product)) * c)) /\ exists ff_q_ftsf_pair_outer_product_factor. b = ff_q_ftsf_pair_outer_product_factor * S ((S (ff_i_ftsf_pair_outer_product)) * c) + (ff_p_ftsf_pair_outer_product))) /\ ((((exists ff_h_ftsf_pair_outer_product_partial. ff_h_ftsf_pair_outer_product_partial + S (ff_r_ftsf_pair_outer_product) = S ((S (ff_i_ftsf_pair_outer_product)) * ff_v_ftsf_pair_outer_product)) /\ exists ff_q_ftsf_pair_outer_product_partial. ff_u_ftsf_pair_outer_product = ff_q_ftsf_pair_outer_product_partial * S ((S (ff_i_ftsf_pair_outer_product)) * ff_v_ftsf_pair_outer_product) + (ff_r_ftsf_pair_outer_product))) /\ ((((exists ff_h_ftsf_pair_outer_product_successor. ff_h_ftsf_pair_outer_product_successor + S (ff_s_ftsf_pair_outer_product) = S ((S (S ff_i_ftsf_pair_outer_product)) * ff_v_ftsf_pair_outer_product)) /\ exists ff_q_ftsf_pair_outer_product_successor. ff_u_ftsf_pair_outer_product = ff_q_ftsf_pair_outer_product_successor * S ((S (S ff_i_ftsf_pair_outer_product)) * ff_v_ftsf_pair_outer_product) + (ff_s_ftsf_pair_outer_product))) /\ ff_s_ftsf_pair_outer_product = ff_r_ftsf_pair_outer_product * ff_p_ftsf_pair_outer_product)))))) /\ n = t * a))
  10. 0010specialize beta_product_succ_decompose b
  11. 0011specialize beta_product_succ_decompose c
  12. 0012specialize beta_product_succ_decompose (S l)
  13. 0013specialize beta_product_succ_decompose n
  14. 0014apply beta_product_succ_decompose
  15. 0015exact hproduct
  16. 0016cases houter
  17. 0017cases houter_witness
  18. 0018cases houter_witness_witness
  19. 0019cases houter_witness_witness_right
  20. 0020have hinner : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Product(b,c,l,r) ∧ x1 = r · a)
    Exact native replay linehave hinner : exists a r. ((((exists ff_h_ftsf_pair_inner. ff_h_ftsf_pair_inner + S (a) = S ((S (l)) * c)) /\ exists ff_q_ftsf_pair_inner. b = ff_q_ftsf_pair_inner * S ((S (l)) * c) + (a))) /\ ((exists ff_u_ftsf_pair_inner_product ff_v_ftsf_pair_inner_product. ((((exists ff_h_ftsf_pair_inner_product_start. ff_h_ftsf_pair_inner_product_start + S (1) = S ((S (0)) * ff_v_ftsf_pair_inner_product)) /\ exists ff_q_ftsf_pair_inner_product_start. ff_u_ftsf_pair_inner_product = ff_q_ftsf_pair_inner_product_start * S ((S (0)) * ff_v_ftsf_pair_inner_product) + (1))) /\ ((((exists ff_h_ftsf_pair_inner_product_terminal. ff_h_ftsf_pair_inner_product_terminal + S (r) = S ((S (l)) * ff_v_ftsf_pair_inner_product)) /\ exists ff_q_ftsf_pair_inner_product_terminal. ff_u_ftsf_pair_inner_product = ff_q_ftsf_pair_inner_product_terminal * S ((S (l)) * ff_v_ftsf_pair_inner_product) + (r))) /\ forall ff_i_ftsf_pair_inner_product. (exists ff_lt_ftsf_pair_inner_product_bound. ff_lt_ftsf_pair_inner_product_bound + S ff_i_ftsf_pair_inner_product = l) -> exists ff_p_ftsf_pair_inner_product ff_r_ftsf_pair_inner_product ff_s_ftsf_pair_inner_product. ((((exists ff_h_ftsf_pair_inner_product_factor. ff_h_ftsf_pair_inner_product_factor + S (ff_p_ftsf_pair_inner_product) = S ((S (ff_i_ftsf_pair_inner_product)) * c)) /\ exists ff_q_ftsf_pair_inner_product_factor. b = ff_q_ftsf_pair_inner_product_factor * S ((S (ff_i_ftsf_pair_inner_product)) * c) + (ff_p_ftsf_pair_inner_product))) /\ ((((exists ff_h_ftsf_pair_inner_product_partial. ff_h_ftsf_pair_inner_product_partial + S (ff_r_ftsf_pair_inner_product) = S ((S (ff_i_ftsf_pair_inner_product)) * ff_v_ftsf_pair_inner_product)) /\ exists ff_q_ftsf_pair_inner_product_partial. ff_u_ftsf_pair_inner_product = ff_q_ftsf_pair_inner_product_partial * S ((S (ff_i_ftsf_pair_inner_product)) * ff_v_ftsf_pair_inner_product) + (ff_r_ftsf_pair_inner_product))) /\ ((((exists ff_h_ftsf_pair_inner_product_successor. ff_h_ftsf_pair_inner_product_successor + S (ff_s_ftsf_pair_inner_product) = S ((S (S ff_i_ftsf_pair_inner_product)) * ff_v_ftsf_pair_inner_product)) /\ exists ff_q_ftsf_pair_inner_product_successor. ff_u_ftsf_pair_inner_product = ff_q_ftsf_pair_inner_product_successor * S ((S (S ff_i_ftsf_pair_inner_product)) * ff_v_ftsf_pair_inner_product) + (ff_s_ftsf_pair_inner_product))) /\ ff_s_ftsf_pair_inner_product = ff_r_ftsf_pair_inner_product * ff_p_ftsf_pair_inner_product)))))) /\ x1 = r * a))
  21. 0021specialize beta_product_succ_decompose b
  22. 0022specialize beta_product_succ_decompose c
  23. 0023specialize beta_product_succ_decompose l
  24. 0024specialize beta_product_succ_decompose x1
  25. 0025apply beta_product_succ_decompose
  26. 0026exact houter_witness_witness_right_left
  27. 0027cases hinner
  28. 0028cases hinner_witness
  29. 0029cases hinner_witness_witness
  30. 0030cases hinner_witness_witness_right
  31. 0031have hlast_equal : x = q
  32. 0032specialize beta_at_unique b
  33. 0033specialize beta_at_unique c
  34. 0034specialize beta_at_unique (S l)
  35. 0035specialize beta_at_unique x
  36. 0036specialize beta_at_unique q
  37. 0037apply beta_at_unique
  38. 0038exact houter_witness_witness_left
  39. 0039exact hsecond
  40. 0040have hfirst_equal : x2 = q
  41. 0041specialize beta_at_unique b
  42. 0042specialize beta_at_unique c
  43. 0043specialize beta_at_unique l
  44. 0044specialize beta_at_unique x2
  45. 0045specialize beta_at_unique q
  46. 0046apply beta_at_unique
  47. 0047exact hinner_witness_witness_left
  48. 0048exact hfirst
  49. 0049exists x3
  50. 0050split
  51. 0051exact hinner_witness_witness_right_left
  52. 0052trans x1 * x
  53. 0053exact houter_witness_witness_right_right
  54. 0054trans (x3 * x2) * x
  55. 0055congr
  56. 0056exact hinner_witness_witness_right_right
  57. 0057refl
  58. 0058rewrite hfirst_equal
  59. 0059rewrite hlast_equal
  60. 0060apply mul_assoc