BX0002

binary_canonical_residue_exists

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

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

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 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)))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 32 exact native proof lines.

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

Proof neighborhood

Direct dependencies

BX0001 binary_modulus_nontrivial_nonzero division_remainder_exists Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized remainder_decomposition_to_mod_eq Stable theorem; checked-use authorized

Direct dependents

BX0004 binary_canonical_residue_exists_unique BX000A binary_modular_square_residue_exists BX000B binary_modular_multiply_residue_exists BX000C binary_modular_step_exists BX000E binary_modular_exponentiation_result_exists

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

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.

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 exact 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