SS001C

divisor_signed_table_reindex_functional

All actual pullbacks of the same signed table and map agree in canonical value, even when their component representatives differ.

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

∀ F. ∀ G. ∀ H. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ r. ∀ s. ∀ l. MatrixMinorFourCode(F,pb,pc,nb,nc) → ArithReindex(F,G,r,s,l) → ArithReindex(F,H,r,s,l) → ArithTableEqual(G,H,l)

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

Definition DAG

MatrixMinorFourCode(z,up,us,un,ut) · 1ArithAt(F,i,z) · 1ArithTableEqual(F,G,l) · 1ArithReindex(F,G,r,s,l) · 2BetaAt(b,c,i,x) · 1

Actual proof prerequisites

beta_at_exists · checked external prerequisitedivisor_signed_table_lookup_from_componentsdivisor_signed_table_at_functional
Original expanded first-order statement 
forall F G H pb pc nb nc r s l. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))))) -> (forall dsr_index_functional_first dsr_image_functional_first dsr_value_functional_first. (exists pvs_gap_functional_firstbound. pvs_gap_functional_firstbound + S (dsr_index_functional_first) = (l)) -> (((exists ff_h_pvs_functional_firstmap. ff_h_pvs_functional_firstmap + S (dsr_image_functional_first) = S ((S (dsr_index_functional_first)) * s)) /\ exists ff_q_pvs_functional_firstmap. r = ff_q_pvs_functional_firstmap * S ((S (dsr_index_functional_first)) * s) + (dsr_image_functional_first))) -> (exists dst_positive_code_functional_firstsource dst_positive_scale_functional_firstsource dst_negative_code_functional_firstsource dst_negative_scale_functional_firstsource dst_positive_functional_firstsource dst_negative_functional_firstsource. (((F) = (((((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) * S ((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) + ((dst_positive_scale_functional_firstsource) + (dst_positive_scale_functional_firstsource))) + (((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource)))) * S ((((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) * S ((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) + ((dst_positive_scale_functional_firstsource) + (dst_positive_scale_functional_firstsource))) + (((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource)))) + ((((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource))) + (((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource)))))) /\ (((((exists ff_h_pvs_functional_firstsourcepositive. ff_h_pvs_functional_firstsourcepositive + S (dst_positive_functional_firstsource) = S ((S (dsr_image_functional_first)) * dst_positive_scale_functional_firstsource)) /\ exists ff_q_pvs_functional_firstsourcepositive. dst_positive_code_functional_firstsource = ff_q_pvs_functional_firstsourcepositive * S ((S (dsr_image_functional_first)) * dst_positive_scale_functional_firstsource) + (dst_positive_functional_firstsource))) /\ (((((exists ff_h_pvs_functional_firstsourcenegative. ff_h_pvs_functional_firstsourcenegative + S (dst_negative_functional_firstsource) = S ((S (dsr_image_functional_first)) * dst_negative_scale_functional_firstsource)) /\ exists ff_q_pvs_functional_firstsourcenegative. dst_negative_code_functional_firstsource = ff_q_pvs_functional_firstsourcenegative * S ((S (dsr_image_functional_first)) * dst_negative_scale_functional_firstsource) + (dst_negative_functional_firstsource))) /\ (exists ge_balance_positive_functional_firstsourcevalue ge_balance_negative_functional_firstsourcevalue. (((((dsr_value_functional_first) = 2 * (ge_balance_positive_functional_firstsourcevalue) /\ (ge_balance_negative_functional_firstsourcevalue) = 0) \/ exists ge_signed_half_functional_firstsourcevaluedecode. (((dsr_value_functional_first) = 2 * ge_signed_half_functional_firstsourcevaluedecode + 1 /\ (ge_balance_positive_functional_firstsourcevalue) = 0) /\ (ge_balance_negative_functional_firstsourcevalue) = S ge_signed_half_functional_firstsourcevaluedecode))) /\ ((dst_positive_functional_firstsource) + ge_balance_negative_functional_firstsourcevalue = (dst_negative_functional_firstsource) + ge_balance_positive_functional_firstsourcevalue))))))))) -> (exists dst_positive_code_functional_firsttarget dst_positive_scale_functional_firsttarget dst_negative_code_functional_firsttarget dst_negative_scale_functional_firsttarget dst_positive_functional_firsttarget dst_negative_functional_firsttarget. (((G) = (((((dst_positive_code_functional_firsttarget) + (dst_positive_scale_functional_firsttarget)) * S ((dst_positive_code_functional_firsttarget) + (dst_positive_scale_functional_firsttarget)) + ((dst_positive_scale_functional_firsttarget) + (dst_positive_scale_functional_firsttarget))) + (((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) * S ((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) + ((dst_negative_scale_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)))) * S ((((dst_positive_code_functional_firsttarget) + (dst_positive_scale_functional_firsttarget)) * S ((dst_positive_code_functional_firsttarget) + (dst_positive_scale_functional_firsttarget)) + ((dst_positive_scale_functional_firsttarget) + (dst_positive_scale_functional_firsttarget))) + (((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) * S ((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) + ((dst_negative_scale_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)))) + ((((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) * S ((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) + ((dst_negative_scale_functional_firsttarget) + (dst_negative_scale_functional_firsttarget))) + (((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) * S ((dst_negative_code_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)) + ((dst_negative_scale_functional_firsttarget) + (dst_negative_scale_functional_firsttarget)))))) /\ (((((exists ff_h_pvs_functional_firsttargetpositive. ff_h_pvs_functional_firsttargetpositive + S (dst_positive_functional_firsttarget) = S ((S (dsr_index_functional_first)) * dst_positive_scale_functional_firsttarget)) /\ exists ff_q_pvs_functional_firsttargetpositive. dst_positive_code_functional_firsttarget = ff_q_pvs_functional_firsttargetpositive * S ((S (dsr_index_functional_first)) * dst_positive_scale_functional_firsttarget) + (dst_positive_functional_firsttarget))) /\ (((((exists ff_h_pvs_functional_firsttargetnegative. ff_h_pvs_functional_firsttargetnegative + S (dst_negative_functional_firsttarget) = S ((S (dsr_index_functional_first)) * dst_negative_scale_functional_firsttarget)) /\ exists ff_q_pvs_functional_firsttargetnegative. dst_negative_code_functional_firsttarget = ff_q_pvs_functional_firsttargetnegative * S ((S (dsr_index_functional_first)) * dst_negative_scale_functional_firsttarget) + (dst_negative_functional_firsttarget))) /\ (exists ge_balance_positive_functional_firsttargetvalue ge_balance_negative_functional_firsttargetvalue. (((((dsr_value_functional_first) = 2 * (ge_balance_positive_functional_firsttargetvalue) /\ (ge_balance_negative_functional_firsttargetvalue) = 0) \/ exists ge_signed_half_functional_firsttargetvaluedecode. (((dsr_value_functional_first) = 2 * ge_signed_half_functional_firsttargetvaluedecode + 1 /\ (ge_balance_positive_functional_firsttargetvalue) = 0) /\ (ge_balance_negative_functional_firsttargetvalue) = S ge_signed_half_functional_firsttargetvaluedecode))) /\ ((dst_positive_functional_firsttarget) + ge_balance_negative_functional_firsttargetvalue = (dst_negative_functional_firsttarget) + ge_balance_positive_functional_firsttargetvalue)))))))))) -> (forall dsr_index_functional_second dsr_image_functional_second dsr_value_functional_second. (exists pvs_gap_functional_secondbound. pvs_gap_functional_secondbound + S (dsr_index_functional_second) = (l)) -> (((exists ff_h_pvs_functional_secondmap. ff_h_pvs_functional_secondmap + S (dsr_image_functional_second) = S ((S (dsr_index_functional_second)) * s)) /\ exists ff_q_pvs_functional_secondmap. r = ff_q_pvs_functional_secondmap * S ((S (dsr_index_functional_second)) * s) + (dsr_image_functional_second))) -> (exists dst_positive_code_functional_secondsource dst_positive_scale_functional_secondsource dst_negative_code_functional_secondsource dst_negative_scale_functional_secondsource dst_positive_functional_secondsource dst_negative_functional_secondsource. (((F) = (((((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) * S ((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) + ((dst_positive_scale_functional_secondsource) + (dst_positive_scale_functional_secondsource))) + (((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource)))) * S ((((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) * S ((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) + ((dst_positive_scale_functional_secondsource) + (dst_positive_scale_functional_secondsource))) + (((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource)))) + ((((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource))) + (((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource)))))) /\ (((((exists ff_h_pvs_functional_secondsourcepositive. ff_h_pvs_functional_secondsourcepositive + S (dst_positive_functional_secondsource) = S ((S (dsr_image_functional_second)) * dst_positive_scale_functional_secondsource)) /\ exists ff_q_pvs_functional_secondsourcepositive. dst_positive_code_functional_secondsource = ff_q_pvs_functional_secondsourcepositive * S ((S (dsr_image_functional_second)) * dst_positive_scale_functional_secondsource) + (dst_positive_functional_secondsource))) /\ (((((exists ff_h_pvs_functional_secondsourcenegative. ff_h_pvs_functional_secondsourcenegative + S (dst_negative_functional_secondsource) = S ((S (dsr_image_functional_second)) * dst_negative_scale_functional_secondsource)) /\ exists ff_q_pvs_functional_secondsourcenegative. dst_negative_code_functional_secondsource = ff_q_pvs_functional_secondsourcenegative * S ((S (dsr_image_functional_second)) * dst_negative_scale_functional_secondsource) + (dst_negative_functional_secondsource))) /\ (exists ge_balance_positive_functional_secondsourcevalue ge_balance_negative_functional_secondsourcevalue. (((((dsr_value_functional_second) = 2 * (ge_balance_positive_functional_secondsourcevalue) /\ (ge_balance_negative_functional_secondsourcevalue) = 0) \/ exists ge_signed_half_functional_secondsourcevaluedecode. (((dsr_value_functional_second) = 2 * ge_signed_half_functional_secondsourcevaluedecode + 1 /\ (ge_balance_positive_functional_secondsourcevalue) = 0) /\ (ge_balance_negative_functional_secondsourcevalue) = S ge_signed_half_functional_secondsourcevaluedecode))) /\ ((dst_positive_functional_secondsource) + ge_balance_negative_functional_secondsourcevalue = (dst_negative_functional_secondsource) + ge_balance_positive_functional_secondsourcevalue))))))))) -> (exists dst_positive_code_functional_secondtarget dst_positive_scale_functional_secondtarget dst_negative_code_functional_secondtarget dst_negative_scale_functional_secondtarget dst_positive_functional_secondtarget dst_negative_functional_secondtarget. (((H) = (((((dst_positive_code_functional_secondtarget) + (dst_positive_scale_functional_secondtarget)) * S ((dst_positive_code_functional_secondtarget) + (dst_positive_scale_functional_secondtarget)) + ((dst_positive_scale_functional_secondtarget) + (dst_positive_scale_functional_secondtarget))) + (((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) * S ((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) + ((dst_negative_scale_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)))) * S ((((dst_positive_code_functional_secondtarget) + (dst_positive_scale_functional_secondtarget)) * S ((dst_positive_code_functional_secondtarget) + (dst_positive_scale_functional_secondtarget)) + ((dst_positive_scale_functional_secondtarget) + (dst_positive_scale_functional_secondtarget))) + (((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) * S ((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) + ((dst_negative_scale_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)))) + ((((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) * S ((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) + ((dst_negative_scale_functional_secondtarget) + (dst_negative_scale_functional_secondtarget))) + (((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) * S ((dst_negative_code_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)) + ((dst_negative_scale_functional_secondtarget) + (dst_negative_scale_functional_secondtarget)))))) /\ (((((exists ff_h_pvs_functional_secondtargetpositive. ff_h_pvs_functional_secondtargetpositive + S (dst_positive_functional_secondtarget) = S ((S (dsr_index_functional_second)) * dst_positive_scale_functional_secondtarget)) /\ exists ff_q_pvs_functional_secondtargetpositive. dst_positive_code_functional_secondtarget = ff_q_pvs_functional_secondtargetpositive * S ((S (dsr_index_functional_second)) * dst_positive_scale_functional_secondtarget) + (dst_positive_functional_secondtarget))) /\ (((((exists ff_h_pvs_functional_secondtargetnegative. ff_h_pvs_functional_secondtargetnegative + S (dst_negative_functional_secondtarget) = S ((S (dsr_index_functional_second)) * dst_negative_scale_functional_secondtarget)) /\ exists ff_q_pvs_functional_secondtargetnegative. dst_negative_code_functional_secondtarget = ff_q_pvs_functional_secondtargetnegative * S ((S (dsr_index_functional_second)) * dst_negative_scale_functional_secondtarget) + (dst_negative_functional_secondtarget))) /\ (exists ge_balance_positive_functional_secondtargetvalue ge_balance_negative_functional_secondtargetvalue. (((((dsr_value_functional_second) = 2 * (ge_balance_positive_functional_secondtargetvalue) /\ (ge_balance_negative_functional_secondtargetvalue) = 0) \/ exists ge_signed_half_functional_secondtargetvaluedecode. (((dsr_value_functional_second) = 2 * ge_signed_half_functional_secondtargetvaluedecode + 1 /\ (ge_balance_positive_functional_secondtargetvalue) = 0) /\ (ge_balance_negative_functional_secondtargetvalue) = S ge_signed_half_functional_secondtargetvaluedecode))) /\ ((dst_positive_functional_secondtarget) + ge_balance_negative_functional_secondtargetvalue = (dst_negative_functional_secondtarget) + ge_balance_positive_functional_secondtargetvalue)))))))))) -> (forall dst_index_functional_result dst_first_functional_result dst_second_functional_result. (exists pvs_gap_functional_resultbound. pvs_gap_functional_resultbound + S (dst_index_functional_result) = (l)) -> (exists dst_positive_code_functional_resultfirst dst_positive_scale_functional_resultfirst dst_negative_code_functional_resultfirst dst_negative_scale_functional_resultfirst dst_positive_functional_resultfirst dst_negative_functional_resultfirst. (((G) = (((((dst_positive_code_functional_resultfirst) + (dst_positive_scale_functional_resultfirst)) * S ((dst_positive_code_functional_resultfirst) + (dst_positive_scale_functional_resultfirst)) + ((dst_positive_scale_functional_resultfirst) + (dst_positive_scale_functional_resultfirst))) + (((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) * S ((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) + ((dst_negative_scale_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)))) * S ((((dst_positive_code_functional_resultfirst) + (dst_positive_scale_functional_resultfirst)) * S ((dst_positive_code_functional_resultfirst) + (dst_positive_scale_functional_resultfirst)) + ((dst_positive_scale_functional_resultfirst) + (dst_positive_scale_functional_resultfirst))) + (((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) * S ((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) + ((dst_negative_scale_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)))) + ((((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) * S ((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) + ((dst_negative_scale_functional_resultfirst) + (dst_negative_scale_functional_resultfirst))) + (((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) * S ((dst_negative_code_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)) + ((dst_negative_scale_functional_resultfirst) + (dst_negative_scale_functional_resultfirst)))))) /\ (((((exists ff_h_pvs_functional_resultfirstpositive. ff_h_pvs_functional_resultfirstpositive + S (dst_positive_functional_resultfirst) = S ((S (dst_index_functional_result)) * dst_positive_scale_functional_resultfirst)) /\ exists ff_q_pvs_functional_resultfirstpositive. dst_positive_code_functional_resultfirst = ff_q_pvs_functional_resultfirstpositive * S ((S (dst_index_functional_result)) * dst_positive_scale_functional_resultfirst) + (dst_positive_functional_resultfirst))) /\ (((((exists ff_h_pvs_functional_resultfirstnegative. ff_h_pvs_functional_resultfirstnegative + S (dst_negative_functional_resultfirst) = S ((S (dst_index_functional_result)) * dst_negative_scale_functional_resultfirst)) /\ exists ff_q_pvs_functional_resultfirstnegative. dst_negative_code_functional_resultfirst = ff_q_pvs_functional_resultfirstnegative * S ((S (dst_index_functional_result)) * dst_negative_scale_functional_resultfirst) + (dst_negative_functional_resultfirst))) /\ (exists ge_balance_positive_functional_resultfirstvalue ge_balance_negative_functional_resultfirstvalue. (((((dst_first_functional_result) = 2 * (ge_balance_positive_functional_resultfirstvalue) /\ (ge_balance_negative_functional_resultfirstvalue) = 0) \/ exists ge_signed_half_functional_resultfirstvaluedecode. (((dst_first_functional_result) = 2 * ge_signed_half_functional_resultfirstvaluedecode + 1 /\ (ge_balance_positive_functional_resultfirstvalue) = 0) /\ (ge_balance_negative_functional_resultfirstvalue) = S ge_signed_half_functional_resultfirstvaluedecode))) /\ ((dst_positive_functional_resultfirst) + ge_balance_negative_functional_resultfirstvalue = (dst_negative_functional_resultfirst) + ge_balance_positive_functional_resultfirstvalue))))))))) -> (exists dst_positive_code_functional_resultsecond dst_positive_scale_functional_resultsecond dst_negative_code_functional_resultsecond dst_negative_scale_functional_resultsecond dst_positive_functional_resultsecond dst_negative_functional_resultsecond. (((H) = (((((dst_positive_code_functional_resultsecond) + (dst_positive_scale_functional_resultsecond)) * S ((dst_positive_code_functional_resultsecond) + (dst_positive_scale_functional_resultsecond)) + ((dst_positive_scale_functional_resultsecond) + (dst_positive_scale_functional_resultsecond))) + (((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) * S ((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) + ((dst_negative_scale_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)))) * S ((((dst_positive_code_functional_resultsecond) + (dst_positive_scale_functional_resultsecond)) * S ((dst_positive_code_functional_resultsecond) + (dst_positive_scale_functional_resultsecond)) + ((dst_positive_scale_functional_resultsecond) + (dst_positive_scale_functional_resultsecond))) + (((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) * S ((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) + ((dst_negative_scale_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)))) + ((((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) * S ((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) + ((dst_negative_scale_functional_resultsecond) + (dst_negative_scale_functional_resultsecond))) + (((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) * S ((dst_negative_code_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)) + ((dst_negative_scale_functional_resultsecond) + (dst_negative_scale_functional_resultsecond)))))) /\ (((((exists ff_h_pvs_functional_resultsecondpositive. ff_h_pvs_functional_resultsecondpositive + S (dst_positive_functional_resultsecond) = S ((S (dst_index_functional_result)) * dst_positive_scale_functional_resultsecond)) /\ exists ff_q_pvs_functional_resultsecondpositive. dst_positive_code_functional_resultsecond = ff_q_pvs_functional_resultsecondpositive * S ((S (dst_index_functional_result)) * dst_positive_scale_functional_resultsecond) + (dst_positive_functional_resultsecond))) /\ (((((exists ff_h_pvs_functional_resultsecondnegative. ff_h_pvs_functional_resultsecondnegative + S (dst_negative_functional_resultsecond) = S ((S (dst_index_functional_result)) * dst_negative_scale_functional_resultsecond)) /\ exists ff_q_pvs_functional_resultsecondnegative. dst_negative_code_functional_resultsecond = ff_q_pvs_functional_resultsecondnegative * S ((S (dst_index_functional_result)) * dst_negative_scale_functional_resultsecond) + (dst_negative_functional_resultsecond))) /\ (exists ge_balance_positive_functional_resultsecondvalue ge_balance_negative_functional_resultsecondvalue. (((((dst_second_functional_result) = 2 * (ge_balance_positive_functional_resultsecondvalue) /\ (ge_balance_negative_functional_resultsecondvalue) = 0) \/ exists ge_signed_half_functional_resultsecondvaluedecode. (((dst_second_functional_result) = 2 * ge_signed_half_functional_resultsecondvaluedecode + 1 /\ (ge_balance_positive_functional_resultsecondvalue) = 0) /\ (ge_balance_negative_functional_resultsecondvalue) = S ge_signed_half_functional_resultsecondvaluedecode))) /\ ((dst_positive_functional_resultsecond) + ge_balance_negative_functional_resultsecondvalue = (dst_negative_functional_resultsecond) + ge_balance_positive_functional_resultsecondvalue))))))))) -> dst_first_functional_result = dst_second_functional_result)

Complete tactic proof in conservative notation

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

63 script commands · 12 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 (2)
divisor signed table lookup from componentsdivisor signed table at functional
01Fix variables and assumptionsL1–10

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro H
  4. L4
    intro pb
  5. L5
    intro pc
  6. L6
    intro nb
  7. L7
    intro nc
  8. L8
    intro r
  9. L9
    intro s
  10. L10
    intro l
02Fix variables and assumptionsL11–19

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

  1. L11
    intro hrep
  2. L12
    intro hG
  3. L13
    intro hH
  4. L14
    intro i
  5. L15
    intro u
  6. L16
    intro v
  7. L17
    intro hi
  8. L18
    intro hu
  9. L19
    intro hv
03Establish hmapL20–24

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

  1. L20
    have hmap : ∃ j. BetaAt(r,s,i,j)Definitions: BetaAt(r,s,i,j)Original native command in the exact edition
  2. L21
    specialize beta_at_exists (r)
  3. L22
    specialize beta_at_exists (s)
  4. L23
    specialize beta_at_exists (i)
  5. L24
    apply beta_at_exists
04Separate the logical casesL25–25

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

  1. L25
    cases hmap
05Establish hsourceL26–34

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

  1. L26
    have hsource : ∃ z. ArithAt(F,x,z)Definitions: ArithAt(F,x,z)Original native command in the exact edition
  2. L27
    specialize divisor_signed_table_lookup_from_components (F)
  3. L28
    specialize divisor_signed_table_lookup_from_components (pb)
  4. L29
    specialize divisor_signed_table_lookup_from_components (pc)
  5. L30
    specialize divisor_signed_table_lookup_from_components (nb)
  6. L31
    specialize divisor_signed_table_lookup_from_components (nc)
  7. L32
    specialize divisor_signed_table_lookup_from_components (x)
  8. L33
    apply divisor_signed_table_lookup_from_components
  9. L34
    exact hrep
06Separate the logical casesL35–35

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

  1. L35
    cases hsource
07Calculate and transport equalitiesL36–36

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

  1. L36
    trans x1
08Use earlier factsL37–46

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

  1. L37
    specialize divisor_signed_table_at_functional (G)
  2. L38
    specialize divisor_signed_table_at_functional (i)
  3. L39
    specialize divisor_signed_table_at_functional (u)
  4. L40
    specialize divisor_signed_table_at_functional (x1)
  5. L41
    apply divisor_signed_table_at_functional
  6. L42
    exact hu
  7. L43
    specialize hG (i)
  8. L44
    specialize hG (x)
  9. L45
    specialize hG (x1)
  10. L46
    apply hG
09Use earlier factsL47–49

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

  1. L47
    exact hi
  2. L48
    exact hmap_witness
  3. L49
    exact hsource_witness
10Calculate and transport equalitiesL50–50

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

  1. L50
    symm
11Use earlier factsL51–60

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

  1. L51
    specialize divisor_signed_table_at_functional (H)
  2. L52
    specialize divisor_signed_table_at_functional (i)
  3. L53
    specialize divisor_signed_table_at_functional (v)
  4. L54
    specialize divisor_signed_table_at_functional (x1)
  5. L55
    apply divisor_signed_table_at_functional
  6. L56
    exact hv
  7. L57
    specialize hH (i)
  8. L58
    specialize hH (x)
  9. L59
    specialize hH (x1)
  10. L60
    apply hH
12Use earlier factsL61–63

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

  1. L61
    exact hi
  2. L62
    exact hmap_witness
  3. L63
    exact hsource_witness

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro H
  4. 0004intro pb
  5. 0005intro pc
  6. 0006intro nb
  7. 0007intro nc
  8. 0008intro r
  9. 0009intro s
  10. 0010intro l
  11. 0011intro hrep
  12. 0012intro hG
  13. 0013intro hH
  14. 0014intro i
  15. 0015intro u
  16. 0016intro v
  17. 0017intro hi
  18. 0018intro hu
  19. 0019intro hv
  20. 0020have hmap : ∃ j. BetaAt(r,s,i,j)
  21. 0021specialize beta_at_exists (r)
  22. 0022specialize beta_at_exists (s)
  23. 0023specialize beta_at_exists (i)
  24. 0024apply beta_at_exists
  25. 0025cases hmap
  26. 0026have hsource : ∃ z. ArithAt(F,x,z)
  27. 0027specialize divisor_signed_table_lookup_from_components (F)
  28. 0028specialize divisor_signed_table_lookup_from_components (pb)
  29. 0029specialize divisor_signed_table_lookup_from_components (pc)
  30. 0030specialize divisor_signed_table_lookup_from_components (nb)
  31. 0031specialize divisor_signed_table_lookup_from_components (nc)
  32. 0032specialize divisor_signed_table_lookup_from_components (x)
  33. 0033apply divisor_signed_table_lookup_from_components
  34. 0034exact hrep
  35. 0035cases hsource
  36. 0036trans x1
  37. 0037specialize divisor_signed_table_at_functional (G)
  38. 0038specialize divisor_signed_table_at_functional (i)
  39. 0039specialize divisor_signed_table_at_functional (u)
  40. 0040specialize divisor_signed_table_at_functional (x1)
  41. 0041apply divisor_signed_table_at_functional
  42. 0042exact hu
  43. 0043specialize hG (i)
  44. 0044specialize hG (x)
  45. 0045specialize hG (x1)
  46. 0046apply hG
  47. 0047exact hi
  48. 0048exact hmap_witness
  49. 0049exact hsource_witness
  50. 0050symm
  51. 0051specialize divisor_signed_table_at_functional (H)
  52. 0052specialize divisor_signed_table_at_functional (i)
  53. 0053specialize divisor_signed_table_at_functional (v)
  54. 0054specialize divisor_signed_table_at_functional (x1)
  55. 0055apply divisor_signed_table_at_functional
  56. 0056exact hv
  57. 0057specialize hH (i)
  58. 0058specialize hH (x)
  59. 0059specialize hH (x1)
  60. 0060apply hH
  61. 0061exact hi
  62. 0062exact hmap_witness
  63. 0063exact hsource_witness