ND0105 — SignedDeterminantNodeAt(b,c,i,d,pb,pc,nb,nc,p,n)

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

∃ mdr_z_secondwave. SignedDeterminantNodeCode(mdr_z_secondwave,d,pb,pc,nb,nc,p,n) ∧ BetaAt(b,c,i,mdr_z_secondwave)

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

Hygienic expanded first-order definition

exists mdr_z_secondwave. ((exists mdr_a_secondwavec mdr_b_secondwavec mdr_c_secondwavec mdr_e_secondwavec mdr_f_secondwavec. ((mdr_a_secondwavec = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_secondwavec = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_secondwavec = ((mdr_a_secondwavec) + (mdr_b_secondwavec)) * S ((mdr_a_secondwavec) + (mdr_b_secondwavec)) + ((mdr_b_secondwavec) + (mdr_b_secondwavec))) /\ ((mdr_e_secondwavec = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_secondwavec = ((nc) + (mdr_e_secondwavec)) * S ((nc) + (mdr_e_secondwavec)) + ((mdr_e_secondwavec) + (mdr_e_secondwavec))) /\ ((mdr_z_secondwave) = ((mdr_c_secondwavec) + (mdr_f_secondwavec)) * S ((mdr_c_secondwavec) + (mdr_f_secondwavec)) + ((mdr_f_secondwavec) + (mdr_f_secondwavec))))))))) /\ (((exists ff_h_mdr_secondwaveb. ff_h_mdr_secondwaveb + S (mdr_z_secondwave) = S ((S (i)) * c)) /\ exists ff_q_mdr_secondwaveb. b = ff_q_mdr_secondwaveb * S ((S (i)) * c) + (mdr_z_secondwave))))

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

Direct definition dependencies

SignedDeterminantNodeCode(z,d,pb,pc,nb,nc,p,n)BetaAt(b,c,i,x)

Definitions depending on this notation

SignedDeterminantChildPrefix(b,c,limit,pb,pc,nb,nc,q,eb,ec,fb,fc,l)SignedDeterminantHistory(b,c,l)SignedRecursiveDeterminant(pb,pc,nb,nc,d,p,n)

Checked theorems using this definition