CD0021

finite_modular_composition_pullback

The constructed value-level composition has exact two-way modular-set pullback membership.

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

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.

Sets are complete characteristic-bit codes with actual finite cardinality witnesses. The proof constructs translations and the sumset; no finite-choice oracle, supplied cardinality conclusion, or unproved polynomial-method premise is used.

Exact theorem in conservative defined notation

∀ p. ∀ t. ∀ r. ∀ s. ∀ b. ∀ c. ∀ z. ∀ d. (∀ x. Lt(x,p) → ∃ y. BetaAt(r,s,x,y) ∧ (Lt(y,p) ∧ ModEq(p,x + t,y))) → (∀ x. ∀ y. ∀ n. Lt(x,p) → BetaAt(r,s,x,y) → BetaAt(b,c,y,n) → BetaAt(z,d,x,n)) → ModularSetPullback(b,c,z,d,p,t)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ModularSetPullback(b,c,d,e,p,t) · 1Lt(a,b) · 4ModEq(m,a,b) · 2BetaAt(b,c,i,x) · 7

Actual proof prerequisites

mod_eq_bounded_unique · checked external prerequisitemod_eq_trans · checked external prerequisitemod_eq_symm · checked external prerequisitebeta_at_exists · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall p t r s b c z d. (forall fms_i_indices. (exists fms_gap_indices. fms_gap_indices + S (fms_i_indices) = (p)) -> exists fms_j_indices. (((exists fs_h_fms_indices_entry. fs_h_fms_indices_entry + S (fms_j_indices) = S ((S (fms_i_indices)) * s)) /\ exists fs_q_fms_indices_entry. r = fs_q_fms_indices_entry * S ((S (fms_i_indices)) * s) + (fms_j_indices))) /\ ((exists fms_gap_indices_bound. fms_gap_indices_bound + S (fms_j_indices) = (p)) /\ (exists fms_u_indices fms_v_indices. (fms_i_indices+t) + (p) * fms_u_indices = (fms_j_indices) + (p) * fms_v_indices))) -> (forall fms_i_compose fms_j_compose fms_v_compose. (exists fms_gap_compose. fms_gap_compose + S (fms_i_compose) = (p)) -> (((exists fs_h_fms_compose_index. fs_h_fms_compose_index + S (fms_j_compose) = S ((S (fms_i_compose)) * s)) /\ exists fs_q_fms_compose_index. r = fs_q_fms_compose_index * S ((S (fms_i_compose)) * s) + (fms_j_compose))) -> (((exists fs_h_fms_compose_source. fs_h_fms_compose_source + S (fms_v_compose) = S ((S (fms_j_compose)) * c)) /\ exists fs_q_fms_compose_source. b = fs_q_fms_compose_source * S ((S (fms_j_compose)) * c) + (fms_v_compose))) -> (((exists fs_h_fms_compose_target. fs_h_fms_compose_target + S (fms_v_compose) = S ((S (fms_i_compose)) * d)) /\ exists fs_q_fms_compose_target. z = fs_q_fms_compose_target * S ((S (fms_i_compose)) * d) + (fms_v_compose)))) -> (forall fms_i_pullback fms_j_pullback. (exists fms_gap_pullback_i. fms_gap_pullback_i + S (fms_i_pullback) = (p)) -> (exists fms_gap_pullback_j. fms_gap_pullback_j + S (fms_j_pullback) = (p)) -> (exists fms_u_pullback fms_v_pullback. (fms_i_pullback + t) + (p) * fms_u_pullback = (fms_j_pullback) + (p) * fms_v_pullback) -> ((((((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * d)) /\ exists fs_q_fms_pullback_target. z = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * d) + (1))) -> (((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * c) + (1)))) /\ ((((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * c) + (1))) -> (((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * d)) /\ exists fs_q_fms_pullback_target. z = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * d) + (1)))))))

Complete tactic proof in conservative notation

All 78 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

78 script commands · 17 reading checkpoints · 5 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 p
  2. L2
    intro t
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro z
  8. L8
    intro d
  9. L9
    intro hindices
  10. L10
    intro hcompose
02Fix variables and assumptionsL11–15

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

  1. L11
    intro i
  2. L12
    intro j
  3. L13
    intro hi
  4. L14
    intro hj
  5. L15
    intro hmod
03Establish hkL16–19

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

  1. L16
    have hk : ∃ k. BetaAt(r,s,i,k) ∧ (Lt(k,p) ∧ ModEq(p,i + t,k))Definitions: BetaAt(r,s,i,k)Lt(k,p)ModEq(p,i + t,k)Original native command in the exact edition
  2. L17
    specialize hindices i
  3. L18
    apply hindices
  4. L19
    exact hi
04Separate the logical casesL20–22

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

  1. L20
    cases hk
  2. L21
    cases hk_witness
  3. L22
    cases hk_witness_right
05Establish heL23–32

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

  1. L23
    have he : x=j
  2. L24
    specialize mod_eq_bounded_unique p
  3. L25
    specialize mod_eq_bounded_unique x
  4. L26
    specialize mod_eq_bounded_unique j
  5. L27
    apply mod_eq_bounded_unique
  6. L28
    exact hk_witness_right_left
  7. L29
    exact hj
  8. L30
    specialize mod_eq_trans p
  9. L31
    specialize mod_eq_trans x
  10. L32
    specialize mod_eq_trans i+t
06Use earlier factsL33–40

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

  1. L33
    specialize mod_eq_trans j
  2. L34
    apply mod_eq_trans
  3. L35
    specialize mod_eq_symm p
  4. L36
    specialize mod_eq_symm i+t
  5. L37
    specialize mod_eq_symm x
  6. L38
    apply mod_eq_symm
  7. L39
    exact hk_witness_right_right
  8. L40
    exact hmod
07Calculate and transport equalitiesL41–42

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

  1. L41
    rewrite he at hk_witness_left
  2. L42
    rewrite he at hk_witness_left
08Separate the logical casesL43–43

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

  1. L43
    split
09Fix variables and assumptionsL44–44

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

  1. L44
    intro ht
10Establish haL45–49

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

  1. L45
    have ha : ∃ a. BetaAt(b,c,j,a)Definitions: BetaAt(b,c,j,a)Original native command in the exact edition
  2. L46
    specialize beta_at_exists b
  3. L47
    specialize beta_at_exists c
  4. L48
    specialize beta_at_exists j
  5. L49
    apply beta_at_exists
11Separate the logical casesL50–50

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

  1. L50
    cases ha
12Establish hvL51–58

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

  1. L51
  2. L52
    specialize hcompose i
  3. L53
    specialize hcompose j
  4. L54
    specialize hcompose x1
  5. L55
    apply hcompose
  6. L56
    exact hi
  7. L57
    exact hk_witness_left
  8. L58
    exact ha_witness
13Establish honeL59–68

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

  1. L59
    have hone : x1=1
  2. L60
    specialize beta_at_unique z
  3. L61
    specialize beta_at_unique d
  4. L62
    specialize beta_at_unique i
  5. L63
    specialize beta_at_unique x1
  6. L64
    specialize beta_at_unique 1
  7. L65
    apply beta_at_unique
  8. L66
    exact hv
  9. L67
    exact ht
  10. L68
    rewrite hone at ha_witness
14Calculate and transport equalitiesL69–69

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

  1. L69
    rewrite hone at ha_witness
15Use earlier factsL70–70

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

  1. L70
    exact ha_witness
16Fix variables and assumptionsL71–71

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

  1. L71
    intro hs
17Use earlier factsL72–78

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

  1. L72
    specialize hcompose i
  2. L73
    specialize hcompose j
  3. L74
    specialize hcompose 1
  4. L75
    apply hcompose
  5. L76
    exact hi
  6. L77
    exact hk_witness_left
  7. L78
    exact hs

Library-wide reading audit

Original defined command ledger · 78 lines
  1. 0001intro p
  2. 0002intro t
  3. 0003intro r
  4. 0004intro s
  5. 0005intro b
  6. 0006intro c
  7. 0007intro z
  8. 0008intro d
  9. 0009intro hindices
  10. 0010intro hcompose
  11. 0011intro i
  12. 0012intro j
  13. 0013intro hi
  14. 0014intro hj
  15. 0015intro hmod
  16. 0016have hk : ∃ k. BetaAt(r,s,i,k) ∧ (Lt(k,p) ∧ ModEq(p,i + t,k))
  17. 0017specialize hindices i
  18. 0018apply hindices
  19. 0019exact hi
  20. 0020cases hk
  21. 0021cases hk_witness
  22. 0022cases hk_witness_right
  23. 0023have he : x=j
  24. 0024specialize mod_eq_bounded_unique p
  25. 0025specialize mod_eq_bounded_unique x
  26. 0026specialize mod_eq_bounded_unique j
  27. 0027apply mod_eq_bounded_unique
  28. 0028exact hk_witness_right_left
  29. 0029exact hj
  30. 0030specialize mod_eq_trans p
  31. 0031specialize mod_eq_trans x
  32. 0032specialize mod_eq_trans i+t
  33. 0033specialize mod_eq_trans j
  34. 0034apply mod_eq_trans
  35. 0035specialize mod_eq_symm p
  36. 0036specialize mod_eq_symm i+t
  37. 0037specialize mod_eq_symm x
  38. 0038apply mod_eq_symm
  39. 0039exact hk_witness_right_right
  40. 0040exact hmod
  41. 0041rewrite he at hk_witness_left
  42. 0042rewrite he at hk_witness_left
  43. 0043split
  44. 0044intro ht
  45. 0045have ha : ∃ a. BetaAt(b,c,j,a)
  46. 0046specialize beta_at_exists b
  47. 0047specialize beta_at_exists c
  48. 0048specialize beta_at_exists j
  49. 0049apply beta_at_exists
  50. 0050cases ha
  51. 0051have hv : BetaAt(z,d,i,x1)
  52. 0052specialize hcompose i
  53. 0053specialize hcompose j
  54. 0054specialize hcompose x1
  55. 0055apply hcompose
  56. 0056exact hi
  57. 0057exact hk_witness_left
  58. 0058exact ha_witness
  59. 0059have hone : x1=1
  60. 0060specialize beta_at_unique z
  61. 0061specialize beta_at_unique d
  62. 0062specialize beta_at_unique i
  63. 0063specialize beta_at_unique x1
  64. 0064specialize beta_at_unique 1
  65. 0065apply beta_at_unique
  66. 0066exact hv
  67. 0067exact ht
  68. 0068rewrite hone at ha_witness
  69. 0069rewrite hone at ha_witness
  70. 0070exact ha_witness
  71. 0071intro hs
  72. 0072specialize hcompose i
  73. 0073specialize hcompose j
  74. 0074specialize hcompose 1
  75. 0075apply hcompose
  76. 0076exact hi
  77. 0077exact hk_witness_left
  78. 0078exact hs