DU0009

dirichlet_constant_one_table_reencoding

Equal represented positive values preserve this table graph without equating table codes, component representatives or their arbitrary zero entries.

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.

Signed one is code 2. Positive-only table graphs preserve arbitrary zeroth values, including N=0. The unit and divisor-sum identities are proved, never embedded in definitions. The separate inverse family proves the general unit-at-one criterion; multiplicative-function closure remains open.

Exact theorem in conservative defined notation

∀ N. ∀ F. ∀ G. ConstantOneTable(N,F) → ArithTable(N,G) → ArithPositiveEqual(F,G,N) → ConstantOneTable(N,G)

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

Definition DAG

ArithTable(N,F) · 1ArithAt(F,i,z) · 1ArithPositiveEqual(F,G,N) · 1ConstantOneTable(N,U) · 2

Actual proof prerequisites

divisor_signed_table_lookup · checked external prerequisite
Original expanded first-order statement 
forall N F G. (((exists dst_positive_code_constant_onetransport_sourcetable dst_positive_scale_constant_onetransport_sourcetable dst_negative_code_constant_onetransport_sourcetable dst_negative_scale_constant_onetransport_sourcetable. (((F) = (((((dst_positive_code_constant_onetransport_sourcetable) + (dst_positive_scale_constant_onetransport_sourcetable)) * S ((dst_positive_code_constant_onetransport_sourcetable) + (dst_positive_scale_constant_onetransport_sourcetable)) + ((dst_positive_scale_constant_onetransport_sourcetable) + (dst_positive_scale_constant_onetransport_sourcetable))) + (((dst_negative_code_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)) * S ((dst_negative_code_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)) + ((dst_negative_scale_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)))) * S ((((dst_positive_code_constant_onetransport_sourcetable) + (dst_positive_scale_constant_onetransport_sourcetable)) * S ((dst_positive_code_constant_onetransport_sourcetable) + (dst_positive_scale_constant_onetransport_sourcetable)) + ((dst_positive_scale_constant_onetransport_sourcetable) + (dst_positive_scale_constant_onetransport_sourcetable))) + (((dst_negative_code_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)) * S ((dst_negative_code_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)) + ((dst_negative_scale_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)))) + ((((dst_negative_code_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)) * S ((dst_negative_code_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)) + ((dst_negative_scale_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable))) + (((dst_negative_code_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)) * S ((dst_negative_code_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)) + ((dst_negative_scale_constant_onetransport_sourcetable) + (dst_negative_scale_constant_onetransport_sourcetable)))))) /\ (forall dst_index_constant_onetransport_sourcetable. (exists pvs_le_gap_constant_onetransport_sourcetabledomain. pvs_le_gap_constant_onetransport_sourcetabledomain + (dst_index_constant_onetransport_sourcetable) = (N)) -> exists dst_positive_constant_onetransport_sourcetable dst_negative_constant_onetransport_sourcetable dst_value_constant_onetransport_sourcetable. ((((exists ff_h_pvs_constant_onetransport_sourcetableentrypositive. ff_h_pvs_constant_onetransport_sourcetableentrypositive + S (dst_positive_constant_onetransport_sourcetable) = S ((S (dst_index_constant_onetransport_sourcetable)) * dst_positive_scale_constant_onetransport_sourcetable)) /\ exists ff_q_pvs_constant_onetransport_sourcetableentrypositive. dst_positive_code_constant_onetransport_sourcetable = ff_q_pvs_constant_onetransport_sourcetableentrypositive * S ((S (dst_index_constant_onetransport_sourcetable)) * dst_positive_scale_constant_onetransport_sourcetable) + (dst_positive_constant_onetransport_sourcetable))) /\ (((((exists ff_h_pvs_constant_onetransport_sourcetableentrynegative. ff_h_pvs_constant_onetransport_sourcetableentrynegative + S (dst_negative_constant_onetransport_sourcetable) = S ((S (dst_index_constant_onetransport_sourcetable)) * dst_negative_scale_constant_onetransport_sourcetable)) /\ exists ff_q_pvs_constant_onetransport_sourcetableentrynegative. dst_negative_code_constant_onetransport_sourcetable = ff_q_pvs_constant_onetransport_sourcetableentrynegative * S ((S (dst_index_constant_onetransport_sourcetable)) * dst_negative_scale_constant_onetransport_sourcetable) + (dst_negative_constant_onetransport_sourcetable))) /\ (exists ge_balance_positive_constant_onetransport_sourcetableentryvalue ge_balance_negative_constant_onetransport_sourcetableentryvalue. (((((dst_value_constant_onetransport_sourcetable) = 2 * (ge_balance_positive_constant_onetransport_sourcetableentryvalue) /\ (ge_balance_negative_constant_onetransport_sourcetableentryvalue) = 0) \/ exists ge_signed_half_constant_onetransport_sourcetableentryvaluedecode. (((dst_value_constant_onetransport_sourcetable) = 2 * ge_signed_half_constant_onetransport_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_constant_onetransport_sourcetableentryvalue) = 0) /\ (ge_balance_negative_constant_onetransport_sourcetableentryvalue) = S ge_signed_half_constant_onetransport_sourcetableentryvaluedecode))) /\ ((dst_positive_constant_onetransport_sourcetable) + ge_balance_negative_constant_onetransport_sourcetableentryvalue = (dst_negative_constant_onetransport_sourcetable) + ge_balance_positive_constant_onetransport_sourcetableentryvalue))))))))) /\ (forall du_index_constant_onetransport_source du_value_constant_onetransport_source. ~(du_index_constant_onetransport_source=0) -> (exists pvs_le_gap_constant_onetransport_sourcebound. pvs_le_gap_constant_onetransport_sourcebound + (du_index_constant_onetransport_source) = (N)) -> (exists dst_positive_code_constant_onetransport_sourceentry dst_positive_scale_constant_onetransport_sourceentry dst_negative_code_constant_onetransport_sourceentry dst_negative_scale_constant_onetransport_sourceentry dst_positive_constant_onetransport_sourceentry dst_negative_constant_onetransport_sourceentry. (((F) = (((((dst_positive_code_constant_onetransport_sourceentry) + (dst_positive_scale_constant_onetransport_sourceentry)) * S ((dst_positive_code_constant_onetransport_sourceentry) + (dst_positive_scale_constant_onetransport_sourceentry)) + ((dst_positive_scale_constant_onetransport_sourceentry) + (dst_positive_scale_constant_onetransport_sourceentry))) + (((dst_negative_code_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)) * S ((dst_negative_code_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)) + ((dst_negative_scale_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)))) * S ((((dst_positive_code_constant_onetransport_sourceentry) + (dst_positive_scale_constant_onetransport_sourceentry)) * S ((dst_positive_code_constant_onetransport_sourceentry) + (dst_positive_scale_constant_onetransport_sourceentry)) + ((dst_positive_scale_constant_onetransport_sourceentry) + (dst_positive_scale_constant_onetransport_sourceentry))) + (((dst_negative_code_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)) * S ((dst_negative_code_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)) + ((dst_negative_scale_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)))) + ((((dst_negative_code_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)) * S ((dst_negative_code_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)) + ((dst_negative_scale_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry))) + (((dst_negative_code_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)) * S ((dst_negative_code_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)) + ((dst_negative_scale_constant_onetransport_sourceentry) + (dst_negative_scale_constant_onetransport_sourceentry)))))) /\ (((((exists ff_h_pvs_constant_onetransport_sourceentrypositive. ff_h_pvs_constant_onetransport_sourceentrypositive + S (dst_positive_constant_onetransport_sourceentry) = S ((S (du_index_constant_onetransport_source)) * dst_positive_scale_constant_onetransport_sourceentry)) /\ exists ff_q_pvs_constant_onetransport_sourceentrypositive. dst_positive_code_constant_onetransport_sourceentry = ff_q_pvs_constant_onetransport_sourceentrypositive * S ((S (du_index_constant_onetransport_source)) * dst_positive_scale_constant_onetransport_sourceentry) + (dst_positive_constant_onetransport_sourceentry))) /\ (((((exists ff_h_pvs_constant_onetransport_sourceentrynegative. ff_h_pvs_constant_onetransport_sourceentrynegative + S (dst_negative_constant_onetransport_sourceentry) = S ((S (du_index_constant_onetransport_source)) * dst_negative_scale_constant_onetransport_sourceentry)) /\ exists ff_q_pvs_constant_onetransport_sourceentrynegative. dst_negative_code_constant_onetransport_sourceentry = ff_q_pvs_constant_onetransport_sourceentrynegative * S ((S (du_index_constant_onetransport_source)) * dst_negative_scale_constant_onetransport_sourceentry) + (dst_negative_constant_onetransport_sourceentry))) /\ (exists ge_balance_positive_constant_onetransport_sourceentryvalue ge_balance_negative_constant_onetransport_sourceentryvalue. (((((du_value_constant_onetransport_source) = 2 * (ge_balance_positive_constant_onetransport_sourceentryvalue) /\ (ge_balance_negative_constant_onetransport_sourceentryvalue) = 0) \/ exists ge_signed_half_constant_onetransport_sourceentryvaluedecode. (((du_value_constant_onetransport_source) = 2 * ge_signed_half_constant_onetransport_sourceentryvaluedecode + 1 /\ (ge_balance_positive_constant_onetransport_sourceentryvalue) = 0) /\ (ge_balance_negative_constant_onetransport_sourceentryvalue) = S ge_signed_half_constant_onetransport_sourceentryvaluedecode))) /\ ((dst_positive_constant_onetransport_sourceentry) + ge_balance_negative_constant_onetransport_sourceentryvalue = (dst_negative_constant_onetransport_sourceentry) + ge_balance_positive_constant_onetransport_sourceentryvalue))))))))) -> du_value_constant_onetransport_source=2))) -> (exists dst_positive_code_constant_onetransport_valid dst_positive_scale_constant_onetransport_valid dst_negative_code_constant_onetransport_valid dst_negative_scale_constant_onetransport_valid. (((G) = (((((dst_positive_code_constant_onetransport_valid) + (dst_positive_scale_constant_onetransport_valid)) * S ((dst_positive_code_constant_onetransport_valid) + (dst_positive_scale_constant_onetransport_valid)) + ((dst_positive_scale_constant_onetransport_valid) + (dst_positive_scale_constant_onetransport_valid))) + (((dst_negative_code_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)) * S ((dst_negative_code_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)) + ((dst_negative_scale_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)))) * S ((((dst_positive_code_constant_onetransport_valid) + (dst_positive_scale_constant_onetransport_valid)) * S ((dst_positive_code_constant_onetransport_valid) + (dst_positive_scale_constant_onetransport_valid)) + ((dst_positive_scale_constant_onetransport_valid) + (dst_positive_scale_constant_onetransport_valid))) + (((dst_negative_code_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)) * S ((dst_negative_code_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)) + ((dst_negative_scale_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)))) + ((((dst_negative_code_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)) * S ((dst_negative_code_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)) + ((dst_negative_scale_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid))) + (((dst_negative_code_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)) * S ((dst_negative_code_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)) + ((dst_negative_scale_constant_onetransport_valid) + (dst_negative_scale_constant_onetransport_valid)))))) /\ (forall dst_index_constant_onetransport_valid. (exists pvs_le_gap_constant_onetransport_validdomain. pvs_le_gap_constant_onetransport_validdomain + (dst_index_constant_onetransport_valid) = (N)) -> exists dst_positive_constant_onetransport_valid dst_negative_constant_onetransport_valid dst_value_constant_onetransport_valid. ((((exists ff_h_pvs_constant_onetransport_validentrypositive. ff_h_pvs_constant_onetransport_validentrypositive + S (dst_positive_constant_onetransport_valid) = S ((S (dst_index_constant_onetransport_valid)) * dst_positive_scale_constant_onetransport_valid)) /\ exists ff_q_pvs_constant_onetransport_validentrypositive. dst_positive_code_constant_onetransport_valid = ff_q_pvs_constant_onetransport_validentrypositive * S ((S (dst_index_constant_onetransport_valid)) * dst_positive_scale_constant_onetransport_valid) + (dst_positive_constant_onetransport_valid))) /\ (((((exists ff_h_pvs_constant_onetransport_validentrynegative. ff_h_pvs_constant_onetransport_validentrynegative + S (dst_negative_constant_onetransport_valid) = S ((S (dst_index_constant_onetransport_valid)) * dst_negative_scale_constant_onetransport_valid)) /\ exists ff_q_pvs_constant_onetransport_validentrynegative. dst_negative_code_constant_onetransport_valid = ff_q_pvs_constant_onetransport_validentrynegative * S ((S (dst_index_constant_onetransport_valid)) * dst_negative_scale_constant_onetransport_valid) + (dst_negative_constant_onetransport_valid))) /\ (exists ge_balance_positive_constant_onetransport_validentryvalue ge_balance_negative_constant_onetransport_validentryvalue. (((((dst_value_constant_onetransport_valid) = 2 * (ge_balance_positive_constant_onetransport_validentryvalue) /\ (ge_balance_negative_constant_onetransport_validentryvalue) = 0) \/ exists ge_signed_half_constant_onetransport_validentryvaluedecode. (((dst_value_constant_onetransport_valid) = 2 * ge_signed_half_constant_onetransport_validentryvaluedecode + 1 /\ (ge_balance_positive_constant_onetransport_validentryvalue) = 0) /\ (ge_balance_negative_constant_onetransport_validentryvalue) = S ge_signed_half_constant_onetransport_validentryvaluedecode))) /\ ((dst_positive_constant_onetransport_valid) + ge_balance_negative_constant_onetransport_validentryvalue = (dst_negative_constant_onetransport_valid) + ge_balance_positive_constant_onetransport_validentryvalue))))))))) -> (forall dm_index_constant_onetransport_equal dm_first_value_constant_onetransport_equal dm_second_value_constant_onetransport_equal. ~(dm_index_constant_onetransport_equal=0) -> (exists pvs_le_gap_constant_onetransport_equaldomain. pvs_le_gap_constant_onetransport_equaldomain + (dm_index_constant_onetransport_equal) = (N)) -> (exists dst_positive_code_constant_onetransport_equalfirst dst_positive_scale_constant_onetransport_equalfirst dst_negative_code_constant_onetransport_equalfirst dst_negative_scale_constant_onetransport_equalfirst dst_positive_constant_onetransport_equalfirst dst_negative_constant_onetransport_equalfirst. (((F) = (((((dst_positive_code_constant_onetransport_equalfirst) + (dst_positive_scale_constant_onetransport_equalfirst)) * S ((dst_positive_code_constant_onetransport_equalfirst) + (dst_positive_scale_constant_onetransport_equalfirst)) + ((dst_positive_scale_constant_onetransport_equalfirst) + (dst_positive_scale_constant_onetransport_equalfirst))) + (((dst_negative_code_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)) * S ((dst_negative_code_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)) + ((dst_negative_scale_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)))) * S ((((dst_positive_code_constant_onetransport_equalfirst) + (dst_positive_scale_constant_onetransport_equalfirst)) * S ((dst_positive_code_constant_onetransport_equalfirst) + (dst_positive_scale_constant_onetransport_equalfirst)) + ((dst_positive_scale_constant_onetransport_equalfirst) + (dst_positive_scale_constant_onetransport_equalfirst))) + (((dst_negative_code_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)) * S ((dst_negative_code_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)) + ((dst_negative_scale_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)))) + ((((dst_negative_code_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)) * S ((dst_negative_code_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)) + ((dst_negative_scale_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst))) + (((dst_negative_code_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)) * S ((dst_negative_code_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)) + ((dst_negative_scale_constant_onetransport_equalfirst) + (dst_negative_scale_constant_onetransport_equalfirst)))))) /\ (((((exists ff_h_pvs_constant_onetransport_equalfirstpositive. ff_h_pvs_constant_onetransport_equalfirstpositive + S (dst_positive_constant_onetransport_equalfirst) = S ((S (dm_index_constant_onetransport_equal)) * dst_positive_scale_constant_onetransport_equalfirst)) /\ exists ff_q_pvs_constant_onetransport_equalfirstpositive. dst_positive_code_constant_onetransport_equalfirst = ff_q_pvs_constant_onetransport_equalfirstpositive * S ((S (dm_index_constant_onetransport_equal)) * dst_positive_scale_constant_onetransport_equalfirst) + (dst_positive_constant_onetransport_equalfirst))) /\ (((((exists ff_h_pvs_constant_onetransport_equalfirstnegative. ff_h_pvs_constant_onetransport_equalfirstnegative + S (dst_negative_constant_onetransport_equalfirst) = S ((S (dm_index_constant_onetransport_equal)) * dst_negative_scale_constant_onetransport_equalfirst)) /\ exists ff_q_pvs_constant_onetransport_equalfirstnegative. dst_negative_code_constant_onetransport_equalfirst = ff_q_pvs_constant_onetransport_equalfirstnegative * S ((S (dm_index_constant_onetransport_equal)) * dst_negative_scale_constant_onetransport_equalfirst) + (dst_negative_constant_onetransport_equalfirst))) /\ (exists ge_balance_positive_constant_onetransport_equalfirstvalue ge_balance_negative_constant_onetransport_equalfirstvalue. (((((dm_first_value_constant_onetransport_equal) = 2 * (ge_balance_positive_constant_onetransport_equalfirstvalue) /\ (ge_balance_negative_constant_onetransport_equalfirstvalue) = 0) \/ exists ge_signed_half_constant_onetransport_equalfirstvaluedecode. (((dm_first_value_constant_onetransport_equal) = 2 * ge_signed_half_constant_onetransport_equalfirstvaluedecode + 1 /\ (ge_balance_positive_constant_onetransport_equalfirstvalue) = 0) /\ (ge_balance_negative_constant_onetransport_equalfirstvalue) = S ge_signed_half_constant_onetransport_equalfirstvaluedecode))) /\ ((dst_positive_constant_onetransport_equalfirst) + ge_balance_negative_constant_onetransport_equalfirstvalue = (dst_negative_constant_onetransport_equalfirst) + ge_balance_positive_constant_onetransport_equalfirstvalue))))))))) -> (exists dst_positive_code_constant_onetransport_equalsecond dst_positive_scale_constant_onetransport_equalsecond dst_negative_code_constant_onetransport_equalsecond dst_negative_scale_constant_onetransport_equalsecond dst_positive_constant_onetransport_equalsecond dst_negative_constant_onetransport_equalsecond. (((G) = (((((dst_positive_code_constant_onetransport_equalsecond) + (dst_positive_scale_constant_onetransport_equalsecond)) * S ((dst_positive_code_constant_onetransport_equalsecond) + (dst_positive_scale_constant_onetransport_equalsecond)) + ((dst_positive_scale_constant_onetransport_equalsecond) + (dst_positive_scale_constant_onetransport_equalsecond))) + (((dst_negative_code_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)) * S ((dst_negative_code_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)) + ((dst_negative_scale_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)))) * S ((((dst_positive_code_constant_onetransport_equalsecond) + (dst_positive_scale_constant_onetransport_equalsecond)) * S ((dst_positive_code_constant_onetransport_equalsecond) + (dst_positive_scale_constant_onetransport_equalsecond)) + ((dst_positive_scale_constant_onetransport_equalsecond) + (dst_positive_scale_constant_onetransport_equalsecond))) + (((dst_negative_code_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)) * S ((dst_negative_code_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)) + ((dst_negative_scale_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)))) + ((((dst_negative_code_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)) * S ((dst_negative_code_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)) + ((dst_negative_scale_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond))) + (((dst_negative_code_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)) * S ((dst_negative_code_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)) + ((dst_negative_scale_constant_onetransport_equalsecond) + (dst_negative_scale_constant_onetransport_equalsecond)))))) /\ (((((exists ff_h_pvs_constant_onetransport_equalsecondpositive. ff_h_pvs_constant_onetransport_equalsecondpositive + S (dst_positive_constant_onetransport_equalsecond) = S ((S (dm_index_constant_onetransport_equal)) * dst_positive_scale_constant_onetransport_equalsecond)) /\ exists ff_q_pvs_constant_onetransport_equalsecondpositive. dst_positive_code_constant_onetransport_equalsecond = ff_q_pvs_constant_onetransport_equalsecondpositive * S ((S (dm_index_constant_onetransport_equal)) * dst_positive_scale_constant_onetransport_equalsecond) + (dst_positive_constant_onetransport_equalsecond))) /\ (((((exists ff_h_pvs_constant_onetransport_equalsecondnegative. ff_h_pvs_constant_onetransport_equalsecondnegative + S (dst_negative_constant_onetransport_equalsecond) = S ((S (dm_index_constant_onetransport_equal)) * dst_negative_scale_constant_onetransport_equalsecond)) /\ exists ff_q_pvs_constant_onetransport_equalsecondnegative. dst_negative_code_constant_onetransport_equalsecond = ff_q_pvs_constant_onetransport_equalsecondnegative * S ((S (dm_index_constant_onetransport_equal)) * dst_negative_scale_constant_onetransport_equalsecond) + (dst_negative_constant_onetransport_equalsecond))) /\ (exists ge_balance_positive_constant_onetransport_equalsecondvalue ge_balance_negative_constant_onetransport_equalsecondvalue. (((((dm_second_value_constant_onetransport_equal) = 2 * (ge_balance_positive_constant_onetransport_equalsecondvalue) /\ (ge_balance_negative_constant_onetransport_equalsecondvalue) = 0) \/ exists ge_signed_half_constant_onetransport_equalsecondvaluedecode. (((dm_second_value_constant_onetransport_equal) = 2 * ge_signed_half_constant_onetransport_equalsecondvaluedecode + 1 /\ (ge_balance_positive_constant_onetransport_equalsecondvalue) = 0) /\ (ge_balance_negative_constant_onetransport_equalsecondvalue) = S ge_signed_half_constant_onetransport_equalsecondvaluedecode))) /\ ((dst_positive_constant_onetransport_equalsecond) + ge_balance_negative_constant_onetransport_equalsecondvalue = (dst_negative_constant_onetransport_equalsecond) + ge_balance_positive_constant_onetransport_equalsecondvalue))))))))) -> dm_first_value_constant_onetransport_equal=dm_second_value_constant_onetransport_equal) -> (((exists dst_positive_code_constant_onetransport_resulttable dst_positive_scale_constant_onetransport_resulttable dst_negative_code_constant_onetransport_resulttable dst_negative_scale_constant_onetransport_resulttable. (((G) = (((((dst_positive_code_constant_onetransport_resulttable) + (dst_positive_scale_constant_onetransport_resulttable)) * S ((dst_positive_code_constant_onetransport_resulttable) + (dst_positive_scale_constant_onetransport_resulttable)) + ((dst_positive_scale_constant_onetransport_resulttable) + (dst_positive_scale_constant_onetransport_resulttable))) + (((dst_negative_code_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)) * S ((dst_negative_code_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)) + ((dst_negative_scale_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)))) * S ((((dst_positive_code_constant_onetransport_resulttable) + (dst_positive_scale_constant_onetransport_resulttable)) * S ((dst_positive_code_constant_onetransport_resulttable) + (dst_positive_scale_constant_onetransport_resulttable)) + ((dst_positive_scale_constant_onetransport_resulttable) + (dst_positive_scale_constant_onetransport_resulttable))) + (((dst_negative_code_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)) * S ((dst_negative_code_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)) + ((dst_negative_scale_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)))) + ((((dst_negative_code_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)) * S ((dst_negative_code_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)) + ((dst_negative_scale_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable))) + (((dst_negative_code_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)) * S ((dst_negative_code_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)) + ((dst_negative_scale_constant_onetransport_resulttable) + (dst_negative_scale_constant_onetransport_resulttable)))))) /\ (forall dst_index_constant_onetransport_resulttable. (exists pvs_le_gap_constant_onetransport_resulttabledomain. pvs_le_gap_constant_onetransport_resulttabledomain + (dst_index_constant_onetransport_resulttable) = (N)) -> exists dst_positive_constant_onetransport_resulttable dst_negative_constant_onetransport_resulttable dst_value_constant_onetransport_resulttable. ((((exists ff_h_pvs_constant_onetransport_resulttableentrypositive. ff_h_pvs_constant_onetransport_resulttableentrypositive + S (dst_positive_constant_onetransport_resulttable) = S ((S (dst_index_constant_onetransport_resulttable)) * dst_positive_scale_constant_onetransport_resulttable)) /\ exists ff_q_pvs_constant_onetransport_resulttableentrypositive. dst_positive_code_constant_onetransport_resulttable = ff_q_pvs_constant_onetransport_resulttableentrypositive * S ((S (dst_index_constant_onetransport_resulttable)) * dst_positive_scale_constant_onetransport_resulttable) + (dst_positive_constant_onetransport_resulttable))) /\ (((((exists ff_h_pvs_constant_onetransport_resulttableentrynegative. ff_h_pvs_constant_onetransport_resulttableentrynegative + S (dst_negative_constant_onetransport_resulttable) = S ((S (dst_index_constant_onetransport_resulttable)) * dst_negative_scale_constant_onetransport_resulttable)) /\ exists ff_q_pvs_constant_onetransport_resulttableentrynegative. dst_negative_code_constant_onetransport_resulttable = ff_q_pvs_constant_onetransport_resulttableentrynegative * S ((S (dst_index_constant_onetransport_resulttable)) * dst_negative_scale_constant_onetransport_resulttable) + (dst_negative_constant_onetransport_resulttable))) /\ (exists ge_balance_positive_constant_onetransport_resulttableentryvalue ge_balance_negative_constant_onetransport_resulttableentryvalue. (((((dst_value_constant_onetransport_resulttable) = 2 * (ge_balance_positive_constant_onetransport_resulttableentryvalue) /\ (ge_balance_negative_constant_onetransport_resulttableentryvalue) = 0) \/ exists ge_signed_half_constant_onetransport_resulttableentryvaluedecode. (((dst_value_constant_onetransport_resulttable) = 2 * ge_signed_half_constant_onetransport_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_constant_onetransport_resulttableentryvalue) = 0) /\ (ge_balance_negative_constant_onetransport_resulttableentryvalue) = S ge_signed_half_constant_onetransport_resulttableentryvaluedecode))) /\ ((dst_positive_constant_onetransport_resulttable) + ge_balance_negative_constant_onetransport_resulttableentryvalue = (dst_negative_constant_onetransport_resulttable) + ge_balance_positive_constant_onetransport_resulttableentryvalue))))))))) /\ (forall du_index_constant_onetransport_result du_value_constant_onetransport_result. ~(du_index_constant_onetransport_result=0) -> (exists pvs_le_gap_constant_onetransport_resultbound. pvs_le_gap_constant_onetransport_resultbound + (du_index_constant_onetransport_result) = (N)) -> (exists dst_positive_code_constant_onetransport_resultentry dst_positive_scale_constant_onetransport_resultentry dst_negative_code_constant_onetransport_resultentry dst_negative_scale_constant_onetransport_resultentry dst_positive_constant_onetransport_resultentry dst_negative_constant_onetransport_resultentry. (((G) = (((((dst_positive_code_constant_onetransport_resultentry) + (dst_positive_scale_constant_onetransport_resultentry)) * S ((dst_positive_code_constant_onetransport_resultentry) + (dst_positive_scale_constant_onetransport_resultentry)) + ((dst_positive_scale_constant_onetransport_resultentry) + (dst_positive_scale_constant_onetransport_resultentry))) + (((dst_negative_code_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)) * S ((dst_negative_code_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)) + ((dst_negative_scale_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)))) * S ((((dst_positive_code_constant_onetransport_resultentry) + (dst_positive_scale_constant_onetransport_resultentry)) * S ((dst_positive_code_constant_onetransport_resultentry) + (dst_positive_scale_constant_onetransport_resultentry)) + ((dst_positive_scale_constant_onetransport_resultentry) + (dst_positive_scale_constant_onetransport_resultentry))) + (((dst_negative_code_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)) * S ((dst_negative_code_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)) + ((dst_negative_scale_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)))) + ((((dst_negative_code_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)) * S ((dst_negative_code_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)) + ((dst_negative_scale_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry))) + (((dst_negative_code_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)) * S ((dst_negative_code_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)) + ((dst_negative_scale_constant_onetransport_resultentry) + (dst_negative_scale_constant_onetransport_resultentry)))))) /\ (((((exists ff_h_pvs_constant_onetransport_resultentrypositive. ff_h_pvs_constant_onetransport_resultentrypositive + S (dst_positive_constant_onetransport_resultentry) = S ((S (du_index_constant_onetransport_result)) * dst_positive_scale_constant_onetransport_resultentry)) /\ exists ff_q_pvs_constant_onetransport_resultentrypositive. dst_positive_code_constant_onetransport_resultentry = ff_q_pvs_constant_onetransport_resultentrypositive * S ((S (du_index_constant_onetransport_result)) * dst_positive_scale_constant_onetransport_resultentry) + (dst_positive_constant_onetransport_resultentry))) /\ (((((exists ff_h_pvs_constant_onetransport_resultentrynegative. ff_h_pvs_constant_onetransport_resultentrynegative + S (dst_negative_constant_onetransport_resultentry) = S ((S (du_index_constant_onetransport_result)) * dst_negative_scale_constant_onetransport_resultentry)) /\ exists ff_q_pvs_constant_onetransport_resultentrynegative. dst_negative_code_constant_onetransport_resultentry = ff_q_pvs_constant_onetransport_resultentrynegative * S ((S (du_index_constant_onetransport_result)) * dst_negative_scale_constant_onetransport_resultentry) + (dst_negative_constant_onetransport_resultentry))) /\ (exists ge_balance_positive_constant_onetransport_resultentryvalue ge_balance_negative_constant_onetransport_resultentryvalue. (((((du_value_constant_onetransport_result) = 2 * (ge_balance_positive_constant_onetransport_resultentryvalue) /\ (ge_balance_negative_constant_onetransport_resultentryvalue) = 0) \/ exists ge_signed_half_constant_onetransport_resultentryvaluedecode. (((du_value_constant_onetransport_result) = 2 * ge_signed_half_constant_onetransport_resultentryvaluedecode + 1 /\ (ge_balance_positive_constant_onetransport_resultentryvalue) = 0) /\ (ge_balance_negative_constant_onetransport_resultentryvalue) = S ge_signed_half_constant_onetransport_resultentryvaluedecode))) /\ ((dst_positive_constant_onetransport_resultentry) + ge_balance_negative_constant_onetransport_resultentryvalue = (dst_negative_constant_onetransport_resultentry) + ge_balance_positive_constant_onetransport_resultentryvalue))))))))) -> du_value_constant_onetransport_result=2)))

Complete tactic proof in conservative notation

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

40 script commands · 9 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.

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 G
  4. L4
    intro hf
  5. L5
    intro hg
  6. L6
    intro he
02Separate the logical casesL7–8

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

  1. L7
    cases hf
  2. L8
    split
03Use earlier factsL9–9

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

  1. L9
    exact hg
04Fix variables and assumptionsL10–14

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

  1. L10
    intro i
  2. L11
    intro z
  3. L12
    intro hi
  4. L13
    intro hb
  5. L14
    intro hz
05Establish hvL15–21

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

  1. L15
    have hv : ∃ v. ArithAt(F,i,v)Definitions: ArithAt(F,i,v)Original native command in the exact edition
  2. L16
    specialize divisor_signed_table_lookup (N)
  3. L17
    specialize divisor_signed_table_lookup (F)
  4. L18
    specialize divisor_signed_table_lookup (i)
  5. L19
    apply divisor_signed_table_lookup
  6. L20
    exact hf_left
  7. L21
    exact hb
06Separate the logical casesL22–22

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

  1. L22
    cases hv
07Establish heqL23–32

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

  1. L23
    have heq : x=z
  2. L24
    specialize he (i)
  3. L25
    specialize he (x)
  4. L26
    specialize he (z)
  5. L27
    apply he
  6. L28
    exact hi
  7. L29
    exact hb
  8. L30
    exact hv_witness
  9. L31
    exact hz
  10. L32
    trans x
08Calculate and transport equalitiesL33–33

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

  1. L33
    symm
09Use earlier factsL34–40

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

  1. L34
    exact heq
  2. L35
    specialize hf_right (i)
  3. L36
    specialize hf_right (x)
  4. L37
    apply hf_right
  5. L38
    exact hi
  6. L39
    exact hb
  7. L40
    exact hv_witness

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro G
  4. 0004intro hf
  5. 0005intro hg
  6. 0006intro he
  7. 0007cases hf
  8. 0008split
  9. 0009exact hg
  10. 0010intro i
  11. 0011intro z
  12. 0012intro hi
  13. 0013intro hb
  14. 0014intro hz
  15. 0015have hv : ∃ v. ArithAt(F,i,v)
  16. 0016specialize divisor_signed_table_lookup (N)
  17. 0017specialize divisor_signed_table_lookup (F)
  18. 0018specialize divisor_signed_table_lookup (i)
  19. 0019apply divisor_signed_table_lookup
  20. 0020exact hf_left
  21. 0021exact hb
  22. 0022cases hv
  23. 0023have heq : x=z
  24. 0024specialize he (i)
  25. 0025specialize he (x)
  26. 0026specialize he (z)
  27. 0027apply he
  28. 0028exact hi
  29. 0029exact hb
  30. 0030exact hv_witness
  31. 0031exact hz
  32. 0032trans x
  33. 0033symm
  34. 0034exact heq
  35. 0035specialize hf_right (i)
  36. 0036specialize hf_right (x)
  37. 0037apply hf_right
  38. 0038exact hi
  39. 0039exact hb
  40. 0040exact hv_witness