We construct a common-action effective-field-theory interface between geometric–information relaxation and right-handed-neutrino condensation, retaining the distinction between configuration-space geometry and Lorentzian dynamics. A specified positive mediator operator bounds the induced four-Fermi susceptibility and excludes neutral condensation in a spectral parameter region. A derivative portal of the V20 form shifts the regulated mean-field gap equation, allowing a unique neutral threshold crossing when the bare coupling is supercritical and the statistical kinetic variable relaxes through the required value. The coupling's time dependence and its radial backreaction follow from the same action. At fixed statistical momentum and phase charge, a Routh reduction produces barriers at both the vanishing condensate and the degenerating kinetic coefficient. The reduced force is strictly increasing on the healthy interval: nonzero phase charge gives a unique positive stationary branch and rounds the neutral phase transition into a crossover. A two-reservoir Ward balance further yields a moving-equilibrium transport equation and a sufficient criterion for preserving condensate charge during exchange. Positive noise variance does not select a signed mean charge, and a configuration-space spectral bound does not establish a four-dimensional wormhole action. The companion Lean source imports the supplied V20 module, calls its CGICECore and UnifiedDynamics theorems, and extends the regulated-gap, transport and inequality evidence chains. This revision adds a complex rank–Takagi–ordering chain under explicit external mass inputs, and proves the algebraic freedom of complex mixing at fixed spectrum and flavor-singlet data. A restricted GY exponential ansatz also yields a scale-independent residual mass-ratio test. The new source compiles under Lean 4.34.0-rc1 (commit 3447a668) and Mathlib (commit 18accd59) with zero errors, zero sorry, and zero research axioms; the golden-gate #print axioms audit reports only propext / Classical.choice / Quot.sound. The derived restrictions and branch classification are conditional on explicit mediator, portal and initial-state inputs; measured neutrino masses, baryon yields and a quantum-gravity completion remain to be calculated.