Exact expanded first-order arithmetic statement
forall b c k. forall jt_divisor_one. (exists jt_factor_onemodulus. (1)=(jt_divisor_one)*jt_factor_onemodulus) -> (forall jt_index_onecoordinates jt_value_onecoordinates. (exists jt_gap_onecoordinatesindex. jt_gap_onecoordinatesindex+S (jt_index_onecoordinates)=(k)) -> (((exists fs_h_jt_onecoordinatesat. fs_h_jt_onecoordinatesat + S (jt_value_onecoordinates) = S ((S (jt_index_onecoordinates)) * c)) /\ exists fs_q_jt_onecoordinatesat. b = fs_q_jt_onecoordinatesat * S ((S (jt_index_onecoordinates)) * c) + (jt_value_onecoordinates))) -> (exists jt_factor_onecoordinatesdivides. (jt_value_onecoordinates)=(jt_divisor_one)*jt_factor_onecoordinatesdivides)) -> jt_divisor_one=1Constructive proof overview
Generated structural guide
Every finite tuple is primitive modulo one, including the zero tuple.
The unchanged tactic script uses 1 declared prerequisite and contains 9 exact native proof lines.
Alpha v35 checked-use · first admitted v35 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
divisor_one Alpha theorem; checked-use authorizedDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
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.