JT004E

jordan_enumeration_index_map_empty

The zero-length index map is vacuous, independently of target length.

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. ∀ A. ∀ B. ∀ C. ∀ D. ∀ E. ∀ F. ∀ G. ∀ H. ∀ Z. ∀ W. ∀ v. ∀ x. Lt(x,0) → ∃ y. BetaAt(Z,W,x,y) ∧ (Lt(y,v) ∧ (∀ z. ∀ n. ∀ m. ∀ i. BetaAt(A,B,x,z) ∧ BetaAt(C,D,x,n) → BetaAt(E,F,y,m) ∧ BetaAt(G,H,y,i) → IntegerVectorZero(z,n,m,i,k)))

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

Definition DAG

IntegerVectorZero(ab,ac,db,dc,l) · 1Lt(a,b) · 2BetaAt(b,c,i,x) · 5

Actual proof prerequisites

lt_not_le · checked external prerequisitezero_le · checked external prerequisite
Original expanded first-order statement 
forall k A B C D E F G H Z W v. (forall jt_index_empty_map. (exists jt_gap_empty_mapindex. jt_gap_empty_mapindex+S (jt_index_empty_map)=(0)) -> exists jt_image_empty_map. ((((exists fs_h_jt_empty_mapat. fs_h_jt_empty_mapat + S (jt_image_empty_map) = S ((S (jt_index_empty_map)) * W)) /\ exists fs_q_jt_empty_mapat. Z = fs_q_jt_empty_mapat * S ((S (jt_index_empty_map)) * W) + (jt_image_empty_map))) /\ (((exists jt_gap_empty_mapbound. jt_gap_empty_mapbound+S (jt_image_empty_map)=(v)) /\ (forall jt_b_empty_mapmatch jt_c_empty_mapmatch jt_d_empty_mapmatch jt_e_empty_mapmatch. (((((exists fs_h_jt_empty_mapmatchleftcode. fs_h_jt_empty_mapmatchleftcode + S (jt_b_empty_mapmatch) = S ((S (jt_index_empty_map)) * B)) /\ exists fs_q_jt_empty_mapmatchleftcode. A = fs_q_jt_empty_mapmatchleftcode * S ((S (jt_index_empty_map)) * B) + (jt_b_empty_mapmatch))) /\ (((exists fs_h_jt_empty_mapmatchleftscale. fs_h_jt_empty_mapmatchleftscale + S (jt_c_empty_mapmatch) = S ((S (jt_index_empty_map)) * D)) /\ exists fs_q_jt_empty_mapmatchleftscale. C = fs_q_jt_empty_mapmatchleftscale * S ((S (jt_index_empty_map)) * D) + (jt_c_empty_mapmatch))))) -> (((((exists fs_h_jt_empty_mapmatchrightcode. fs_h_jt_empty_mapmatchrightcode + S (jt_d_empty_mapmatch) = S ((S (jt_image_empty_map)) * F)) /\ exists fs_q_jt_empty_mapmatchrightcode. E = fs_q_jt_empty_mapmatchrightcode * S ((S (jt_image_empty_map)) * F) + (jt_d_empty_mapmatch))) /\ (((exists fs_h_jt_empty_mapmatchrightscale. fs_h_jt_empty_mapmatchrightscale + S (jt_e_empty_mapmatch) = S ((S (jt_image_empty_map)) * H)) /\ exists fs_q_jt_empty_mapmatchrightscale. G = fs_q_jt_empty_mapmatchrightscale * S ((S (jt_image_empty_map)) * H) + (jt_e_empty_mapmatch))))) -> (forall jt_index_empty_mapmatchequal jt_left_empty_mapmatchequal jt_right_empty_mapmatchequal. (exists jt_gap_empty_mapmatchequalindex. jt_gap_empty_mapmatchequalindex+S (jt_index_empty_mapmatchequal)=(k)) -> (((exists fs_h_jt_empty_mapmatchequalleft. fs_h_jt_empty_mapmatchequalleft + S (jt_left_empty_mapmatchequal) = S ((S (jt_index_empty_mapmatchequal)) * jt_c_empty_mapmatch)) /\ exists fs_q_jt_empty_mapmatchequalleft. jt_b_empty_mapmatch = fs_q_jt_empty_mapmatchequalleft * S ((S (jt_index_empty_mapmatchequal)) * jt_c_empty_mapmatch) + (jt_left_empty_mapmatchequal))) -> (((exists fs_h_jt_empty_mapmatchequalright. fs_h_jt_empty_mapmatchequalright + S (jt_right_empty_mapmatchequal) = S ((S (jt_index_empty_mapmatchequal)) * jt_e_empty_mapmatch)) /\ exists fs_q_jt_empty_mapmatchequalright. jt_d_empty_mapmatch = fs_q_jt_empty_mapmatchequalright * S ((S (jt_index_empty_mapmatchequal)) * jt_e_empty_mapmatch) + (jt_right_empty_mapmatchequal))) -> jt_left_empty_mapmatchequal=jt_right_empty_mapmatchequal))))))

Complete tactic proof in conservative notation

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

21 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–10

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

  1. L1
    intro k
  2. L2
    intro A
  3. L3
    intro B
  4. L4
    intro C
  5. L5
    intro D
  6. L6
    intro E
  7. L7
    intro F
  8. L8
    intro G
  9. L9
    intro H
  10. L10
    intro Z
02Fix variables and assumptionsL11–14

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

  1. L11
    intro W
  2. L12
    intro v
  3. L13
    intro i
  4. L14
    intro hi
03Separate the logical casesL15–15

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

  1. L15
    exfalso
04Use earlier factsL16–21

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

  1. L16
    specialize lt_not_le (i)
  2. L17
    specialize lt_not_le (0)
  3. L18
    apply lt_not_le
  4. L19
    exact hi
  5. L20
    specialize zero_le (i)
  6. L21
    apply zero_le

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro k
  2. 0002intro A
  3. 0003intro B
  4. 0004intro C
  5. 0005intro D
  6. 0006intro E
  7. 0007intro F
  8. 0008intro G
  9. 0009intro H
  10. 0010intro Z
  11. 0011intro W
  12. 0012intro v
  13. 0013intro i
  14. 0014intro hi
  15. 0015exfalso
  16. 0016specialize lt_not_le (i)
  17. 0017specialize lt_not_le (0)
  18. 0018apply lt_not_le
  19. 0019exact hi
  20. 0020specialize zero_le (i)
  21. 0021apply zero_le