DI000B

divisor_complement_prefix_involution

Decoding the constructed finite map twice returns the original index, with the intermediate index proved to remain in bounds.

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

The complementary quotient is witnessed by n=d*q at positive divisors. The actual permutation covers indices zero through n, fixing zero and nondivisors. This is the involution foundation for the separate cancellation and full G007 inversion proofs, not an assumed divisor bijection.

Exact theorem in conservative defined notation

∀ n. ∀ b. ∀ c. ∀ i. ∀ q. ¬n = 0 → DivisorComplementPrefix(n,b,c,S n) → Le(i,n) → BetaAt(b,c,i,q) → BetaAt(b,c,q,i)

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

Definition DAG

DivisorComplement(n,d,q) · 2DivisorComplementPrefix(n,b,c,l) · 1Le(a,b) · 2BetaAt(b,c,i,x) · 3

Actual proof prerequisites

divisor_complement_prefix_lookupsucc_le_succ · checked external prerequisitedivisor_complement_boundeddivisor_complement_functionaldivisor_complement_symmetric
Original expanded first-order statement 
forall n b c i q. ~(n=0) -> (forall dvi_index_decoded_prefix. (exists pvs_gap_decoded_prefixdomain. pvs_gap_decoded_prefixdomain + S (dvi_index_decoded_prefix) = (S n)) -> exists dvi_value_decoded_prefix. ((((exists ff_h_pvs_decoded_prefixentry. ff_h_pvs_decoded_prefixentry + S (dvi_value_decoded_prefix) = S ((S (dvi_index_decoded_prefix)) * c)) /\ exists ff_q_pvs_decoded_prefixentry. b = ff_q_pvs_decoded_prefixentry * S ((S (dvi_index_decoded_prefix)) * c) + (dvi_value_decoded_prefix))) /\ ((((~((dvi_index_decoded_prefix)=0)) /\ ((n)=(dvi_index_decoded_prefix)*(dvi_value_decoded_prefix)))) \/ ((((dvi_index_decoded_prefix)=0 \/ ~(exists pvs_factor_decoded_prefixgraphnondivisor. (n) = (dvi_index_decoded_prefix) * pvs_factor_decoded_prefixgraphnondivisor)) /\ ((dvi_value_decoded_prefix)=(dvi_index_decoded_prefix))))))) -> (exists pvs_le_gap_decoded_input_bound. pvs_le_gap_decoded_input_bound + (i) = (n)) -> (((exists ff_h_pvs_decoded_first. ff_h_pvs_decoded_first + S (q) = S ((S (i)) * c)) /\ exists ff_q_pvs_decoded_first. b = ff_q_pvs_decoded_first * S ((S (i)) * c) + (q))) -> (((exists ff_h_pvs_decoded_second. ff_h_pvs_decoded_second + S (i) = S ((S (q)) * c)) /\ exists ff_q_pvs_decoded_second. b = ff_q_pvs_decoded_second * S ((S (q)) * c) + (i)))

Complete tactic proof in conservative notation

All 56 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

56 script commands · 10 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.

Named ingredients (4)
divisor complement prefix lookupdivisor complement boundeddivisor complement functionaldivisor complement symmetric
01Fix variables and assumptionsL1–9

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

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro i
  5. L5
    intro q
  6. L6
    intro hn
  7. L7
    intro hp
  8. L8
    intro hi
  9. L9
    intro hat
02Establish hcompL10–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor complement prefix lookup.

  1. L10
    have hcomp : DivisorComplement(n,i,q)Definitions: DivisorComplement(n,i,q)Original native command in the exact edition
  2. L11
    specialize divisor_complement_prefix_lookup (n)
  3. L12
    specialize divisor_complement_prefix_lookup (b)
  4. L13
    specialize divisor_complement_prefix_lookup (c)
  5. L14
    specialize divisor_complement_prefix_lookup (S n)
  6. L15
    specialize divisor_complement_prefix_lookup (i)
  7. L16
    specialize divisor_complement_prefix_lookup (q)
  8. L17
    apply divisor_complement_prefix_lookup
  9. L18
    exact hp
  10. L19
    specialize succ_le_succ (i)
03Use earlier factsL20–23

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

  1. L20
    specialize succ_le_succ (n)
  2. L21
    apply succ_le_succ
  3. L22
    exact hi
  4. L23
    exact hat
04Establish hqL24–31

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

  1. L24
  2. L25
    specialize divisor_complement_bounded (n)
  3. L26
    specialize divisor_complement_bounded (i)
  4. L27
    specialize divisor_complement_bounded (q)
  5. L28
    apply divisor_complement_bounded
  6. L29
    exact hn
  7. L30
    exact hi
  8. L31
    exact hcomp
05Establish hnextL32–38

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

  1. L32
    have hnext : ∃ r. BetaAt(b,c,q,r) ∧ DivisorComplement(n,q,r)Definitions: BetaAt(b,c,q,r)DivisorComplement(n,q,r)Original native command in the exact edition
  2. L33
    specialize hp (q)
  3. L34
    apply hp
  4. L35
    specialize succ_le_succ (q)
  5. L36
    specialize succ_le_succ (n)
  6. L37
    apply succ_le_succ
  7. L38
    exact hq
06Separate the logical casesL39–40

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

  1. L39
    cases hnext
  2. L40
    cases hnext_witness
07Establish heqL41–50

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

  1. L41
    have heq : x=i
  2. L42
    specialize divisor_complement_functional (n)
  3. L43
    specialize divisor_complement_functional (q)
  4. L44
    specialize divisor_complement_functional (x)
  5. L45
    specialize divisor_complement_functional (i)
  6. L46
    apply divisor_complement_functional
  7. L47
    exact hnext_witness_right
  8. L48
    specialize divisor_complement_symmetric (n)
  9. L49
    specialize divisor_complement_symmetric (i)
  10. L50
    specialize divisor_complement_symmetric (q)
08Use earlier factsL51–53

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

  1. L51
    apply divisor_complement_symmetric
  2. L52
    exact hn
  3. L53
    exact hcomp
09Calculate and transport equalitiesL54–55

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

  1. L54
    rewrite heq at hnext_witness_left
  2. L55
    rewrite heq at hnext_witness_left
10Use earlier factsL56–56

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

  1. L56
    exact hnext_witness_left

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro i
  5. 0005intro q
  6. 0006intro hn
  7. 0007intro hp
  8. 0008intro hi
  9. 0009intro hat
  10. 0010have hcomp : DivisorComplement(n,i,q)
  11. 0011specialize divisor_complement_prefix_lookup (n)
  12. 0012specialize divisor_complement_prefix_lookup (b)
  13. 0013specialize divisor_complement_prefix_lookup (c)
  14. 0014specialize divisor_complement_prefix_lookup (S n)
  15. 0015specialize divisor_complement_prefix_lookup (i)
  16. 0016specialize divisor_complement_prefix_lookup (q)
  17. 0017apply divisor_complement_prefix_lookup
  18. 0018exact hp
  19. 0019specialize succ_le_succ (i)
  20. 0020specialize succ_le_succ (n)
  21. 0021apply succ_le_succ
  22. 0022exact hi
  23. 0023exact hat
  24. 0024have hq : Le(q,n)
  25. 0025specialize divisor_complement_bounded (n)
  26. 0026specialize divisor_complement_bounded (i)
  27. 0027specialize divisor_complement_bounded (q)
  28. 0028apply divisor_complement_bounded
  29. 0029exact hn
  30. 0030exact hi
  31. 0031exact hcomp
  32. 0032have hnext : ∃ r. BetaAt(b,c,q,r) ∧ DivisorComplement(n,q,r)
  33. 0033specialize hp (q)
  34. 0034apply hp
  35. 0035specialize succ_le_succ (q)
  36. 0036specialize succ_le_succ (n)
  37. 0037apply succ_le_succ
  38. 0038exact hq
  39. 0039cases hnext
  40. 0040cases hnext_witness
  41. 0041have heq : x=i
  42. 0042specialize divisor_complement_functional (n)
  43. 0043specialize divisor_complement_functional (q)
  44. 0044specialize divisor_complement_functional (x)
  45. 0045specialize divisor_complement_functional (i)
  46. 0046apply divisor_complement_functional
  47. 0047exact hnext_witness_right
  48. 0048specialize divisor_complement_symmetric (n)
  49. 0049specialize divisor_complement_symmetric (i)
  50. 0050specialize divisor_complement_symmetric (q)
  51. 0051apply divisor_complement_symmetric
  52. 0052exact hn
  53. 0053exact hcomp
  54. 0054rewrite heq at hnext_witness_left
  55. 0055rewrite heq at hnext_witness_left
  56. 0056exact hnext_witness_left