DI000C

divisor_complement_prefix_positive_quotient

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

The actual beta code at a positive divisor is precisely its witnessed quotient, not merely an unspecified bounded permutation image.

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 d q. ~(n=0) -> (forall dvi_index_decoded_quotient_prefix. (exists pvs_gap_decoded_quotient_prefixdomain. pvs_gap_decoded_quotient_prefixdomain + S (dvi_index_decoded_quotient_prefix) = (S n)) -> exists dvi_value_decoded_quotient_prefix. ((((exists ff_h_pvs_decoded_quotient_prefixentry. ff_h_pvs_decoded_quotient_prefixentry + S (dvi_value_decoded_quotient_prefix) = S ((S (dvi_index_decoded_quotient_prefix)) * c)) /\ exists ff_q_pvs_decoded_quotient_prefixentry. b = ff_q_pvs_decoded_quotient_prefixentry * S ((S (dvi_index_decoded_quotient_prefix)) * c) + (dvi_value_decoded_quotient_prefix))) /\ ((((~((dvi_index_decoded_quotient_prefix)=0)) /\ ((n)=(dvi_index_decoded_quotient_prefix)*(dvi_value_decoded_quotient_prefix)))) \/ ((((dvi_index_decoded_quotient_prefix)=0 \/ ~(exists pvs_factor_decoded_quotient_prefixgraphnondivisor. (n) = (dvi_index_decoded_quotient_prefix) * pvs_factor_decoded_quotient_prefixgraphnondivisor)) /\ ((dvi_value_decoded_quotient_prefix)=(dvi_index_decoded_quotient_prefix))))))) -> ~(d=0) -> n=d*q -> (((exists ff_h_pvs_decoded_quotient_result. ff_h_pvs_decoded_quotient_result + S (q) = S ((S (d)) * c)) /\ exists ff_q_pvs_decoded_quotient_result. b = ff_q_pvs_decoded_quotient_result * S ((S (d)) * c) + (q)))

Constructive proof overview

Generated structural guide

The actual beta code at a positive divisor is precisely its witnessed quotient, not merely an unspecified bounded permutation image.

The unchanged tactic script uses 3 declared prerequisites and contains 39 exact native proof lines.

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

Proof neighborhood

Direct dependencies

succ_le_succ Stable theorem; checked-use authorized divisor_le_nonzero Stable theorem; checked-use authorized DI0003 divisor_complement_functional

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

39 script commands · 11 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)
divisor complement functional
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 d
  5. L5
    intro q
  6. L6
    intro hn
  7. L7
    intro hp
  8. L8
    intro hd
  9. L9
    intro heq
02Establish hboundL10–17

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

  1. L10
    have hbound : exists pvs_gap_decoded_quotient_bound. pvs_gap_decoded_quotient_bound + S (d) = (S n)
  2. L11
    specialize succ_le_succ (d)
  3. L12
    specialize succ_le_succ (n)
  4. L13
    apply succ_le_succ
  5. L14
    specialize divisor_le_nonzero (d)
  6. L15
    specialize divisor_le_nonzero (n)
  7. L16
    apply divisor_le_nonzero
  8. L17
    exact hn
03Construct an explicit witnessL18–18

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

  1. L18
    exists q
04Use earlier factsL19–19

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

  1. L19
    exact heq
05Establish hvL20–23

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

  1. L20
    have hv : exists r. (((((exists ff_h_pvs_decoded_quotient_entry. ff_h_pvs_decoded_quotient_entry + S (r) = S ((S (d)) * c)) /\ exists ff_q_pvs_decoded_quotient_entry. b = ff_q_pvs_decoded_quotient_entry * S ((S (d)) * c) + (r))) /\ ((((~((d)=0)) /\ ((n)=(d)*(r)))) \/ ((((d)=0 \/ ~(exists pvs_factor_decoded_quotient_graphnondivisor. (n) = (d) * pvs_factor_decoded_quotient_graphnondivisor)) /\ ((r)=(d)))))))
  2. L21
    specialize hp (d)
  3. L22
    apply hp
  4. L23
    exact hbound
06Separate the logical casesL24–25

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

  1. L24
    cases hv
  2. L25
    cases hv_witness
07Establish hvalueL26–32

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

  1. L26
    have hvalue : x=q
  2. L27
    specialize divisor_complement_functional (n)
  3. L28
    specialize divisor_complement_functional (d)
  4. L29
    specialize divisor_complement_functional (x)
  5. L30
    specialize divisor_complement_functional (q)
  6. L31
    apply divisor_complement_functional
  7. L32
    exact hv_witness_right
08Separate the logical casesL33–34

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

  1. L33
    left
  2. L34
    split
09Use earlier factsL35–36

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

  1. L35
    exact hd
  2. L36
    exact heq
10Calculate and transport equalitiesL37–38

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

  1. L37
    rewrite hvalue at hv_witness_left
  2. L38
    rewrite hvalue at hv_witness_left
11Use earlier factsL39–39

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

  1. L39
    exact hv_witness_left

Library-wide reading audit

Original exact command ledger · 39 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro q
  6. 0006intro hn
  7. 0007intro hp
  8. 0008intro hd
  9. 0009intro heq
  10. 0010have hbound : exists pvs_gap_decoded_quotient_bound. pvs_gap_decoded_quotient_bound + S (d) = (S n)
  11. 0011specialize succ_le_succ (d)
  12. 0012specialize succ_le_succ (n)
  13. 0013apply succ_le_succ
  14. 0014specialize divisor_le_nonzero (d)
  15. 0015specialize divisor_le_nonzero (n)
  16. 0016apply divisor_le_nonzero
  17. 0017exact hn
  18. 0018exists q
  19. 0019exact heq
  20. 0020have hv : exists r. (((((exists ff_h_pvs_decoded_quotient_entry. ff_h_pvs_decoded_quotient_entry + S (r) = S ((S (d)) * c)) /\ exists ff_q_pvs_decoded_quotient_entry. b = ff_q_pvs_decoded_quotient_entry * S ((S (d)) * c) + (r))) /\ ((((~((d)=0)) /\ ((n)=(d)*(r)))) \/ ((((d)=0 \/ ~(exists pvs_factor_decoded_quotient_graphnondivisor. (n) = (d) * pvs_factor_decoded_quotient_graphnondivisor)) /\ ((r)=(d)))))))
  21. 0021specialize hp (d)
  22. 0022apply hp
  23. 0023exact hbound
  24. 0024cases hv
  25. 0025cases hv_witness
  26. 0026have hvalue : x=q
  27. 0027specialize divisor_complement_functional (n)
  28. 0028specialize divisor_complement_functional (d)
  29. 0029specialize divisor_complement_functional (x)
  30. 0030specialize divisor_complement_functional (q)
  31. 0031apply divisor_complement_functional
  32. 0032exact hv_witness_right
  33. 0033left
  34. 0034split
  35. 0035exact hd
  36. 0036exact heq
  37. 0037rewrite hvalue at hv_witness_left
  38. 0038rewrite hvalue at hv_witness_left
  39. 0039exact hv_witness_left