ND0271 — FpPolyScale(p,k,ab,ac,bb,bc,l)

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

Definition in prerequisite notation

Lt(k,p) ∧ (∀ x. Lt(x,l) → ∃ y. ∃ z. BetaAt(ab,ac,x,y) ∧ (BetaAt(bb,bc,x,z) ∧ FpMul(p,k,y,z)))

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

Hygienic expanded first-order definition

((exists pfa_gap_lowertierscalar. pfa_gap_lowertierscalar + S ((k)) = ((p))) /\ ((forall pfp_index_lowertier. (exists pfa_gap_lowertierindex. pfa_gap_lowertierindex + S (pfp_index_lowertier) = ((l))) -> exists pfp_source_lowertier pfp_value_lowertier. ((((exists ff_h_pfp_lowertiersource. ff_h_pfp_lowertiersource + S (pfp_source_lowertier) = S ((S (pfp_index_lowertier)) * (ac))) /\ exists ff_q_pfp_lowertiersource. (ab) = ff_q_pfp_lowertiersource * S ((S (pfp_index_lowertier)) * (ac)) + (pfp_source_lowertier))) /\ (((((exists ff_h_pfp_lowertiertarget. ff_h_pfp_lowertiertarget + S (pfp_value_lowertier) = S ((S (pfp_index_lowertier)) * (bc))) /\ exists ff_q_pfp_lowertiertarget. (bb) = ff_q_pfp_lowertiertarget * S ((S (pfp_index_lowertier)) * (bc)) + (pfp_value_lowertier))) /\ ((((exists pfa_gap_lowertieroperationleft. pfa_gap_lowertieroperationleft + S ((k)) = ((p))) /\ (((exists pfa_gap_lowertieroperationright. pfa_gap_lowertieroperationright + S (pfp_source_lowertier) = ((p))) /\ ((((exists pfa_gap_lowertieroperationresultbound. pfa_gap_lowertieroperationresultbound + S (pfp_value_lowertier) = ((p))) /\ ((exists pfa_offset_left_lowertieroperationresultcongruence pfa_offset_right_lowertieroperationresultcongruence. (((k)) * (pfp_source_lowertier)) + ((p)) * pfa_offset_left_lowertieroperationresultcongruence = (pfp_value_lowertier) + ((p)) * pfa_offset_right_lowertieroperationresultcongruence))))))))))))))))

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)BetaAt(b,c,i,x)FpMul(p,a,b,c)

Definitions depending on this notation

FpMonicNormalization(p,k,ab,ac,bb,bc,L)

Checked theorems using this definition