JT0036

jordan_rectangle_flat_bound

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

Every actual pair of bounded indices has a row-major index below the literal product.

Exact expanded first-order arithmetic statement

forall u v i j. (exists jt_gap_flatrow. jt_gap_flatrow+S (i)=(u)) -> (exists jt_gap_flatcolumn. jt_gap_flatcolumn+S (j)=(v)) -> (exists jt_gap_flatresult. jt_gap_flatresult+S (v*i+j)=(u*v))

Constructive proof overview

Generated structural guide

Every actual pair of bounded indices has a row-major index below the literal product.

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

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

Proof neighborhood

Direct dependencies

finite_add_lt_of_le_of_lt Alpha theorem; checked-use authorized le_refl Alpha theorem; checked-use authorized lt_of_lt_of_le Alpha theorem; checked-use authorized mul_le_mul_right Alpha theorem; checked-use authorized mul_comm Alpha theorem; checked-use authorized

Direct dependents

JT0044 jordan_rectangle_crt_pair_value JT0047 jordan_rectangle_crt_covers

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

35 script commands · 6 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro u
  2. L2
    intro v
  3. L3
    intro i
  4. L4
    intro j
  5. L5
    intro hi
  6. L6
    intro hj
02Establish hsL7–16

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

  1. L7
    have hs : exists jt_gap_flatadd. jt_gap_flatadd+S (v*i+j)=(v*i+v)
  2. L8
    specialize finite_add_lt_of_le_of_lt (v*i)
  3. L9
    specialize finite_add_lt_of_le_of_lt (v*i)
  4. L10
    specialize finite_add_lt_of_le_of_lt (j)
  5. L11
    specialize finite_add_lt_of_le_of_lt (v)
  6. L12
    apply finite_add_lt_of_le_of_lt
  7. L13
    specialize le_refl (v*i)
  8. L14
    apply le_refl
  9. L15
    exact hj
  10. L16
    specialize lt_of_lt_of_le (v*i+j)
03Use earlier factsL17–20

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

  1. L17
    specialize lt_of_lt_of_le (v*i+v)
  2. L18
    specialize lt_of_lt_of_le (u*v)
  3. L19
    apply lt_of_lt_of_le
  4. L20
    exact hs
04Establish hmL21–26

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

  1. L21
    have hm : exists jt_gap_flatmult. jt_gap_flatmult+(S i*v)=(u*v)
  2. L22
    specialize mul_le_mul_right (S i)
  3. L23
    specialize mul_le_mul_right (u)
  4. L24
    specialize mul_le_mul_right (v)
  5. L25
    apply mul_le_mul_right
  6. L26
    exact hi
05Establish hcommL27–31

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

  1. L27
    have hcomm : S i*v=v*S i
  2. L28
    specialize mul_comm (S i)
  3. L29
    specialize mul_comm (v)
  4. L30
    apply mul_comm
  5. L31
    rewrite hcomm at hm
06Establish hstepL32–35

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

  1. L32
    have hstep : v*S i=v*i+v
  2. L33
    apply PA6
  3. L34
    rewrite hstep at hm
  4. L35
    exact hm

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro u
  2. 0002intro v
  3. 0003intro i
  4. 0004intro j
  5. 0005intro hi
  6. 0006intro hj
  7. 0007have hs : exists jt_gap_flatadd. jt_gap_flatadd+S (v*i+j)=(v*i+v)
  8. 0008specialize finite_add_lt_of_le_of_lt (v*i)
  9. 0009specialize finite_add_lt_of_le_of_lt (v*i)
  10. 0010specialize finite_add_lt_of_le_of_lt (j)
  11. 0011specialize finite_add_lt_of_le_of_lt (v)
  12. 0012apply finite_add_lt_of_le_of_lt
  13. 0013specialize le_refl (v*i)
  14. 0014apply le_refl
  15. 0015exact hj
  16. 0016specialize lt_of_lt_of_le (v*i+j)
  17. 0017specialize lt_of_lt_of_le (v*i+v)
  18. 0018specialize lt_of_lt_of_le (u*v)
  19. 0019apply lt_of_lt_of_le
  20. 0020exact hs
  21. 0021have hm : exists jt_gap_flatmult. jt_gap_flatmult+(S i*v)=(u*v)
  22. 0022specialize mul_le_mul_right (S i)
  23. 0023specialize mul_le_mul_right (u)
  24. 0024specialize mul_le_mul_right (v)
  25. 0025apply mul_le_mul_right
  26. 0026exact hi
  27. 0027have hcomm : S i*v=v*S i
  28. 0028specialize mul_comm (S i)
  29. 0029specialize mul_comm (v)
  30. 0030apply mul_comm
  31. 0031rewrite hcomm at hm
  32. 0032have hstep : v*S i=v*i+v
  33. 0033apply PA6
  34. 0034rewrite hstep at hm
  35. 0035exact hm