JT001D

jordan_tuple_scan_empty

Empty scan has soundness, no duplicate positions, and vacuous code coverage.

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

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ k. ∀ n. ∀ c. ∀ B. ∀ C. ∀ D. ∀ E. JordanTupleScan(k,n,c,0,B,C,D,E,0)

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

Definition DAG

JordanTupleScan(k,n,c,limit,B,C,D,E,j) · 1

Actual proof prerequisites

lt_not_le · checked external prerequisitezero_le · checked external prerequisite
Original expanded first-order statement 
forall k n c B C D E. ((forall jt_i_scanempty. (exists jt_gap_scanemptysoundindex. jt_gap_scanemptysoundindex+S (jt_i_scanempty)=(0)) -> exists jt_b_scanempty jt_e_scanempty. ((((((exists fs_h_jt_scanemptysoundcode. fs_h_jt_scanemptysoundcode + S (jt_b_scanempty) = S ((S (jt_i_scanempty)) * C)) /\ exists fs_q_jt_scanemptysoundcode. B = fs_q_jt_scanemptysoundcode * S ((S (jt_i_scanempty)) * C) + (jt_b_scanempty))) /\ (((exists fs_h_jt_scanemptysoundscale. fs_h_jt_scanemptysoundscale + S (jt_e_scanempty) = S ((S (jt_i_scanempty)) * E)) /\ exists fs_q_jt_scanemptysoundscale. D = fs_q_jt_scanemptysoundscale * S ((S (jt_i_scanempty)) * E) + (jt_e_scanempty))))) /\ (((forall jt_index_scanemptybound. (exists jt_gap_scanemptyboundindex. jt_gap_scanemptyboundindex+S (jt_index_scanemptybound)=(k)) -> exists jt_value_scanemptybound. ((((exists fs_h_jt_scanemptyboundat. fs_h_jt_scanemptyboundat + S (jt_value_scanemptybound) = S ((S (jt_index_scanemptybound)) * jt_e_scanempty)) /\ exists fs_q_jt_scanemptyboundat. jt_b_scanempty = fs_q_jt_scanemptyboundat * S ((S (jt_index_scanemptybound)) * jt_e_scanempty) + (jt_value_scanemptybound))) /\ (exists jt_gap_scanemptyboundvalue. jt_gap_scanemptyboundvalue+S (jt_value_scanemptybound)=(n)))) /\ (forall jt_divisor_scanemptyprimitive. (exists jt_factor_scanemptyprimitivemodulus. (n)=(jt_divisor_scanemptyprimitive)*jt_factor_scanemptyprimitivemodulus) -> (forall jt_index_scanemptyprimitivecoordinates jt_value_scanemptyprimitivecoordinates. (exists jt_gap_scanemptyprimitivecoordinatesindex. jt_gap_scanemptyprimitivecoordinatesindex+S (jt_index_scanemptyprimitivecoordinates)=(k)) -> (((exists fs_h_jt_scanemptyprimitivecoordinatesat. fs_h_jt_scanemptyprimitivecoordinatesat + S (jt_value_scanemptyprimitivecoordinates) = S ((S (jt_index_scanemptyprimitivecoordinates)) * jt_e_scanempty)) /\ exists fs_q_jt_scanemptyprimitivecoordinatesat. jt_b_scanempty = fs_q_jt_scanemptyprimitivecoordinatesat * S ((S (jt_index_scanemptyprimitivecoordinates)) * jt_e_scanempty) + (jt_value_scanemptyprimitivecoordinates))) -> (exists jt_factor_scanemptyprimitivecoordinatesdivides. (jt_value_scanemptyprimitivecoordinates)=(jt_divisor_scanemptyprimitive)*jt_factor_scanemptyprimitivecoordinatesdivides)) -> jt_divisor_scanemptyprimitive=1))))) /\ (((forall jt_i_scanempty jt_h_scanempty jt_b_scanempty jt_e_scanempty jt_d_scanempty jt_f_scanempty. (exists jt_gap_scanemptyfirstindex. jt_gap_scanemptyfirstindex+S (jt_i_scanempty)=(0)) -> (exists jt_gap_scanemptysecondindex. jt_gap_scanemptysecondindex+S (jt_h_scanempty)=(0)) -> (((((exists fs_h_jt_scanemptyfirstcode. fs_h_jt_scanemptyfirstcode + S (jt_b_scanempty) = S ((S (jt_i_scanempty)) * C)) /\ exists fs_q_jt_scanemptyfirstcode. B = fs_q_jt_scanemptyfirstcode * S ((S (jt_i_scanempty)) * C) + (jt_b_scanempty))) /\ (((exists fs_h_jt_scanemptyfirstscale. fs_h_jt_scanemptyfirstscale + S (jt_e_scanempty) = S ((S (jt_i_scanempty)) * E)) /\ exists fs_q_jt_scanemptyfirstscale. D = fs_q_jt_scanemptyfirstscale * S ((S (jt_i_scanempty)) * E) + (jt_e_scanempty))))) -> (((((exists fs_h_jt_scanemptysecondcode. fs_h_jt_scanemptysecondcode + S (jt_d_scanempty) = S ((S (jt_h_scanempty)) * C)) /\ exists fs_q_jt_scanemptysecondcode. B = fs_q_jt_scanemptysecondcode * S ((S (jt_h_scanempty)) * C) + (jt_d_scanempty))) /\ (((exists fs_h_jt_scanemptysecondscale. fs_h_jt_scanemptysecondscale + S (jt_f_scanempty) = S ((S (jt_h_scanempty)) * E)) /\ exists fs_q_jt_scanemptysecondscale. D = fs_q_jt_scanemptysecondscale * S ((S (jt_h_scanempty)) * E) + (jt_f_scanempty))))) -> (forall jt_index_scanemptysame jt_left_scanemptysame jt_right_scanemptysame. (exists jt_gap_scanemptysameindex. jt_gap_scanemptysameindex+S (jt_index_scanemptysame)=(k)) -> (((exists fs_h_jt_scanemptysameleft. fs_h_jt_scanemptysameleft + S (jt_left_scanemptysame) = S ((S (jt_index_scanemptysame)) * jt_e_scanempty)) /\ exists fs_q_jt_scanemptysameleft. jt_b_scanempty = fs_q_jt_scanemptysameleft * S ((S (jt_index_scanemptysame)) * jt_e_scanempty) + (jt_left_scanemptysame))) -> (((exists fs_h_jt_scanemptysameright. fs_h_jt_scanemptysameright + S (jt_right_scanemptysame) = S ((S (jt_index_scanemptysame)) * jt_f_scanempty)) /\ exists fs_q_jt_scanemptysameright. jt_d_scanempty = fs_q_jt_scanemptysameright * S ((S (jt_index_scanemptysame)) * jt_f_scanempty) + (jt_right_scanemptysame))) -> jt_left_scanemptysame=jt_right_scanemptysame) -> jt_i_scanempty=jt_h_scanempty) /\ (forall jt_z_scanempty. (exists jt_gap_scanemptycodeindex. jt_gap_scanemptycodeindex+S (jt_z_scanempty)=(0)) -> (forall jt_index_scanemptyinputbound. (exists jt_gap_scanemptyinputboundindex. jt_gap_scanemptyinputboundindex+S (jt_index_scanemptyinputbound)=(k)) -> exists jt_value_scanemptyinputbound. ((((exists fs_h_jt_scanemptyinputboundat. fs_h_jt_scanemptyinputboundat + S (jt_value_scanemptyinputbound) = S ((S (jt_index_scanemptyinputbound)) * c)) /\ exists fs_q_jt_scanemptyinputboundat. jt_z_scanempty = fs_q_jt_scanemptyinputboundat * S ((S (jt_index_scanemptyinputbound)) * c) + (jt_value_scanemptyinputbound))) /\ (exists jt_gap_scanemptyinputboundvalue. jt_gap_scanemptyinputboundvalue+S (jt_value_scanemptyinputbound)=(n)))) -> (forall jt_divisor_scanemptyinputprimitive. (exists jt_factor_scanemptyinputprimitivemodulus. (n)=(jt_divisor_scanemptyinputprimitive)*jt_factor_scanemptyinputprimitivemodulus) -> (forall jt_index_scanemptyinputprimitivecoordinates jt_value_scanemptyinputprimitivecoordinates. (exists jt_gap_scanemptyinputprimitivecoordinatesindex. jt_gap_scanemptyinputprimitivecoordinatesindex+S (jt_index_scanemptyinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_scanemptyinputprimitivecoordinatesat. fs_h_jt_scanemptyinputprimitivecoordinatesat + S (jt_value_scanemptyinputprimitivecoordinates) = S ((S (jt_index_scanemptyinputprimitivecoordinates)) * c)) /\ exists fs_q_jt_scanemptyinputprimitivecoordinatesat. jt_z_scanempty = fs_q_jt_scanemptyinputprimitivecoordinatesat * S ((S (jt_index_scanemptyinputprimitivecoordinates)) * c) + (jt_value_scanemptyinputprimitivecoordinates))) -> (exists jt_factor_scanemptyinputprimitivecoordinatesdivides. (jt_value_scanemptyinputprimitivecoordinates)=(jt_divisor_scanemptyinputprimitive)*jt_factor_scanemptyinputprimitivecoordinatesdivides)) -> jt_divisor_scanemptyinputprimitive=1) -> (exists jt_index_scanemptylisted jt_code_scanemptylisted jt_scale_scanemptylisted. ((exists jt_gap_scanemptylistedindex. jt_gap_scanemptylistedindex+S (jt_index_scanemptylisted)=(0)) /\ (((((((exists fs_h_jt_scanemptylistedcode. fs_h_jt_scanemptylistedcode + S (jt_code_scanemptylisted) = S ((S (jt_index_scanemptylisted)) * C)) /\ exists fs_q_jt_scanemptylistedcode. B = fs_q_jt_scanemptylistedcode * S ((S (jt_index_scanemptylisted)) * C) + (jt_code_scanemptylisted))) /\ (((exists fs_h_jt_scanemptylistedscale. fs_h_jt_scanemptylistedscale + S (jt_scale_scanemptylisted) = S ((S (jt_index_scanemptylisted)) * E)) /\ exists fs_q_jt_scanemptylistedscale. D = fs_q_jt_scanemptylistedscale * S ((S (jt_index_scanemptylisted)) * E) + (jt_scale_scanemptylisted))))) /\ (forall jt_index_scanemptylistedequal jt_left_scanemptylistedequal jt_right_scanemptylistedequal. (exists jt_gap_scanemptylistedequalindex. jt_gap_scanemptylistedequalindex+S (jt_index_scanemptylistedequal)=(k)) -> (((exists fs_h_jt_scanemptylistedequalleft. fs_h_jt_scanemptylistedequalleft + S (jt_left_scanemptylistedequal) = S ((S (jt_index_scanemptylistedequal)) * c)) /\ exists fs_q_jt_scanemptylistedequalleft. jt_z_scanempty = fs_q_jt_scanemptylistedequalleft * S ((S (jt_index_scanemptylistedequal)) * c) + (jt_left_scanemptylistedequal))) -> (((exists fs_h_jt_scanemptylistedequalright. fs_h_jt_scanemptylistedequalright + S (jt_right_scanemptylistedequal) = S ((S (jt_index_scanemptylistedequal)) * jt_scale_scanemptylisted)) /\ exists fs_q_jt_scanemptylistedequalright. jt_code_scanemptylisted = fs_q_jt_scanemptylistedequalright * S ((S (jt_index_scanemptylistedequal)) * jt_scale_scanemptylisted) + (jt_right_scanemptylistedequal))) -> jt_left_scanemptylistedequal=jt_right_scanemptylistedequal)))))))))

Complete tactic proof in conservative notation

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

47 script commands · 13 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro k
  2. L2
    intro n
  3. L3
    intro c
  4. L4
    intro B
  5. L5
    intro C
  6. L6
    intro D
  7. L7
    intro E
02Separate the logical casesL8–8

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

  1. L8
    split
03Fix variables and assumptionsL9–10

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

  1. L9
    intro i
  2. L10
    intro hi
04Separate the logical casesL11–11

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

  1. L11
    exfalso
05Use earlier factsL12–17

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

  1. L12
    specialize lt_not_le (i)
  2. L13
    specialize lt_not_le (0)
  3. L14
    apply lt_not_le
  4. L15
    exact hi
  5. L16
    specialize zero_le (i)
  6. L17
    apply zero_le
06Separate the logical casesL18–18

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

  1. L18
    split
07Fix variables and assumptionsL19–28

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

  1. L19
    intro i
  2. L20
    intro h
  3. L21
    intro b
  4. L22
    intro e
  5. L23
    intro d
  6. L24
    intro f
  7. L25
    intro hi
  8. L26
    intro hh
  9. L27
    intro he
  10. L28
    intro hf
08Fix variables and assumptionsL29–29

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

  1. L29
    intro heq
09Separate the logical casesL30–30

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

  1. L30
    exfalso
10Use earlier factsL31–36

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

  1. L31
    specialize lt_not_le (i)
  2. L32
    specialize lt_not_le (0)
  3. L33
    apply lt_not_le
  4. L34
    exact hi
  5. L35
    specialize zero_le (i)
  6. L36
    apply zero_le
11Fix variables and assumptionsL37–40

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

  1. L37
    intro z
  2. L38
    intro hz
  3. L39
    intro hb
  4. L40
    intro hp
12Separate the logical casesL41–41

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

  1. L41
    exfalso
13Use earlier factsL42–47

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

  1. L42
    specialize lt_not_le (z)
  2. L43
    specialize lt_not_le (0)
  3. L44
    apply lt_not_le
  4. L45
    exact hz
  5. L46
    specialize zero_le (z)
  6. L47
    apply zero_le

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro k
  2. 0002intro n
  3. 0003intro c
  4. 0004intro B
  5. 0005intro C
  6. 0006intro D
  7. 0007intro E
  8. 0008split
  9. 0009intro i
  10. 0010intro hi
  11. 0011exfalso
  12. 0012specialize lt_not_le (i)
  13. 0013specialize lt_not_le (0)
  14. 0014apply lt_not_le
  15. 0015exact hi
  16. 0016specialize zero_le (i)
  17. 0017apply zero_le
  18. 0018split
  19. 0019intro i
  20. 0020intro h
  21. 0021intro b
  22. 0022intro e
  23. 0023intro d
  24. 0024intro f
  25. 0025intro hi
  26. 0026intro hh
  27. 0027intro he
  28. 0028intro hf
  29. 0029intro heq
  30. 0030exfalso
  31. 0031specialize lt_not_le (i)
  32. 0032specialize lt_not_le (0)
  33. 0033apply lt_not_le
  34. 0034exact hi
  35. 0035specialize zero_le (i)
  36. 0036apply zero_le
  37. 0037intro z
  38. 0038intro hz
  39. 0039intro hb
  40. 0040intro hp
  41. 0041exfalso
  42. 0042specialize lt_not_le (z)
  43. 0043specialize lt_not_le (0)
  44. 0044apply lt_not_le
  45. 0045exact hz
  46. 0046specialize zero_le (z)
  47. 0047apply zero_le