DI000B

divisor_complement_prefix_involution

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

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

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 expanded first-order arithmetic 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)))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 5 declared prerequisites and contains 56 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DI0008 divisor_complement_prefix_lookup succ_le_succ Stable theorem; checked-use authorized DI0006 divisor_complement_bounded DI0003 divisor_complement_functional DI0005 divisor_complement_symmetric

Direct dependents

none

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

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.

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 : (((~((i)=0)) /\ ((n)=(i)*(q)))) \/ ((((i)=0 \/ ~(exists pvs_factor_decoded_complementnondivisor. (n) = (i) * pvs_factor_decoded_complementnondivisor)) /\ ((q)=(i))))
  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
    have hq : exists pvs_le_gap_decoded_bound. pvs_le_gap_decoded_bound + (q) = (n)
  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 : exists r. (((((exists ff_h_pvs_decoded_next. ff_h_pvs_decoded_next + S (r) = S ((S (q)) * c)) /\ exists ff_q_pvs_decoded_next. b = ff_q_pvs_decoded_next * S ((S (q)) * c) + (r))) /\ ((((~((q)=0)) /\ ((n)=(q)*(r)))) \/ ((((q)=0 \/ ~(exists pvs_factor_decoded_next_graphnondivisor. (n) = (q) * pvs_factor_decoded_next_graphnondivisor)) /\ ((r)=(q)))))))
  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 exact 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 : (((~((i)=0)) /\ ((n)=(i)*(q)))) \/ ((((i)=0 \/ ~(exists pvs_factor_decoded_complementnondivisor. (n) = (i) * pvs_factor_decoded_complementnondivisor)) /\ ((q)=(i))))
  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 : exists pvs_le_gap_decoded_bound. pvs_le_gap_decoded_bound + (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 : exists r. (((((exists ff_h_pvs_decoded_next. ff_h_pvs_decoded_next + S (r) = S ((S (q)) * c)) /\ exists ff_q_pvs_decoded_next. b = ff_q_pvs_decoded_next * S ((S (q)) * c) + (r))) /\ ((((~((q)=0)) /\ ((n)=(q)*(r)))) \/ ((((q)=0 \/ ~(exists pvs_factor_decoded_next_graphnondivisor. (n) = (q) * pvs_factor_decoded_next_graphnondivisor)) /\ ((r)=(q)))))))
  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