BX000D

binary_modular_step_functional

A fixed binary digit and state determine exactly one modular transition result.

Alpha v34 checked-use · first admitted v21 · 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.

G102 was OPEN when this family was first admitted in Alpha v21. It is now CLOSED in Alpha v23: every arbitrary exponent has actual canonical beta-coded digits, a complete modular execution, and exact counted bound operations≤3*BitLen(e)+2.

Exact theorem in conservative defined notation

∀ m. ∀ x. ∀ a. ∀ b. ∀ r. ∀ s. BinaryModularStep(m,x,a,b,r) → BinaryModularStep(m,x,a,b,s) → r = s

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

Definition DAG

BinaryModularStep(m,u,a,b,r) · 2

Actual proof prerequisites

binary_canonical_residue_functional
Original expanded first-order statement 
forall m x a b r s. ((((b = 0) /\ (((exists ff_gap_binary_step_square. ff_gap_binary_step_square + S (r) = m) /\ (exists ff_left_binary_step_square_congruence ff_right_binary_step_square_congruence. (x * x) + m * ff_left_binary_step_square_congruence = (r) + m * ff_right_binary_step_square_congruence)))) \/ ((b = 1) /\ (((exists ff_gap_binary_step_multiply. ff_gap_binary_step_multiply + S (r) = m) /\ (exists ff_left_binary_step_multiply_congruence ff_right_binary_step_multiply_congruence. ((x * x) * a) + m * ff_left_binary_step_multiply_congruence = (r) + m * ff_right_binary_step_multiply_congruence)))))) -> ((((b = 0) /\ (((exists ff_gap_binary_step_other_square. ff_gap_binary_step_other_square + S (s) = m) /\ (exists ff_left_binary_step_other_square_congruence ff_right_binary_step_other_square_congruence. (x * x) + m * ff_left_binary_step_other_square_congruence = (s) + m * ff_right_binary_step_other_square_congruence)))) \/ ((b = 1) /\ (((exists ff_gap_binary_step_other_multiply. ff_gap_binary_step_other_multiply + S (s) = m) /\ (exists ff_left_binary_step_other_multiply_congruence ff_right_binary_step_other_multiply_congruence. ((x * x) * a) + m * ff_left_binary_step_other_multiply_congruence = (s) + m * ff_right_binary_step_other_multiply_congruence)))))) -> r = s

Complete unchanged native tactic proof

All 41 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

41 script commands · 17 reading checkpoints · 0 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 (1)
binary canonical residue functional
01Fix variables and assumptionsL1–8

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

  1. L1
    intro m
  2. L2
    intro x
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro r
  6. L6
    intro s
  7. L7
    intro hr
  8. L8
    intro hs
02Separate the logical casesL9–12

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

  1. L9
    cases hr
  2. L10
    cases hr_left
  3. L11
    cases hs
  4. L12
    cases hs_left
03Use earlier factsL13–19

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

  1. L13
    specialize binary_canonical_residue_functional m
  2. L14
    specialize binary_canonical_residue_functional (x * x)
  3. L15
    specialize binary_canonical_residue_functional r
  4. L16
    specialize binary_canonical_residue_functional s
  5. L17
    apply binary_canonical_residue_functional
  6. L18
    exact hr_left_right
  7. L19
    exact hs_left_right
04Separate the logical casesL20–20

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

  1. L20
    cases hs_right
05Calculate and transport equalitiesL21–21

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

  1. L21
    rewrite hr_left_left at hs_right_left
06Separate the logical casesL22–22

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

  1. L22
    exfalso
07Use earlier factsL23–23

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

  1. L23
    apply PA1
08Calculate and transport equalitiesL24–24

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

  1. L24
    symm
09Use earlier factsL25–25

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

  1. L25
    exact hs_right_left
10Separate the logical casesL26–28

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

  1. L26
    cases hr_right
  2. L27
    cases hs
  3. L28
    cases hs_left
11Calculate and transport equalitiesL29–29

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

  1. L29
    rewrite hs_left_left at hr_right_left
12Separate the logical casesL30–30

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

  1. L30
    exfalso
13Use earlier factsL31–31

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

  1. L31
    apply PA1
14Calculate and transport equalitiesL32–32

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

  1. L32
    symm
15Use earlier factsL33–33

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

  1. L33
    exact hr_right_left
16Separate the logical casesL34–34

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

  1. L34
    cases hs_right
17Use earlier factsL35–41

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

  1. L35
    specialize binary_canonical_residue_functional m
  2. L36
    specialize binary_canonical_residue_functional ((x * x) * a)
  3. L37
    specialize binary_canonical_residue_functional r
  4. L38
    specialize binary_canonical_residue_functional s
  5. L39
    apply binary_canonical_residue_functional
  6. L40
    exact hr_right_right
  7. L41
    exact hs_right_right

Library-wide reading audit

Original defined command ledger · 41 lines
  1. 0001intro m
  2. 0002intro x
  3. 0003intro a
  4. 0004intro b
  5. 0005intro r
  6. 0006intro s
  7. 0007intro hr
  8. 0008intro hs
  9. 0009cases hr
  10. 0010cases hr_left
  11. 0011cases hs
  12. 0012cases hs_left
  13. 0013specialize binary_canonical_residue_functional m
  14. 0014specialize binary_canonical_residue_functional (x * x)
  15. 0015specialize binary_canonical_residue_functional r
  16. 0016specialize binary_canonical_residue_functional s
  17. 0017apply binary_canonical_residue_functional
  18. 0018exact hr_left_right
  19. 0019exact hs_left_right
  20. 0020cases hs_right
  21. 0021rewrite hr_left_left at hs_right_left
  22. 0022exfalso
  23. 0023apply PA1
  24. 0024symm
  25. 0025exact hs_right_left
  26. 0026cases hr_right
  27. 0027cases hs
  28. 0028cases hs_left
  29. 0029rewrite hs_left_left at hr_right_left
  30. 0030exfalso
  31. 0031apply PA1
  32. 0032symm
  33. 0033exact hr_right_left
  34. 0034cases hs_right
  35. 0035specialize binary_canonical_residue_functional m
  36. 0036specialize binary_canonical_residue_functional ((x * x) * a)
  37. 0037specialize binary_canonical_residue_functional r
  38. 0038specialize binary_canonical_residue_functional s
  39. 0039apply binary_canonical_residue_functional
  40. 0040exact hr_right_right
  41. 0041exact hs_right_right