SignedZeroWindow(F,k,l)

forall sfs_index_dirichlet sfs_value_dirichlet. (exists pvs_le_gap_dirichletlower. pvs_le_gap_dirichletlower + ((k)) = (sfs_index_dirichlet)) -> (exists pvs_gap_dirichletupper. pvs_gap_dirichletupper + S (sfs_index_dirichlet) = ((l))) -> (exists dst_positive_code_dirichletentry dst_positive_scale_dirichletentry dst_negative_code_dirichletentry dst_negative_scale_dirichletentry dst_positive_dirichletentry dst_negative_dirichletentry. ((((F)) = (((((dst_positive_code_dirichletentry) + (dst_positive_scale_dirichletentry)) * S ((dst_positive_code_dirichletentry) + (dst_positive_scale_dirichletentry)) + ((dst_positive_scale_dirichletentry) + (dst_positive_scale_dirichletentry))) + (((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) * S ((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) + ((dst_negative_scale_dirichletentry) + (dst_negative_scale_dirichletentry)))) * S ((((dst_positive_code_dirichletentry) + (dst_positive_scale_dirichletentry)) * S ((dst_positive_code_dirichletentry) + (dst_positive_scale_dirichletentry)) + ((dst_positive_scale_dirichletentry) + (dst_positive_scale_dirichletentry))) + (((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) * S ((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) + ((dst_negative_scale_dirichletentry) + (dst_negative_scale_dirichletentry)))) + ((((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) * S ((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) + ((dst_negative_scale_dirichletentry) + (dst_negative_scale_dirichletentry))) + (((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) * S ((dst_negative_code_dirichletentry) + (dst_negative_scale_dirichletentry)) + ((dst_negative_scale_dirichletentry) + (dst_negative_scale_dirichletentry)))))) /\ (((((exists ff_h_pvs_dirichletentrypositive. ff_h_pvs_dirichletentrypositive + S (dst_positive_dirichletentry) = S ((S (sfs_index_dirichlet)) * dst_positive_scale_dirichletentry)) /\ exists ff_q_pvs_dirichletentrypositive. dst_positive_code_dirichletentry = ff_q_pvs_dirichletentrypositive * S ((S (sfs_index_dirichlet)) * dst_positive_scale_dirichletentry) + (dst_positive_dirichletentry))) /\ (((((exists ff_h_pvs_dirichletentrynegative. ff_h_pvs_dirichletentrynegative + S (dst_negative_dirichletentry) = S ((S (sfs_index_dirichlet)) * dst_negative_scale_dirichletentry)) /\ exists ff_q_pvs_dirichletentrynegative. dst_negative_code_dirichletentry = ff_q_pvs_dirichletentrynegative * S ((S (sfs_index_dirichlet)) * dst_negative_scale_dirichletentry) + (dst_negative_dirichletentry))) /\ (exists ge_balance_positive_dirichletentryvalue ge_balance_negative_dirichletentryvalue. (((((sfs_value_dirichlet) = 2 * (ge_balance_positive_dirichletentryvalue) /\ (ge_balance_negative_dirichletentryvalue) = 0) \/ exists ge_signed_half_dirichletentryvaluedecode. (((sfs_value_dirichlet) = 2 * ge_signed_half_dirichletentryvaluedecode + 1 /\ (ge_balance_positive_dirichletentryvalue) = 0) /\ (ge_balance_negative_dirichletentryvalue) = S ge_signed_half_dirichletentryvaluedecode))) /\ ((dst_positive_dirichletentry) + ge_balance_negative_dirichletentryvalue = (dst_negative_dirichletentry) + ge_balance_positive_dirichletentryvalue))))))))) -> sfs_value_dirichlet=0

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