DV000A

mobius_table_exists

Ordinary induction constructs a genuine packed Möbius table for every finite bound, using independently proved positive-input μ totality at each step.

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.

A genuine divisor mask has S n entries, indexed zero through n, and forces its zeroth entry to zero regardless of F(0). Möbius values remain positive-domain only. This family constructs divisor sums and Möbius tables; cancellation and the full G007 endpoint are separately proved later in the same release.

Exact theorem in conservative defined notation

∀ N. ∃ M. MobiusTable(N,M)

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

Definition DAG

Mobius(n,z) · 1ArithTable(N,F) · 1ArithAt(F,i,z) · 1ArithTableEqual(F,G,l) · 1MobiusTable(N,M) · 2

Actual proof prerequisites

arithmetic_signed_table_singletonmobius_table_zero_constructormobius_value_exists · checked external prerequisitemobius_table_append
Original expanded first-order statement 
forall N. exists M. (((exists dst_positive_code_exists_resulttable dst_positive_scale_exists_resulttable dst_negative_code_exists_resulttable dst_negative_scale_exists_resulttable. (((M) = (((((dst_positive_code_exists_resulttable) + (dst_positive_scale_exists_resulttable)) * S ((dst_positive_code_exists_resulttable) + (dst_positive_scale_exists_resulttable)) + ((dst_positive_scale_exists_resulttable) + (dst_positive_scale_exists_resulttable))) + (((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) * S ((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) + ((dst_negative_scale_exists_resulttable) + (dst_negative_scale_exists_resulttable)))) * S ((((dst_positive_code_exists_resulttable) + (dst_positive_scale_exists_resulttable)) * S ((dst_positive_code_exists_resulttable) + (dst_positive_scale_exists_resulttable)) + ((dst_positive_scale_exists_resulttable) + (dst_positive_scale_exists_resulttable))) + (((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) * S ((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) + ((dst_negative_scale_exists_resulttable) + (dst_negative_scale_exists_resulttable)))) + ((((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) * S ((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) + ((dst_negative_scale_exists_resulttable) + (dst_negative_scale_exists_resulttable))) + (((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) * S ((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) + ((dst_negative_scale_exists_resulttable) + (dst_negative_scale_exists_resulttable)))))) /\ (forall dst_index_exists_resulttable. (exists pvs_le_gap_exists_resulttabledomain. pvs_le_gap_exists_resulttabledomain + (dst_index_exists_resulttable) = (N)) -> exists dst_positive_exists_resulttable dst_negative_exists_resulttable dst_value_exists_resulttable. ((((exists ff_h_pvs_exists_resulttableentrypositive. ff_h_pvs_exists_resulttableentrypositive + S (dst_positive_exists_resulttable) = S ((S (dst_index_exists_resulttable)) * dst_positive_scale_exists_resulttable)) /\ exists ff_q_pvs_exists_resulttableentrypositive. dst_positive_code_exists_resulttable = ff_q_pvs_exists_resulttableentrypositive * S ((S (dst_index_exists_resulttable)) * dst_positive_scale_exists_resulttable) + (dst_positive_exists_resulttable))) /\ (((((exists ff_h_pvs_exists_resulttableentrynegative. ff_h_pvs_exists_resulttableentrynegative + S (dst_negative_exists_resulttable) = S ((S (dst_index_exists_resulttable)) * dst_negative_scale_exists_resulttable)) /\ exists ff_q_pvs_exists_resulttableentrynegative. dst_negative_code_exists_resulttable = ff_q_pvs_exists_resulttableentrynegative * S ((S (dst_index_exists_resulttable)) * dst_negative_scale_exists_resulttable) + (dst_negative_exists_resulttable))) /\ (exists ge_balance_positive_exists_resulttableentryvalue ge_balance_negative_exists_resulttableentryvalue. (((((dst_value_exists_resulttable) = 2 * (ge_balance_positive_exists_resulttableentryvalue) /\ (ge_balance_negative_exists_resulttableentryvalue) = 0) \/ exists ge_signed_half_exists_resulttableentryvaluedecode. (((dst_value_exists_resulttable) = 2 * ge_signed_half_exists_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_exists_resulttableentryvalue) = 0) /\ (ge_balance_negative_exists_resulttableentryvalue) = S ge_signed_half_exists_resulttableentryvaluedecode))) /\ ((dst_positive_exists_resulttable) + ge_balance_negative_exists_resulttableentryvalue = (dst_negative_exists_resulttable) + ge_balance_positive_exists_resulttableentryvalue))))))))) /\ (((exists dst_positive_code_exists_resultzero dst_positive_scale_exists_resultzero dst_negative_code_exists_resultzero dst_negative_scale_exists_resultzero dst_positive_exists_resultzero dst_negative_exists_resultzero. (((M) = (((((dst_positive_code_exists_resultzero) + (dst_positive_scale_exists_resultzero)) * S ((dst_positive_code_exists_resultzero) + (dst_positive_scale_exists_resultzero)) + ((dst_positive_scale_exists_resultzero) + (dst_positive_scale_exists_resultzero))) + (((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) * S ((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) + ((dst_negative_scale_exists_resultzero) + (dst_negative_scale_exists_resultzero)))) * S ((((dst_positive_code_exists_resultzero) + (dst_positive_scale_exists_resultzero)) * S ((dst_positive_code_exists_resultzero) + (dst_positive_scale_exists_resultzero)) + ((dst_positive_scale_exists_resultzero) + (dst_positive_scale_exists_resultzero))) + (((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) * S ((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) + ((dst_negative_scale_exists_resultzero) + (dst_negative_scale_exists_resultzero)))) + ((((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) * S ((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) + ((dst_negative_scale_exists_resultzero) + (dst_negative_scale_exists_resultzero))) + (((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) * S ((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) + ((dst_negative_scale_exists_resultzero) + (dst_negative_scale_exists_resultzero)))))) /\ (((((exists ff_h_pvs_exists_resultzeropositive. ff_h_pvs_exists_resultzeropositive + S (dst_positive_exists_resultzero) = S ((S (0)) * dst_positive_scale_exists_resultzero)) /\ exists ff_q_pvs_exists_resultzeropositive. dst_positive_code_exists_resultzero = ff_q_pvs_exists_resultzeropositive * S ((S (0)) * dst_positive_scale_exists_resultzero) + (dst_positive_exists_resultzero))) /\ (((((exists ff_h_pvs_exists_resultzeronegative. ff_h_pvs_exists_resultzeronegative + S (dst_negative_exists_resultzero) = S ((S (0)) * dst_negative_scale_exists_resultzero)) /\ exists ff_q_pvs_exists_resultzeronegative. dst_negative_code_exists_resultzero = ff_q_pvs_exists_resultzeronegative * S ((S (0)) * dst_negative_scale_exists_resultzero) + (dst_negative_exists_resultzero))) /\ (exists ge_balance_positive_exists_resultzerovalue ge_balance_negative_exists_resultzerovalue. (((((0) = 2 * (ge_balance_positive_exists_resultzerovalue) /\ (ge_balance_negative_exists_resultzerovalue) = 0) \/ exists ge_signed_half_exists_resultzerovaluedecode. (((0) = 2 * ge_signed_half_exists_resultzerovaluedecode + 1 /\ (ge_balance_positive_exists_resultzerovalue) = 0) /\ (ge_balance_negative_exists_resultzerovalue) = S ge_signed_half_exists_resultzerovaluedecode))) /\ ((dst_positive_exists_resultzero) + ge_balance_negative_exists_resultzerovalue = (dst_negative_exists_resultzero) + ge_balance_positive_exists_resultzerovalue))))))))) /\ (forall mt_index_exists_result mt_value_exists_result. ~(mt_index_exists_result=0) -> (exists pvs_le_gap_exists_resultdomain. pvs_le_gap_exists_resultdomain + (mt_index_exists_result) = (N)) -> (exists dst_positive_code_exists_resultentry dst_positive_scale_exists_resultentry dst_negative_code_exists_resultentry dst_negative_scale_exists_resultentry dst_positive_exists_resultentry dst_negative_exists_resultentry. (((M) = (((((dst_positive_code_exists_resultentry) + (dst_positive_scale_exists_resultentry)) * S ((dst_positive_code_exists_resultentry) + (dst_positive_scale_exists_resultentry)) + ((dst_positive_scale_exists_resultentry) + (dst_positive_scale_exists_resultentry))) + (((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) * S ((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) + ((dst_negative_scale_exists_resultentry) + (dst_negative_scale_exists_resultentry)))) * S ((((dst_positive_code_exists_resultentry) + (dst_positive_scale_exists_resultentry)) * S ((dst_positive_code_exists_resultentry) + (dst_positive_scale_exists_resultentry)) + ((dst_positive_scale_exists_resultentry) + (dst_positive_scale_exists_resultentry))) + (((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) * S ((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) + ((dst_negative_scale_exists_resultentry) + (dst_negative_scale_exists_resultentry)))) + ((((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) * S ((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) + ((dst_negative_scale_exists_resultentry) + (dst_negative_scale_exists_resultentry))) + (((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) * S ((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) + ((dst_negative_scale_exists_resultentry) + (dst_negative_scale_exists_resultentry)))))) /\ (((((exists ff_h_pvs_exists_resultentrypositive. ff_h_pvs_exists_resultentrypositive + S (dst_positive_exists_resultentry) = S ((S (mt_index_exists_result)) * dst_positive_scale_exists_resultentry)) /\ exists ff_q_pvs_exists_resultentrypositive. dst_positive_code_exists_resultentry = ff_q_pvs_exists_resultentrypositive * S ((S (mt_index_exists_result)) * dst_positive_scale_exists_resultentry) + (dst_positive_exists_resultentry))) /\ (((((exists ff_h_pvs_exists_resultentrynegative. ff_h_pvs_exists_resultentrynegative + S (dst_negative_exists_resultentry) = S ((S (mt_index_exists_result)) * dst_negative_scale_exists_resultentry)) /\ exists ff_q_pvs_exists_resultentrynegative. dst_negative_code_exists_resultentry = ff_q_pvs_exists_resultentrynegative * S ((S (mt_index_exists_result)) * dst_negative_scale_exists_resultentry) + (dst_negative_exists_resultentry))) /\ (exists ge_balance_positive_exists_resultentryvalue ge_balance_negative_exists_resultentryvalue. (((((mt_value_exists_result) = 2 * (ge_balance_positive_exists_resultentryvalue) /\ (ge_balance_negative_exists_resultentryvalue) = 0) \/ exists ge_signed_half_exists_resultentryvaluedecode. (((mt_value_exists_result) = 2 * ge_signed_half_exists_resultentryvaluedecode + 1 /\ (ge_balance_positive_exists_resultentryvalue) = 0) /\ (ge_balance_negative_exists_resultentryvalue) = S ge_signed_half_exists_resultentryvaluedecode))) /\ ((dst_positive_exists_resultentry) + ge_balance_negative_exists_resultentryvalue = (dst_negative_exists_resultentry) + ge_balance_positive_exists_resultentryvalue))))))))) -> (((~((mt_index_exists_result) = 0)) /\ ((((exists mv_square_prime_exists_resultvaluesquare. ((~((mv_square_prime_exists_resultvaluesquare) = 1) /\ forall pvs_left_exists_resultvaluesquareprime pvs_right_exists_resultvaluesquareprime. (mv_square_prime_exists_resultvaluesquare) = pvs_left_exists_resultvaluesquareprime * pvs_right_exists_resultvaluesquareprime -> pvs_left_exists_resultvaluesquareprime = 1 \/ pvs_right_exists_resultvaluesquareprime = 1) /\ (exists pvs_factor_exists_resultvaluesquaredivisor. (mt_index_exists_result) = (mv_square_prime_exists_resultvaluesquare * mv_square_prime_exists_resultvaluesquare) * pvs_factor_exists_resultvaluesquaredivisor))) /\ ((mt_value_exists_result) = 0))) \/ (((((~((mt_index_exists_result) = 0)) /\ (forall sfd_prime_exists_resultvaluesquarefree. (~((sfd_prime_exists_resultvaluesquarefree) = 1) /\ forall pvs_left_exists_resultvaluesquarefreedomain pvs_right_exists_resultvaluesquarefreedomain. (sfd_prime_exists_resultvaluesquarefree) = pvs_left_exists_resultvaluesquarefreedomain * pvs_right_exists_resultvaluesquarefreedomain -> pvs_left_exists_resultvaluesquarefreedomain = 1 \/ pvs_right_exists_resultvaluesquarefreedomain = 1) -> (exists pvs_le_gap_exists_resultvaluesquarefreebound. pvs_le_gap_exists_resultvaluesquarefreebound + (sfd_prime_exists_resultvaluesquarefree) = (mt_index_exists_result)) -> ~(exists pvs_factor_exists_resultvaluesquarefreesquare. (mt_index_exists_result) = (sfd_prime_exists_resultvaluesquarefree * sfd_prime_exists_resultvaluesquarefree) * pvs_factor_exists_resultvaluesquarefreesquare)))) /\ (exists mv_factor_code_exists_resultvaluefactors mv_factor_scale_exists_resultvaluefactors mv_factor_count_exists_resultvaluefactors. (((~(mt_index_exists_result = 0) /\ ((exists ff_u_fsat_exists_resultvaluefactorsfactorization_product ff_v_fsat_exists_resultvaluefactorsfactorization_product. ((((exists ff_h_fsat_exists_resultvaluefactorsfactorization_product_start. ff_h_fsat_exists_resultvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_resultvaluefactorsfactorization_product_start. ff_u_fsat_exists_resultvaluefactorsfactorization_product = ff_q_fsat_exists_resultvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_exists_resultvaluefactorsfactorization_product_terminal. ff_h_fsat_exists_resultvaluefactorsfactorization_product_terminal + S (mt_index_exists_result) = S ((S (mv_factor_count_exists_resultvaluefactors)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_resultvaluefactorsfactorization_product_terminal. ff_u_fsat_exists_resultvaluefactorsfactorization_product = ff_q_fsat_exists_resultvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_exists_resultvaluefactors)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product) + (mt_index_exists_result))) /\ forall ff_i_fsat_exists_resultvaluefactorsfactorization_product. (exists ff_lt_fsat_exists_resultvaluefactorsfactorization_product_bound. ff_lt_fsat_exists_resultvaluefactorsfactorization_product_bound + S ff_i_fsat_exists_resultvaluefactorsfactorization_product = mv_factor_count_exists_resultvaluefactors) -> exists ff_p_fsat_exists_resultvaluefactorsfactorization_product ff_r_fsat_exists_resultvaluefactorsfactorization_product ff_s_fsat_exists_resultvaluefactorsfactorization_product. ((((exists ff_h_fsat_exists_resultvaluefactorsfactorization_product_factor. ff_h_fsat_exists_resultvaluefactorsfactorization_product_factor + S (ff_p_fsat_exists_resultvaluefactorsfactorization_product) = S ((S (ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * mv_factor_scale_exists_resultvaluefactors)) /\ exists ff_q_fsat_exists_resultvaluefactorsfactorization_product_factor. mv_factor_code_exists_resultvaluefactors = ff_q_fsat_exists_resultvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * mv_factor_scale_exists_resultvaluefactors) + (ff_p_fsat_exists_resultvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_resultvaluefactorsfactorization_product_partial. ff_h_fsat_exists_resultvaluefactorsfactorization_product_partial + S (ff_r_fsat_exists_resultvaluefactorsfactorization_product) = S ((S (ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_resultvaluefactorsfactorization_product_partial. ff_u_fsat_exists_resultvaluefactorsfactorization_product = ff_q_fsat_exists_resultvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product) + (ff_r_fsat_exists_resultvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_resultvaluefactorsfactorization_product_successor. ff_h_fsat_exists_resultvaluefactorsfactorization_product_successor + S (ff_s_fsat_exists_resultvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_resultvaluefactorsfactorization_product_successor. ff_u_fsat_exists_resultvaluefactorsfactorization_product = ff_q_fsat_exists_resultvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product) + (ff_s_fsat_exists_resultvaluefactorsfactorization_product))) /\ ff_s_fsat_exists_resultvaluefactorsfactorization_product = ff_r_fsat_exists_resultvaluefactorsfactorization_product * ff_p_fsat_exists_resultvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_exists_resultvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_exists_resultvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_exists_resultvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_exists_resultvaluefactorsfactorization_primes = (mv_factor_count_exists_resultvaluefactors)) -> exists ftsf_factor_fsat_exists_resultvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_exists_resultvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_exists_resultvaluefactorsfactorization_primes)) * mv_factor_scale_exists_resultvaluefactors)) /\ exists ff_q_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_entry. mv_factor_code_exists_resultvaluefactors = ff_q_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_exists_resultvaluefactorsfactorization_primes)) * mv_factor_scale_exists_resultvaluefactors) + (ftsf_factor_fsat_exists_resultvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_exists_resultvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_exists_resultvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_exists_resultvaluefactorsparityeven. (mv_factor_count_exists_resultvaluefactors) = 2 * mv_even_half_exists_resultvaluefactorsparityeven) /\ ((mt_value_exists_result) = 2))) \/ (((exists mv_odd_half_exists_resultvaluefactorsparityodd. (mv_factor_count_exists_resultvaluefactors) = 2 * mv_odd_half_exists_resultvaluefactorsparityodd + 1) /\ ((mt_value_exists_result) = 1))))))))))))))))

Complete tactic proof in conservative notation

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

31 script commands · 13 reading checkpoints · 3 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 (3)
arithmetic signed table singletonmobius table zero constructormobius table append
01Fix variables and assumptionsL1–1

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

  1. L1
    intro N
02Induction on NL2–2

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction N
03Establish hbaseL3–5

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

  1. L3
    have hbase : ∃ F. ArithTable(0,F) ∧ ArithAt(F,0,0)Definitions: ArithTable(0,F)ArithAt(F,0,0)Original native command in the exact edition
  2. L4
    specialize arithmetic_signed_table_singleton (0)
  3. L5
    apply arithmetic_signed_table_singleton
04Separate the logical casesL6–7

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

  1. L6
    cases hbase
  2. L7
    cases hbase_witness
05Construct an explicit witnessL8–8

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

  1. L8
    exists x
06Use earlier factsL9–12

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

  1. L9
    specialize mobius_table_zero_constructor (x)
  2. L10
    apply mobius_table_zero_constructor
  3. L11
    exact hbase_witness_left
  4. L12
    exact hbase_witness_right
07Separate the logical casesL13–13

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

  1. L13
    cases IH
08Establish hzL14–19

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

  1. L14
    have hz : ∃ z. Mobius(S N,z)Definitions: Mobius(S N,z)Original native command in the exact edition
  2. L15
    specialize mobius_value_exists (S N)
  3. L16
    apply mobius_value_exists
  4. L17
    intro hzero
  5. L18
    apply PA1
  6. L19
    exact hzero
09Separate the logical casesL20–20

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

  1. L20
    cases hz
10Establish hnextL21–27

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

  1. L21
    have hnext : ∃ G. MobiusTable(S N,G) ∧ ArithTableEqual(x,G,S N)Definitions: MobiusTable(S N,G)ArithTableEqual(x,G,S N)Original native command in the exact edition
  2. L22
    specialize mobius_table_append (N)
  3. L23
    specialize mobius_table_append (x)
  4. L24
    specialize mobius_table_append (x1)
  5. L25
    apply mobius_table_append
  6. L26
    exact IH_witness
  7. L27
    exact hz_witness
11Separate the logical casesL28–29

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

  1. L28
    cases hnext
  2. L29
    cases hnext_witness
12Construct an explicit witnessL30–30

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

  1. L30
    exists x2
13Use earlier factsL31–31

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

  1. L31
    exact hnext_witness_left

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro N
  2. 0002induction N
  3. 0003have hbase : ∃ F. ArithTable(0,F) ∧ ArithAt(F,0,0)
  4. 0004specialize arithmetic_signed_table_singleton (0)
  5. 0005apply arithmetic_signed_table_singleton
  6. 0006cases hbase
  7. 0007cases hbase_witness
  8. 0008exists x
  9. 0009specialize mobius_table_zero_constructor (x)
  10. 0010apply mobius_table_zero_constructor
  11. 0011exact hbase_witness_left
  12. 0012exact hbase_witness_right
  13. 0013cases IH
  14. 0014have hz : ∃ z. Mobius(S N,z)
  15. 0015specialize mobius_value_exists (S N)
  16. 0016apply mobius_value_exists
  17. 0017intro hzero
  18. 0018apply PA1
  19. 0019exact hzero
  20. 0020cases hz
  21. 0021have hnext : ∃ G. MobiusTable(S N,G) ∧ ArithTableEqual(x,G,S N)
  22. 0022specialize mobius_table_append (N)
  23. 0023specialize mobius_table_append (x)
  24. 0024specialize mobius_table_append (x1)
  25. 0025apply mobius_table_append
  26. 0026exact IH_witness
  27. 0027exact hz_witness
  28. 0028cases hnext
  29. 0029cases hnext_witness
  30. 0030exists x2
  31. 0031exact hnext_witness_left