JT0036

jordan_rectangle_flat_bound

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

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

∀ u. ∀ v. ∀ i. ∀ j. Lt(i,u) → Lt(j,v) → Lt(v · i + j,u · v)

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

Definition DAG

Le(a,b) · 1Lt(a,b) · 4

Actual proof prerequisites

finite_add_lt_of_le_of_lt · checked external prerequisitele_refl · checked external prerequisitelt_of_lt_of_le · checked external prerequisitemul_le_mul_right · checked external prerequisitemul_comm · checked external prerequisite
Original expanded first-order 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))

Complete tactic proof in conservative notation

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

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.

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–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 : Lt(v · i + j,v · i + v)Definitions: Lt(v · i + j,v · i + v)Original native command in the exact edition
  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 : Le(S i · v,u · v)Definitions: Le(S i · v,u · v)Original native command in the exact edition
  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 defined 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 : Lt(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 : Le(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