BX0002

binary_canonical_residue_exists

Every value has a witnessed canonical residue below every modulus m>1.

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. ∀ n. BinaryModulus(m) → ∃ x. CanonicalModularResidue(m,n,x)

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

Definition DAG

BinaryModulus(m) · 1CanonicalModularResidue(m,a,r) · 1

Actual proof prerequisites

binary_modulus_nontrivial_nonzerodivision_remainder_exists · checked external prerequisitemul_comm · checked external prerequisiteremainder_decomposition_to_mod_eq · checked external prerequisite
Original expanded first-order statement 
forall m n. (exists ff_modulus_gap_binary_guard. ff_modulus_gap_binary_guard + S 1 = m) -> exists r. (((exists ff_gap_binary_value. ff_gap_binary_value + S (r) = m) /\ (exists ff_left_binary_value_congruence ff_right_binary_value_congruence. (n) + m * ff_left_binary_value_congruence = (r) + m * ff_right_binary_value_congruence)))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

32 script commands · 8 reading checkpoints · 3 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 modulus nontrivial nonzero
01Fix variables and assumptionsL1–3

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro hmodulus
02Establish hnonzeroL4–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary modulus nontrivial nonzero.

  1. L4
    have hnonzero : ~(m = 0)
  2. L5
    intro hzero
  3. L6
    specialize binary_modulus_nontrivial_nonzero m
  4. L7
    apply binary_modulus_nontrivial_nonzero
  5. L8
    exact hmodulus
  6. L9
    exact hzero
03Establish hdivisionL10–14

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

  1. L10
    have hdivision : exists q r. n = m * q + r /\ exists gap. gap + S r = m
  2. L11
    specialize division_remainder_exists m
  3. L12
    specialize division_remainder_exists n
  4. L13
    apply division_remainder_exists
  5. L14
    exact hnonzero
04Separate the logical casesL15–17

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

  1. L15
    cases hdivision
  2. L16
    cases hdivision_witness
  3. L17
    cases hdivision_witness_witness
05Establish hdecompositionL18–23

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

  1. L18
    have hdecomposition : n = x * m + x1
  2. L19
    trans m * x + x1
  3. L20
    exact hdivision_witness_witness_left
  4. L21
    congr
  5. L22
    apply mul_comm
  6. L23
    refl
06Construct an explicit witnessL24–24

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

  1. L24
    exists x1
07Separate the logical casesL25–25

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

  1. L25
    split
08Use earlier factsL26–32

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

  1. L26
    exact hdivision_witness_witness_right
  2. L27
    specialize remainder_decomposition_to_mod_eq m
  3. L28
    specialize remainder_decomposition_to_mod_eq n
  4. L29
    specialize remainder_decomposition_to_mod_eq x
  5. L30
    specialize remainder_decomposition_to_mod_eq x1
  6. L31
    apply remainder_decomposition_to_mod_eq
  7. L32
    exact hdecomposition

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro hmodulus
  4. 0004have hnonzero : ~(m = 0)
  5. 0005intro hzero
  6. 0006specialize binary_modulus_nontrivial_nonzero m
  7. 0007apply binary_modulus_nontrivial_nonzero
  8. 0008exact hmodulus
  9. 0009exact hzero
  10. 0010have hdivision : exists q r. n = m * q + r /\ exists gap. gap + S r = m
  11. 0011specialize division_remainder_exists m
  12. 0012specialize division_remainder_exists n
  13. 0013apply division_remainder_exists
  14. 0014exact hnonzero
  15. 0015cases hdivision
  16. 0016cases hdivision_witness
  17. 0017cases hdivision_witness_witness
  18. 0018have hdecomposition : n = x * m + x1
  19. 0019trans m * x + x1
  20. 0020exact hdivision_witness_witness_left
  21. 0021congr
  22. 0022apply mul_comm
  23. 0023refl
  24. 0024exists x1
  25. 0025split
  26. 0026exact hdivision_witness_witness_right
  27. 0027specialize remainder_decomposition_to_mod_eq m
  28. 0028specialize remainder_decomposition_to_mod_eq n
  29. 0029specialize remainder_decomposition_to_mod_eq x
  30. 0030specialize remainder_decomposition_to_mod_eq x1
  31. 0031apply remainder_decomposition_to_mod_eq
  32. 0032exact hdecomposition