SS001B

divisor_signed_table_reindex_exists

Any actual finite signed table admits a genuinely beta-coded pullback along an actual beta map, with its new table code constructed.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

These are actual signed-table and finite-sum foundations. Equality compares represented signed values, not arbitrary encodings. MatrixMinorFourCode is reused solely as generic nested pairing, without a matrix hypothesis. Full finite signed G007 is established separately in the Möbius-inversion family.

Exact theorem in conservative defined notation

∀ N. ∀ F. ∀ r. ∀ s. ∀ l. ArithTable(N,F) → ∃ x. ArithTable(l,x) ∧ ArithReindex(F,x,r,s,l)

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

Definition DAG

MatrixMinorFourCode(z,up,us,un,ut) · 1ArithTable(N,F) · 2ArithReindex(F,G,r,s,l) · 1Lt(a,b) · 2BetaAt(b,c,i,x) · 6

Actual proof prerequisites

divisor_signed_table_componentsdivisor_signed_table_reindex_data_existsdivisor_signed_table_from_componentsdivisor_signed_table_reindex_from_components
Original expanded first-order statement 
forall N F r s l. (exists dst_positive_code_constructed_source dst_positive_scale_constructed_source dst_negative_code_constructed_source dst_negative_scale_constructed_source. (((F) = (((((dst_positive_code_constructed_source) + (dst_positive_scale_constructed_source)) * S ((dst_positive_code_constructed_source) + (dst_positive_scale_constructed_source)) + ((dst_positive_scale_constructed_source) + (dst_positive_scale_constructed_source))) + (((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) * S ((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) + ((dst_negative_scale_constructed_source) + (dst_negative_scale_constructed_source)))) * S ((((dst_positive_code_constructed_source) + (dst_positive_scale_constructed_source)) * S ((dst_positive_code_constructed_source) + (dst_positive_scale_constructed_source)) + ((dst_positive_scale_constructed_source) + (dst_positive_scale_constructed_source))) + (((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) * S ((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) + ((dst_negative_scale_constructed_source) + (dst_negative_scale_constructed_source)))) + ((((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) * S ((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) + ((dst_negative_scale_constructed_source) + (dst_negative_scale_constructed_source))) + (((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) * S ((dst_negative_code_constructed_source) + (dst_negative_scale_constructed_source)) + ((dst_negative_scale_constructed_source) + (dst_negative_scale_constructed_source)))))) /\ (forall dst_index_constructed_source. (exists pvs_le_gap_constructed_sourcedomain. pvs_le_gap_constructed_sourcedomain + (dst_index_constructed_source) = (N)) -> exists dst_positive_constructed_source dst_negative_constructed_source dst_value_constructed_source. ((((exists ff_h_pvs_constructed_sourceentrypositive. ff_h_pvs_constructed_sourceentrypositive + S (dst_positive_constructed_source) = S ((S (dst_index_constructed_source)) * dst_positive_scale_constructed_source)) /\ exists ff_q_pvs_constructed_sourceentrypositive. dst_positive_code_constructed_source = ff_q_pvs_constructed_sourceentrypositive * S ((S (dst_index_constructed_source)) * dst_positive_scale_constructed_source) + (dst_positive_constructed_source))) /\ (((((exists ff_h_pvs_constructed_sourceentrynegative. ff_h_pvs_constructed_sourceentrynegative + S (dst_negative_constructed_source) = S ((S (dst_index_constructed_source)) * dst_negative_scale_constructed_source)) /\ exists ff_q_pvs_constructed_sourceentrynegative. dst_negative_code_constructed_source = ff_q_pvs_constructed_sourceentrynegative * S ((S (dst_index_constructed_source)) * dst_negative_scale_constructed_source) + (dst_negative_constructed_source))) /\ (exists ge_balance_positive_constructed_sourceentryvalue ge_balance_negative_constructed_sourceentryvalue. (((((dst_value_constructed_source) = 2 * (ge_balance_positive_constructed_sourceentryvalue) /\ (ge_balance_negative_constructed_sourceentryvalue) = 0) \/ exists ge_signed_half_constructed_sourceentryvaluedecode. (((dst_value_constructed_source) = 2 * ge_signed_half_constructed_sourceentryvaluedecode + 1 /\ (ge_balance_positive_constructed_sourceentryvalue) = 0) /\ (ge_balance_negative_constructed_sourceentryvalue) = S ge_signed_half_constructed_sourceentryvaluedecode))) /\ ((dst_positive_constructed_source) + ge_balance_negative_constructed_sourceentryvalue = (dst_negative_constructed_source) + ge_balance_positive_constructed_sourceentryvalue))))))))) -> exists G. (exists dst_positive_code_constructed_target dst_positive_scale_constructed_target dst_negative_code_constructed_target dst_negative_scale_constructed_target. (((G) = (((((dst_positive_code_constructed_target) + (dst_positive_scale_constructed_target)) * S ((dst_positive_code_constructed_target) + (dst_positive_scale_constructed_target)) + ((dst_positive_scale_constructed_target) + (dst_positive_scale_constructed_target))) + (((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) * S ((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) + ((dst_negative_scale_constructed_target) + (dst_negative_scale_constructed_target)))) * S ((((dst_positive_code_constructed_target) + (dst_positive_scale_constructed_target)) * S ((dst_positive_code_constructed_target) + (dst_positive_scale_constructed_target)) + ((dst_positive_scale_constructed_target) + (dst_positive_scale_constructed_target))) + (((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) * S ((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) + ((dst_negative_scale_constructed_target) + (dst_negative_scale_constructed_target)))) + ((((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) * S ((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) + ((dst_negative_scale_constructed_target) + (dst_negative_scale_constructed_target))) + (((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) * S ((dst_negative_code_constructed_target) + (dst_negative_scale_constructed_target)) + ((dst_negative_scale_constructed_target) + (dst_negative_scale_constructed_target)))))) /\ (forall dst_index_constructed_target. (exists pvs_le_gap_constructed_targetdomain. pvs_le_gap_constructed_targetdomain + (dst_index_constructed_target) = (l)) -> exists dst_positive_constructed_target dst_negative_constructed_target dst_value_constructed_target. ((((exists ff_h_pvs_constructed_targetentrypositive. ff_h_pvs_constructed_targetentrypositive + S (dst_positive_constructed_target) = S ((S (dst_index_constructed_target)) * dst_positive_scale_constructed_target)) /\ exists ff_q_pvs_constructed_targetentrypositive. dst_positive_code_constructed_target = ff_q_pvs_constructed_targetentrypositive * S ((S (dst_index_constructed_target)) * dst_positive_scale_constructed_target) + (dst_positive_constructed_target))) /\ (((((exists ff_h_pvs_constructed_targetentrynegative. ff_h_pvs_constructed_targetentrynegative + S (dst_negative_constructed_target) = S ((S (dst_index_constructed_target)) * dst_negative_scale_constructed_target)) /\ exists ff_q_pvs_constructed_targetentrynegative. dst_negative_code_constructed_target = ff_q_pvs_constructed_targetentrynegative * S ((S (dst_index_constructed_target)) * dst_negative_scale_constructed_target) + (dst_negative_constructed_target))) /\ (exists ge_balance_positive_constructed_targetentryvalue ge_balance_negative_constructed_targetentryvalue. (((((dst_value_constructed_target) = 2 * (ge_balance_positive_constructed_targetentryvalue) /\ (ge_balance_negative_constructed_targetentryvalue) = 0) \/ exists ge_signed_half_constructed_targetentryvaluedecode. (((dst_value_constructed_target) = 2 * ge_signed_half_constructed_targetentryvaluedecode + 1 /\ (ge_balance_positive_constructed_targetentryvalue) = 0) /\ (ge_balance_negative_constructed_targetentryvalue) = S ge_signed_half_constructed_targetentryvaluedecode))) /\ ((dst_positive_constructed_target) + ge_balance_negative_constructed_targetentryvalue = (dst_negative_constructed_target) + ge_balance_positive_constructed_targetentryvalue))))))))) /\ (forall dsr_index_constructed_reindex dsr_image_constructed_reindex dsr_value_constructed_reindex. (exists pvs_gap_constructed_reindexbound. pvs_gap_constructed_reindexbound + S (dsr_index_constructed_reindex) = (l)) -> (((exists ff_h_pvs_constructed_reindexmap. ff_h_pvs_constructed_reindexmap + S (dsr_image_constructed_reindex) = S ((S (dsr_index_constructed_reindex)) * s)) /\ exists ff_q_pvs_constructed_reindexmap. r = ff_q_pvs_constructed_reindexmap * S ((S (dsr_index_constructed_reindex)) * s) + (dsr_image_constructed_reindex))) -> (exists dst_positive_code_constructed_reindexsource dst_positive_scale_constructed_reindexsource dst_negative_code_constructed_reindexsource dst_negative_scale_constructed_reindexsource dst_positive_constructed_reindexsource dst_negative_constructed_reindexsource. (((F) = (((((dst_positive_code_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource)) * S ((dst_positive_code_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource)) + ((dst_positive_scale_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource))) + (((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) * S ((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) + ((dst_negative_scale_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)))) * S ((((dst_positive_code_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource)) * S ((dst_positive_code_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource)) + ((dst_positive_scale_constructed_reindexsource) + (dst_positive_scale_constructed_reindexsource))) + (((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) * S ((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) + ((dst_negative_scale_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)))) + ((((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) * S ((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) + ((dst_negative_scale_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource))) + (((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) * S ((dst_negative_code_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)) + ((dst_negative_scale_constructed_reindexsource) + (dst_negative_scale_constructed_reindexsource)))))) /\ (((((exists ff_h_pvs_constructed_reindexsourcepositive. ff_h_pvs_constructed_reindexsourcepositive + S (dst_positive_constructed_reindexsource) = S ((S (dsr_image_constructed_reindex)) * dst_positive_scale_constructed_reindexsource)) /\ exists ff_q_pvs_constructed_reindexsourcepositive. dst_positive_code_constructed_reindexsource = ff_q_pvs_constructed_reindexsourcepositive * S ((S (dsr_image_constructed_reindex)) * dst_positive_scale_constructed_reindexsource) + (dst_positive_constructed_reindexsource))) /\ (((((exists ff_h_pvs_constructed_reindexsourcenegative. ff_h_pvs_constructed_reindexsourcenegative + S (dst_negative_constructed_reindexsource) = S ((S (dsr_image_constructed_reindex)) * dst_negative_scale_constructed_reindexsource)) /\ exists ff_q_pvs_constructed_reindexsourcenegative. dst_negative_code_constructed_reindexsource = ff_q_pvs_constructed_reindexsourcenegative * S ((S (dsr_image_constructed_reindex)) * dst_negative_scale_constructed_reindexsource) + (dst_negative_constructed_reindexsource))) /\ (exists ge_balance_positive_constructed_reindexsourcevalue ge_balance_negative_constructed_reindexsourcevalue. (((((dsr_value_constructed_reindex) = 2 * (ge_balance_positive_constructed_reindexsourcevalue) /\ (ge_balance_negative_constructed_reindexsourcevalue) = 0) \/ exists ge_signed_half_constructed_reindexsourcevaluedecode. (((dsr_value_constructed_reindex) = 2 * ge_signed_half_constructed_reindexsourcevaluedecode + 1 /\ (ge_balance_positive_constructed_reindexsourcevalue) = 0) /\ (ge_balance_negative_constructed_reindexsourcevalue) = S ge_signed_half_constructed_reindexsourcevaluedecode))) /\ ((dst_positive_constructed_reindexsource) + ge_balance_negative_constructed_reindexsourcevalue = (dst_negative_constructed_reindexsource) + ge_balance_positive_constructed_reindexsourcevalue))))))))) -> (exists dst_positive_code_constructed_reindextarget dst_positive_scale_constructed_reindextarget dst_negative_code_constructed_reindextarget dst_negative_scale_constructed_reindextarget dst_positive_constructed_reindextarget dst_negative_constructed_reindextarget. (((G) = (((((dst_positive_code_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget)) * S ((dst_positive_code_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget)) + ((dst_positive_scale_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget))) + (((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) * S ((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) + ((dst_negative_scale_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)))) * S ((((dst_positive_code_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget)) * S ((dst_positive_code_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget)) + ((dst_positive_scale_constructed_reindextarget) + (dst_positive_scale_constructed_reindextarget))) + (((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) * S ((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) + ((dst_negative_scale_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)))) + ((((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) * S ((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) + ((dst_negative_scale_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget))) + (((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) * S ((dst_negative_code_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)) + ((dst_negative_scale_constructed_reindextarget) + (dst_negative_scale_constructed_reindextarget)))))) /\ (((((exists ff_h_pvs_constructed_reindextargetpositive. ff_h_pvs_constructed_reindextargetpositive + S (dst_positive_constructed_reindextarget) = S ((S (dsr_index_constructed_reindex)) * dst_positive_scale_constructed_reindextarget)) /\ exists ff_q_pvs_constructed_reindextargetpositive. dst_positive_code_constructed_reindextarget = ff_q_pvs_constructed_reindextargetpositive * S ((S (dsr_index_constructed_reindex)) * dst_positive_scale_constructed_reindextarget) + (dst_positive_constructed_reindextarget))) /\ (((((exists ff_h_pvs_constructed_reindextargetnegative. ff_h_pvs_constructed_reindextargetnegative + S (dst_negative_constructed_reindextarget) = S ((S (dsr_index_constructed_reindex)) * dst_negative_scale_constructed_reindextarget)) /\ exists ff_q_pvs_constructed_reindextargetnegative. dst_negative_code_constructed_reindextarget = ff_q_pvs_constructed_reindextargetnegative * S ((S (dsr_index_constructed_reindex)) * dst_negative_scale_constructed_reindextarget) + (dst_negative_constructed_reindextarget))) /\ (exists ge_balance_positive_constructed_reindextargetvalue ge_balance_negative_constructed_reindextargetvalue. (((((dsr_value_constructed_reindex) = 2 * (ge_balance_positive_constructed_reindextargetvalue) /\ (ge_balance_negative_constructed_reindextargetvalue) = 0) \/ exists ge_signed_half_constructed_reindextargetvaluedecode. (((dsr_value_constructed_reindex) = 2 * ge_signed_half_constructed_reindextargetvaluedecode + 1 /\ (ge_balance_positive_constructed_reindextargetvalue) = 0) /\ (ge_balance_negative_constructed_reindextargetvalue) = S ge_signed_half_constructed_reindextargetvaluedecode))) /\ ((dst_positive_constructed_reindextarget) + ge_balance_negative_constructed_reindextargetvalue = (dst_negative_constructed_reindextarget) + ge_balance_positive_constructed_reindextargetvalue))))))))))

Complete tactic proof in conservative notation

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

55 script commands · 13 reading checkpoints · 2 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.

Named ingredients (4)
divisor signed table componentsdivisor signed table reindex data existsdivisor signed table from componentsdivisor signed table reindex from components
01Fix variables and assumptionsL1–6

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro l
  6. L6
    intro ht
02Establish hrepL7–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table components.

  1. L7
    have hrep : ∃ pb. ∃ pc. ∃ nb. ∃ nc. MatrixMinorFourCode(F,pb,pc,nb,nc)Definitions: MatrixMinorFourCode(F,pb,pc,nb,nc)Original native command in the exact edition
  2. L8
    specialize divisor_signed_table_components (N)
  3. L9
    specialize divisor_signed_table_components (F)
  4. L10
    apply divisor_signed_table_components
  5. L11
    exact ht
03Separate the logical casesL12–15

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

  1. L12
    cases hrep
  2. L13
    cases hrep_witness
  3. L14
    cases hrep_witness_witness
  4. L15
    cases hrep_witness_witness_witness
04Establish hdataL16–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table reindex data exists.

  1. L16
    have hdata : ∃ qb. ∃ qc. ∃ mb. ∃ mc. (∀ y. ∀ z. ∀ n. Lt(y,l) → BetaAt(r,s,y,z) → BetaAt(x,x1,z,n) → BetaAt(qb,qc,y,n)) ∧ (∀ y. ∀ z. ∀ n. Lt(y,l) → BetaAt(r,s,y,z) → BetaAt(x2,x3,z,n) → BetaAt(mb,mc,y,n))Definitions: Lt(y,l)BetaAt(r,s,y,z)BetaAt(x,x1,z,n)BetaAt(qb,qc,y,n)BetaAt(x2,x3,z,n)BetaAt(mb,mc,y,n)Original native command in the exact edition
  2. L17
    specialize divisor_signed_table_reindex_data_exists (x)
  3. L18
    specialize divisor_signed_table_reindex_data_exists (x1)
  4. L19
    specialize divisor_signed_table_reindex_data_exists (x2)
  5. L20
    specialize divisor_signed_table_reindex_data_exists (x3)
  6. L21
    specialize divisor_signed_table_reindex_data_exists (r)
  7. L22
    specialize divisor_signed_table_reindex_data_exists (s)
  8. L23
    specialize divisor_signed_table_reindex_data_exists (l)
  9. L24
    apply divisor_signed_table_reindex_data_exists
05Separate the logical casesL25–28

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

  1. L25
    cases hdata
  2. L26
    cases hdata_witness
  3. L27
    cases hdata_witness_witness
  4. L28
    cases hdata_witness_witness_witness
06Construct an explicit witnessL29–29

Supply the displayed value, then prove that it has the required property.

  1. L29
    exists ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))))
07Separate the logical casesL30–30

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

  1. L30
    split
08Use earlier factsL31–37

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

  1. L31
    specialize divisor_signed_table_from_components (l)
  2. L32
    specialize divisor_signed_table_from_components (((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))))
  3. L33
    specialize divisor_signed_table_from_components (x4)
  4. L34
    specialize divisor_signed_table_from_components (x5)
  5. L35
    specialize divisor_signed_table_from_components (x6)
  6. L36
    specialize divisor_signed_table_from_components (x7)
  7. L37
    apply divisor_signed_table_from_components
09Calculate and transport equalitiesL38–38

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

  1. L38
    refl
10Use earlier factsL39–48

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

  1. L39
    specialize divisor_signed_table_reindex_from_components (F)
  2. L40
    specialize divisor_signed_table_reindex_from_components (((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))))
  3. L41
    specialize divisor_signed_table_reindex_from_components (x)
  4. L42
    specialize divisor_signed_table_reindex_from_components (x1)
  5. L43
    specialize divisor_signed_table_reindex_from_components (x2)
  6. L44
    specialize divisor_signed_table_reindex_from_components (x3)
  7. L45
    specialize divisor_signed_table_reindex_from_components (x4)
  8. L46
    specialize divisor_signed_table_reindex_from_components (x5)
  9. L47
    specialize divisor_signed_table_reindex_from_components (x6)
  10. L48
    specialize divisor_signed_table_reindex_from_components (x7)
11Use earlier factsL49–53

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

  1. L49
    specialize divisor_signed_table_reindex_from_components (r)
  2. L50
    specialize divisor_signed_table_reindex_from_components (s)
  3. L51
    specialize divisor_signed_table_reindex_from_components (l)
  4. L52
    apply divisor_signed_table_reindex_from_components
  5. L53
    exact hrep_witness_witness_witness_witness
12Calculate and transport equalitiesL54–54

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

  1. L54
    refl
13Use earlier factsL55–55

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

  1. L55
    exact hdata_witness_witness_witness_witness

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro r
  4. 0004intro s
  5. 0005intro l
  6. 0006intro ht
  7. 0007have hrep : ∃ pb. ∃ pc. ∃ nb. ∃ nc. MatrixMinorFourCode(F,pb,pc,nb,nc)
  8. 0008specialize divisor_signed_table_components (N)
  9. 0009specialize divisor_signed_table_components (F)
  10. 0010apply divisor_signed_table_components
  11. 0011exact ht
  12. 0012cases hrep
  13. 0013cases hrep_witness
  14. 0014cases hrep_witness_witness
  15. 0015cases hrep_witness_witness_witness
  16. 0016have hdata : ∃ qb. ∃ qc. ∃ mb. ∃ mc. (∀ y. ∀ z. ∀ n. Lt(y,l) → BetaAt(r,s,y,z) → BetaAt(x,x1,z,n) → BetaAt(qb,qc,y,n)) ∧ (∀ y. ∀ z. ∀ n. Lt(y,l) → BetaAt(r,s,y,z) → BetaAt(x2,x3,z,n) → BetaAt(mb,mc,y,n))
  17. 0017specialize divisor_signed_table_reindex_data_exists (x)
  18. 0018specialize divisor_signed_table_reindex_data_exists (x1)
  19. 0019specialize divisor_signed_table_reindex_data_exists (x2)
  20. 0020specialize divisor_signed_table_reindex_data_exists (x3)
  21. 0021specialize divisor_signed_table_reindex_data_exists (r)
  22. 0022specialize divisor_signed_table_reindex_data_exists (s)
  23. 0023specialize divisor_signed_table_reindex_data_exists (l)
  24. 0024apply divisor_signed_table_reindex_data_exists
  25. 0025cases hdata
  26. 0026cases hdata_witness
  27. 0027cases hdata_witness_witness
  28. 0028cases hdata_witness_witness_witness
  29. 0029exists ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))))
  30. 0030split
  31. 0031specialize divisor_signed_table_from_components (l)
  32. 0032specialize divisor_signed_table_from_components (((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))))
  33. 0033specialize divisor_signed_table_from_components (x4)
  34. 0034specialize divisor_signed_table_from_components (x5)
  35. 0035specialize divisor_signed_table_from_components (x6)
  36. 0036specialize divisor_signed_table_from_components (x7)
  37. 0037apply divisor_signed_table_from_components
  38. 0038refl
  39. 0039specialize divisor_signed_table_reindex_from_components (F)
  40. 0040specialize divisor_signed_table_reindex_from_components (((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) * S ((((x4) + (x5)) * S ((x4) + (x5)) + ((x5) + (x5))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))) + ((((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7))) + (((x6) + (x7)) * S ((x6) + (x7)) + ((x7) + (x7)))))
  41. 0041specialize divisor_signed_table_reindex_from_components (x)
  42. 0042specialize divisor_signed_table_reindex_from_components (x1)
  43. 0043specialize divisor_signed_table_reindex_from_components (x2)
  44. 0044specialize divisor_signed_table_reindex_from_components (x3)
  45. 0045specialize divisor_signed_table_reindex_from_components (x4)
  46. 0046specialize divisor_signed_table_reindex_from_components (x5)
  47. 0047specialize divisor_signed_table_reindex_from_components (x6)
  48. 0048specialize divisor_signed_table_reindex_from_components (x7)
  49. 0049specialize divisor_signed_table_reindex_from_components (r)
  50. 0050specialize divisor_signed_table_reindex_from_components (s)
  51. 0051specialize divisor_signed_table_reindex_from_components (l)
  52. 0052apply divisor_signed_table_reindex_from_components
  53. 0053exact hrep_witness_witness_witness_witness
  54. 0054refl
  55. 0055exact hdata_witness_witness_witness_witness