JT0037

jordan_rectangle_pair_unique

Actual bounded quotient/remainder decomposition uniquely recovers both indices.

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

∀ v. ∀ i. ∀ j. ∀ r. ∀ s. Lt(j,v) → Lt(s,v) → v · i + j = v · r + s → i = r ∧ j = s

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

Definition DAG

Lt(a,b) · 2

Actual proof prerequisites

division_remainder_unique · checked external prerequisite
Original expanded first-order statement 
forall v i j r s. (exists jt_gap_uniquecolumn. jt_gap_uniquecolumn+S (j)=(v)) -> (exists jt_gap_uniqueother. jt_gap_uniqueother+S (s)=(v)) -> v*i+j=v*r+s -> (i=r /\ j=s)

Complete tactic proof in conservative notation

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

19 script commands · 4 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–8

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

  1. L1
    intro v
  2. L2
    intro i
  3. L3
    intro j
  4. L4
    intro r
  5. L5
    intro s
  6. L6
    intro hj
  7. L7
    intro hs
  8. L8
    intro heq
02Use earlier factsL9–15

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

  1. L9
    specialize division_remainder_unique (v)
  2. L10
    specialize division_remainder_unique (v*i+j)
  3. L11
    specialize division_remainder_unique (i)
  4. L12
    specialize division_remainder_unique (j)
  5. L13
    specialize division_remainder_unique (r)
  6. L14
    specialize division_remainder_unique (s)
  7. L15
    apply division_remainder_unique
03Calculate and transport equalitiesL16–16

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

  1. L16
    refl
04Use earlier factsL17–19

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

  1. L17
    exact hj
  2. L18
    exact heq
  3. L19
    exact hs

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro v
  2. 0002intro i
  3. 0003intro j
  4. 0004intro r
  5. 0005intro s
  6. 0006intro hj
  7. 0007intro hs
  8. 0008intro heq
  9. 0009specialize division_remainder_unique (v)
  10. 0010specialize division_remainder_unique (v*i+j)
  11. 0011specialize division_remainder_unique (i)
  12. 0012specialize division_remainder_unique (j)
  13. 0013specialize division_remainder_unique (r)
  14. 0014specialize division_remainder_unique (s)
  15. 0015apply division_remainder_unique
  16. 0016refl
  17. 0017exact hj
  18. 0018exact heq
  19. 0019exact hs