ND0132

ModularSetPullback(b,c,d,e,p,t)

The target is the actual translated pullback A−t: its bit at i equals A's bit at the canonical residue of i+t.

Conservative notation; not a theorem, primitive, or axiom.

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

Definition in prerequisite notation

∀ fms_i_secondwave. ∀ fms_j_secondwave. Lt(fms_i_secondwave,p) → Lt(fms_j_secondwave,p) → ModEq(p,fms_i_secondwave + t,fms_j_secondwave) → (BetaAt(d,e,fms_i_secondwave,1) → BetaAt(b,c,fms_j_secondwave,1)) ∧ (BetaAt(b,c,fms_j_secondwave,1) → BetaAt(d,e,fms_i_secondwave,1))

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
forall fms_i_secondwave fms_j_secondwave. (exists fms_gap_secondwave_i. fms_gap_secondwave_i + S (fms_i_secondwave) = (p)) -> (exists fms_gap_secondwave_j. fms_gap_secondwave_j + S (fms_j_secondwave) = (p)) -> (exists fms_u_secondwave fms_v_secondwave. (fms_i_secondwave + t) + (p) * fms_u_secondwave = (fms_j_secondwave) + (p) * fms_v_secondwave) -> ((((((exists fs_h_fms_secondwave_target. fs_h_fms_secondwave_target + S (1) = S ((S (fms_i_secondwave)) * e)) /\ exists fs_q_fms_secondwave_target. d = fs_q_fms_secondwave_target * S ((S (fms_i_secondwave)) * e) + (1))) -> (((exists fs_h_fms_secondwave_source. fs_h_fms_secondwave_source + S (1) = S ((S (fms_j_secondwave)) * c)) /\ exists fs_q_fms_secondwave_source. b = fs_q_fms_secondwave_source * S ((S (fms_j_secondwave)) * c) + (1)))) /\ ((((exists fs_h_fms_secondwave_source. fs_h_fms_secondwave_source + S (1) = S ((S (fms_j_secondwave)) * c)) /\ exists fs_q_fms_secondwave_source. b = fs_q_fms_secondwave_source * S ((S (fms_j_secondwave)) * c) + (1))) -> (((exists fs_h_fms_secondwave_target. fs_h_fms_secondwave_target + S (1) = S ((S (fms_i_secondwave)) * e)) /\ exists fs_q_fms_secondwave_target. d = fs_q_fms_secondwave_target * S ((S (fms_i_secondwave)) * e) + (1))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Lt(a,b)ModEq(m,a,b)BetaAt(b,c,i,x)

Definitions depending on this notation

none

Checked theorems using this definition

CD0021 · finite_modular_composition_pullbackCD0022 · finite_modular_set_pullback_existsCD0027 · finite_modular_pullback_membership_witnessCD0028 · finite_modular_pushforward_membership_witnessCD002E · finite_partial_sumset_succ_presentCD002F · finite_modular_sumset_prefix_existsCD0036 · finite_modular_dyson_upper_from_unionCD0037 · finite_modular_dyson_lower_from_pullbackCD0038 · finite_modular_dyson_transform_existsCD0044 · finite_modular_pullback_zero_memberCD0045 · finite_modular_opposite_translates_sum_coverCD0046 · prime_cauchy_davenport_cover_bound