M2Nonsingular curvature operator and Lyapunov candidate
Master systems
PASS · LIMIT CHECKThe complex-safe regularized reciprocal and curvature-feedback operator. Positivity of the modulus-squared denominator removes the historical scalar zero; this does not by itself prove global PDE stability or uniqueness.
$$R_\varepsilon(\psi) := \frac{\overline{\psi}} {|\psi|^2+\varepsilon^2e^{-2\alpha|\psi|^2}},
\Theta_\varepsilon[\psi] := -(\Delta\psi)R_\varepsilon(\psi).
R_\varepsilon(\psi)\longrightarrow \frac1\psi \qquad(\varepsilon\to0).
\mathcal E_{\rm WCT}[\psi] = \int_\Omega \left( |\nabla\psi|^2+|\Theta_\varepsilon[\psi]|^2 \right)\,dx.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_regularized_denominator · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
M3Finite-band spectral selector
Master systems
PASS · SIGN OR EXTREMUM CHECKA Swift–Hohenberg-type finite-band selector whose Fourier symbol damps modes away from the preferred shell. It establishes the linear spectral rail, not global nonlinear pattern selection.
$$\partial_tA = \mu A-g|A|^2A-b(\Delta+k_\star^2)^2A, \qquad b>0.
-b\bigl(|k|^2-k_\star^2\bigr)^2,$$
The assigned executable check is reported under its declared assumptions.
Checker: check_master_sh_sign · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
M4Dimensional stability threshold
Master systems
PASS · FORMAL THEOREMThe standard Sobolev threshold H²→L∞ for integer spatial dimension n≤3. This is a regularity threshold and not, by itself, a universal theorem that all stable confinement is impossible above three dimensions.
$$H^2(\Omega)\hookrightarrow L^\infty(\Omega) \quad\text{when}\quad 2>\frac n2.
n\le3.$$
The standard Sobolev embedding threshold H2 to L-infinity holds under the declared domain hypotheses for integer spatial dimension n less than or equal to 3.
Checker: check_h2_embedding_threshold · Scope: STANDARD MATHEMATICS · Lean: PROVED · Empirical: NOT APPLICABLE
- This standard embedding theorem is not by itself a complete nonlinear WCT stability theorem.
M7Full curvature-wavefield equation
Master systems
PASS · SIGN OR EXTREMUM CHECKCurrent effective status: ✅ PASS The explicit negative fourth-order term supplies finite-band ultraviolet damping. Other dynamical claims require separate analysis.
$$\partial_t\psi = \mathcal N_{\rm curv}[\psi] +g|\psi|^2\psi +c_1(\Delta+\sigma^2)\psi -c_2(\Delta+k_\star^2)^2\psi +i\,c_3m\psi +c_4R^{-(2+n/p)}\psi +\eta\psi\circ\xi(t), \qquad c_2>0.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_master_uwct_sign · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
The canonical registered object for curvature-rate density; consult the source equation and verification metadata for its assumptions and scientific boundary.
$$\sigma_{\rm dens}(s)=\kappa(s)^2+\tau(s)^2, \qquad [\sigma_{\rm dens}]=L^{-2}.$$
The curvature-rate density has inverse-length-squared dimension.
Checker: check_e1a · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
The canonical registered object for curvature spectral rate; consult the source equation and verification metadata for its assumptions and scientific boundary.
$$\sigma(s)=\sqrt{\kappa(s)^2+\tau(s)^2}, \qquad [\sigma]=L^{-1}.$$
The curvature spectral rate has inverse-length dimension.
Checker: check_e1b · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
The normalized weighted loop average for a nonnegative weight with nonzero total weight. It preserves the dimension of the averaged quantity but does not select a physical weighting measure.
$$\langle f\rangle_w = \frac{\oint_\Gamma w(s)f(s)\,ds} {\oint_\Gamma w(s)\,ds}.$$
The positive weighted-average construction has a nonzero denominator and preserves the encoded dimension of the averaged quantity.
Checker: check_weighted_average · Scope: STANDARD MATHEMATICS · Lean: PROVED · Empirical: NOT APPLICABLE
A constrained phase-curvature mismatch action. Nonnegative weighting makes its squared mismatch term nonnegative; existence and uniqueness of continuum minimizers require separate analysis.
$$S_{\rm eff}[\varphi] = \oint_\Gamma w(\partial_s\varphi-\sigma)^2\,ds + \Lambda \left( \oint_\Gamma\partial_s\varphi\,ds-2\pi n \right), \qquad n\in\mathbb Z.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_locking_variation · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Current effective status: ✅ PASS Stationarity gives
$$\partial_s\varphi = \sigma+\frac{\alpha_{\rm lock}}{w},
\alpha_{\rm lock} = \frac{ 2\pi n-\oint_\Gamma\sigma\,ds }{ \oint_\Gamma ds/w },$$
The assigned executable check is reported under its declared assumptions.
Checker: check_locking_solution · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
The effective-wavenumber identification connecting phase winding, integrated curvature, and the weighted curvature average. The chain is derived only under compatible orientation, exact integrated locking, and a positive constant-weight condition.
$$L_s:=\oint_\Gamma ds, \qquad k_{\rm wind}:=\frac{2\pi|n|}{L_s}, \qquad k_\sigma:=\frac1{L_s}\oint_\Gamma\sigma\,ds.
k_{\rm wind}=k_\sigma=\langle\sigma\rangle_w$$
Exact loop closure and the declared orientation and weighting assumptions establish the encoded effective-wavenumber chain.
Checker: check_effective_wavenumber_chain_derived · Scope: MODEL CONDITIONAL · Lean: PROVED · Empirical: NOT TESTED
- This does not independently establish that physical particle masses are generated by the model.
Status history: CONDITIONAL → PASS via derived_overrides.yaml:check_effective_wavenumber_chain_derived.
A dimensionally consistent mapping from an effective inverse-length scale to rest energy and mass. The PASS establishes dimensional closure, not that WCT dynamics generates observed particle masses.
$$E_{\rm rest}=\hbar c\,k_{\rm eff}, \qquad m=\frac{\hbar}{c}k_{\rm eff}.
m=\frac{\hbar}{c}\langle\sigma\rangle_w.$$
The encoded mass-curvature relation has the dimensions of mass.
Checker: check_mass_curvature_dimensions · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
- Dimensional closure does not establish the physical identification of mass with curvature.
The solenoidal form of the mass-curvature mapping using an averaged curve-curvature magnitude. Its physical prediction requires a specified averaging measure and a dynamically selected geometry.
$$m = \frac{\hbar}{c} \left\langle \sqrt{\kappa^2+\tau^2} \right\rangle_\Gamma.$$
The solenoidal curvature average has the dimensions required by the stated mass relation.
Checker: check_mass_curvature_dimensions · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
- The averaging measure and physical identification require separate justification.
Current effective status: ✅ PASS Substituting E4 gives
$$\boxed{ \oint_\Gamma w\,\partial_s\varphi\,ds = \oint_\Gamma w\,\sigma\,ds + \alpha_{\rm lock}L_s }.
2\pi\oint ds/\oint ds/w$$
The assigned executable check is reported under its declared assumptions.
Checker: check_e8_identity · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
The phase-current identity obtained from a supplied polar representation of the complex field. The finite algebraic identity does not replace a function-space proof of full polar differentiation and conservation dynamics.
$$\mathbf S(x,t)=u(x,t)\nabla\theta(x,t).
\partial_tu+\nabla\cdot\mathbf S=0.$$
Polar decomposition yields the normalized phase-current identity under the declared nonzero-field assumptions.
Checker: check_phase_flux_from_polar_field · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
Status history: DEFINITION → PASS via derived_overrides.yaml:check_phase_flux_from_polar_field.
Current effective status: ✅ PASS Both sides are dimensionless.
$$\int_{r_1}^{r_2}k_r(r)\,dr=2\pi n, \qquad n\in\mathbb Z.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_shell_quantization_dimensions · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS provided \(\psi\neq0\) on the loop and the phase is continuous modulo \(2\pi\).
$$m(\gamma) = \frac1{2\pi} \oint_\gamma\nabla\theta\cdot d\boldsymbol\ell \in\mathbb Z,$$
The assigned executable check is reported under its declared assumptions.
Checker: check_winding_dimensions · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
The quartic finite-band dispersion relation with a stationary maximum at the selected nonzero wavenumber. It verifies the preferred linear shell and damping sign.
$$\lambda_{\rm grow}(k) = r+a|k|^2-b|k|^4, \qquad a,b>0.
k_\star=\sqrt{\frac{a}{2b}}.
\lambda_{\rm grow}(k) = \mu-b(|k|^2-k_\star^2)^2, \qquad \mu=r+\frac{a^2}{4b}.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_dispersion_stationary_point · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
The registered finite-band amplitude evolution equation. Its gradient-flow form follows under the stated functional and sign convention; nonlinear existence and long-time selection remain separate obligations.
$$\partial_tA = (r-a\Delta-b\Delta^2)A-\beta|A|^2A,
\partial_tA = \mu A-b(\Delta+k_\star^2)^2A-\beta|A|^2A.$$
The declared band-pass amplitude equation follows from negative gradient flow of the registered functional.
Checker: check_bandpass_gradient_flow · Scope: MODEL CONDITIONAL · Lean: PROVED · Empirical: NOT TESTED
Status history: CONDITIONAL → PASS via derived_overrides.yaml:check_bandpass_gradient_flow.
The energy functional associated with the finite-band amplitude equation. The variational relation is supported under exact negative gradient flow, while full functional-analytic Lyapunov theory remains conditional.
$$\mathcal E[A] = \int_\Omega \left[ -\mu|A|^2 +b|(\Delta+k_\star^2)A|^2 +\frac{\beta}{2}|A|^4 \right]dx.$$
The registered functional generates the declared band-pass gradient flow under the stated sign convention.
Checker: check_bandpass_gradient_flow · Scope: MODEL CONDITIONAL · Lean: PROVED · Empirical: NOT TESTED
Status history: CONDITIONAL → PASS via derived_overrides.yaml:check_bandpass_gradient_flow.
Current effective status: ✅ PASS For the linearized dynamics,
$$P_k(t)=P_k(0)e^{2\lambda_{\rm grow}(k)t}.
\operatorname*{arg\,max}_kP_k(t)\to k_\star.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_linear_spectral_growth · Scope: INTERNAL CONSISTENCY · Lean: OPEN · Empirical: NOT TESTED
Current effective status: ✅ PASS For \(\varepsilon>0\), the denominator is strictly positive for all complex \(\psi\). This replaces
$$R_\varepsilon(\psi) = \frac{\overline\psi} {|\psi|^2+\varepsilon^2e^{-2\alpha|\psi|^2}},
\boxed{ \Theta_\varepsilon[\psi] = -(\Delta\psi)R_\varepsilon(\psi) }.
-\Delta\psi/(\psi+\varepsilon e^{-\alpha|\psi|^2})$$
The assigned executable check is reported under its declared assumptions.
Checker: check_regularized_denominator · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
A WCT energy candidate whose nonnegative terms and exact negative-gradient-flow hypothesis imply monotone descent. The full chain rule and PDE well-posedness are not established by the algebraic PASS.
$$\mathcal E[\psi] = \int_\Omega \left( c_1|\nabla\psi|^2 +c_2|\Theta_\varepsilon[\psi]|^2 \right)dx.$$
Exact negative gradient flow gives monotone energy descent when the registered nonnegativity assumptions hold.
Checker: check_lyapunov_gradient_flow · Scope: MODEL CONDITIONAL · Lean: PROVED · Empirical: NOT TESTED
Status history: CONDITIONAL → PASS via derived_overrides.yaml:check_lyapunov_gradient_flow.
Current effective status: ✅ PASS Let
$$S:=\frac{\Box\psi}{g(\psi)}, \qquad P:=\frac{\Delta\psi}{g(\psi)}.
Q(S,P)=\kappa S^2+\theta P^2-\gamma SP.
\kappa\ge0,\qquad \theta\ge0,\qquad \gamma^2\le4\kappa\theta.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_cavity_quadratic_form · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Current effective status: ✅ PASS For \(\mathcal L(\psi,\partial\psi,\partial^2\psi)\),
$$\frac{\delta\mathcal L}{\delta\psi} = \frac{\partial\mathcal L}{\partial\psi} -\partial_\mu \frac{\partial\mathcal L}{\partial(\partial_\mu\psi)} +\partial_\mu\partial_\nu \frac{\partial\mathcal L} {\partial(\partial_\mu\partial_\nu\psi)} =0.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_second_order_el_template · Scope: INTERNAL CONSISTENCY · Lean: OPEN · Empirical: NOT TESTED
The H²-to-L∞ Sobolev embedding threshold used by the dimensionality argument. It supplies a standard regularity condition, not a complete nonlinear stability theorem.
$$H^2(\Omega)\hookrightarrow L^\infty(\Omega) \quad\Longrightarrow\quad 2>\frac n2.
n\le3.$$
The standard H2-to-L-infinity Sobolev embedding threshold is verified under the declared domain hypotheses.
Checker: check_h2_embedding_threshold · Scope: STANDARD MATHEMATICS · Lean: PROVED · Empirical: NOT APPLICABLE
- The theorem supplies a regularity route and does not characterize every possible confinement mechanism.
Current effective status: ✅ PASS If \(\psi\in H^2(\Omega)\) and
$$|R_\varepsilon(\psi(x))|\le\delta^{-1} \quad\text{a.e.},
\boxed{ \|\Theta_\varepsilon[\psi]\|_{L^2} \le \delta^{-1}\|\Delta\psi\|_{L^2} }.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_theta_l2_from_h2 · Scope: INTERNAL CONSISTENCY · Lean: DEFINITION · Empirical: NOT TESTED
Current effective status: ✅ PASS Let \(\rhot(n)\in(0,1]\) be retained fractions. Define
$$\alpha(n) = 1+\frac1n\sum_{t=1}^{m(n)}\log_2\rho_t(n) +\beta(n).
\beta(n) < -\frac1n\sum_t\log_2\rho_t(n).$$
The assigned executable check is reported under its declared assumptions.
Checker: check_alpha_drop_corrected · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Current effective status: ✅ PASS Iteration gives
$$M_{t+1}\le e^{-\Delta_t}M_t, \qquad \Delta_t\ge0.
M_T \le M_0\exp\!\left(-\sum_{t=0}^{T-1}\Delta_t\right).$$
The assigned executable check is reported under its declared assumptions.
Checker: check_state_decay_iteration · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
The normalized Shannon entropy of a finite spectral distribution and its standard bounds. This is a standard information-theoretic identity rather than a WCT-specific physical result.
$$H_k=-\sum_kP_k\ln P_k.
0\le H_k\le\ln K.$$
The normalized spectral Shannon entropy satisfies its standard finite-support bounds.
Checker: check_entropy_bounds · Scope: STANDARD MATHEMATICS · Lean: OPEN · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS For a distribution supported on \(Kt\) modes,
$$H_k(t)\le\ln K_t,
\boxed{ e^{H_k(t)}\le K_t }.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_support_entropy_bound · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Current effective status: ✅ PASS with dimensionless \(C1\).
$$k_{\max} = C_1\frac{E_{\max}}{\hbar c},$$
The assigned executable check is reported under its declared assumptions.
Checker: check_bandlimit_dimensions · Scope: INTERNAL CONSISTENCY · Lean: OPEN · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS In three spatial dimensions,
$$N_{\rm lanes} \le C_2Vk_{\max}^3,$$
The assigned executable check is reported under its declared assumptions.
Checker: check_channel_capacity_dimensions · Scope: INTERNAL CONSISTENCY · Lean: OPEN · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS where
$$\boxed{ Q_{\rm eff} = \omega\frac{U}{P_{\rm loss}} }
U=\int_\Omega u\,dV$$
The assigned executable check is reported under its declared assumptions.
Checker: check_q_factor_dimensions · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS At stationarity,
$$\boxed{ \frac{dW}{dt} = P_{\rm in} + P_{\rm fusion} - P_{\rm loss} - P_{\rm out} }.
P_{\rm in}+P_{\rm fusion} = P_{\rm loss}+P_{\rm out}.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_power_balance_form · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
The dimensionally corrected relation between an effective spectral gap and squared effective mass. Dimensional consistency does not determine the gap dynamically or calibrate an observed mass spectrum.
$$\omega_j^2=c^2\lambda_j+\Delta_\omega^\star, \qquad [\Delta_\omega^\star]=T^{-2},
\omega^2=c^2k^2+\frac{m_{\rm eff}^2c^4}{\hbar^2}
\boxed{ m_{\rm eff}^2 = \frac{\hbar^2}{c^4}\Delta_\omega^\star }.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_effective_mass_gap_dimensions · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS For a smooth scalar denominator \(D\neq0\), define
$$\Theta_D[\psi]:=-\frac{\Delta\psi}{D}.
[\nabla,\Theta_D]\psi := \nabla(\Theta_D[\psi])-\Theta_D[\nabla\psi] = \frac{\Delta\psi}{D^2}\nabla D.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_curvature_gradient_commutator · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Current effective status: ✅ PASS It is the local curvature contribution to E18.
$$p_\Theta(x) := c_2|\Theta_\varepsilon[\psi](x)|^2.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_pressure_density_embedding · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS Its Fourier symbol is
$$\mathcal{SH}[A] = (\Delta+k_\star^2)^2A.
(|k|^2-k_\star^2)^2.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_sh_fourier_symbol · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
The band-selective Green kernel. A positive spectral offset yields positivity and the bound G(k)≤1/r; the offset and its physical interpretation remain model assumptions.
$$\mathcal L=r+a(\Delta+k_\star^2)^2,
G(k) = \frac1{r+a(|k|^2-k_\star^2)^2}.$$
A strictly positive spectral offset bounds the declared Green kernel and removes the registered pole.
Checker: check_green_kernel_bounded · Scope: MODEL CONDITIONAL · Lean: PROVED · Empirical: NOT TESTED
Status history: CONDITIONAL → PASS via derived_overrides.yaml:check_green_kernel_bounded.
Current effective status: ✅ PASS With a fixed annulus,
$$\mathcal A^\star := \left\{ k\in\mathbb Z^d: \bigl||k|-k_\star\bigr|\le\Delta k \right\},
(P_{k_\star}A)(x) = \sum_{k\in\mathcal A^\star} \widehat A_ke^{ik\cdot x}.
P_{k_\star}^2=P_{k_\star}.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_projection_idempotence · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Current effective status: ✅ PASS In the continuum,
$$r_c = \min_k a(|k|^2-k_\star^2)^2 = 0.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_pattern_threshold · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Current effective status: ✅ PASS For nonzero total spectral energy,
$$\eta(t) = \frac{ \sum_{k\in\mathcal A^\star}|\widehat A_k|^2 }{ \sum_k|\widehat A_k|^2 }, \qquad 0\le\eta(t)\le1.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_spectral_fraction_bounds · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Current effective status: ✅ PASS From E12,
$$k_\star=\sqrt{\frac{a}{2b}}.
\boxed{ \lambda_\star = \frac{2\pi}{k_\star} = 2\pi\sqrt{\frac{2b}{a}} }.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_e12_e64_consistency · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Current effective status: ✅ PASS For \(n>2\),
$$p_c(n)=\frac{n+2}{n-2}.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_critical_sobolev_exponent · Scope: INTERNAL CONSISTENCY · Lean: DEFINITION · Empirical: NOT TESTED
The failure, in general, of the H²-to-L∞ embedding above three spatial dimensions. This blocks that regularity route but does not exclude every possible higher-dimensional confinement mechanism.
$$\text{No standalone display equation recorded.}$$
The general H2-to-L-infinity embedding route fails above three spatial dimensions under the declared Sobolev framework.
Checker: check_h2_embedding_threshold · Scope: STANDARD MATHEMATICS · Lean: PROVED · Empirical: NOT APPLICABLE
- Failure of this regularity route does not exclude every conceivable higher-dimensional confinement mechanism.
Current effective status: ✅ PASS If
$$\psi\in H^s(\Omega), \qquad s>\frac n2+2,
\Theta_\varepsilon[\psi]\in L^\infty(\Omega).$$
The assigned executable check is reported under its declared assumptions.
Checker: check_theta_linf_from_high_regularity · Scope: INTERNAL CONSISTENCY · Lean: DEFINITION · Empirical: NOT TESTED
Current effective status: ✅ PASS With normalized spectral weights \(pk\),
$$\boxed{ \xi_{\rm coh} = \left( \sum_kp_k|k|^2 \right)^{-1/2} }.
\boxed{ \xi_{\rm coh} = \sqrt{ \frac{\int_\Omega|\psi|^2dx} {\int_\Omega|\nabla\psi|^2dx} } }.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_coherence_length_dimensions · Scope: INTERNAL CONSISTENCY · Lean: DEFINITION · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS For the real one-dimensional reduction
$$q:=-\frac{\psi_{xx}}{\psi}-\sigma_\star^2,
\boxed{ q\frac{\psi_{xx}}{\psi^2} -\psi_{xx} -\frac{d^2}{dx^2}\left(\frac q\psi\right) =0 }.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_cle2_variation · Scope: INTERNAL CONSISTENCY · Lean: OPEN · Empirical: NOT TESTED
The canonical registered object for locked-field equation; consult the source equation and verification metadata for its assumptions and scientific boundary.
$$-\Delta\psi = \sigma_\star^2\psi.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_cle_units_chain · Scope: INTERNAL CONSISTENCY · Lean: OPEN · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS For
$$\psi(\theta,\phi)=f(\theta)g(\phi),
\frac{f''}{f} + \frac{R^2}{r^2}\frac{g''}{g} = -\sigma_\star^2R^2.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_separation_substitution · Scope: INTERNAL CONSISTENCY · Lean: OPEN · Empirical: NOT TESTED
Current effective status: ✅ PASS The periodic reduced equation
$$f''+m^2f=0
\boxed{ f(\theta)=A\cos(m\theta)+B\sin(m\theta), \qquad m\in\mathbb Z_{\ge0} }.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_periodic_ode_family · Scope: INTERNAL CONSISTENCY · Lean: OPEN · Empirical: NOT TESTED
Current effective status: ✅ PASS For \(\sigma\star=mec/\hbar\),
$$R=\frac1{\sigma_\star}.
R=\frac{\hbar}{m_ec}\approx386.16\ {\rm fm}.$$
The registered electron-radius expression has the dimensions and numerical scale of the reduced Compton wavelength.
Checker: check_cle_units_chain · Scope: INTERNAL CONSISTENCY · Lean: OPEN · Empirical: NOT APPLICABLE
- Reproducing a known length scale does not establish an independent WCT derivation of electron structure.
The canonical registered object for curvature scalar chain; consult the source equation and verification metadata for its assumptions and scientific boundary.
$$\boxed{ W_\psi = -\frac{\Delta\psi}{\psi} = \sigma_\star^2 }, \qquad R=\sigma_\star^{-1}.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_cle_units_chain · Scope: INTERNAL CONSISTENCY · Lean: OPEN · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS For \(E>0\) and \(E0>0\),
$$\delta_g(E) = A_g\cos\!\left( k_\ell\ln\frac E{E_0}+\phi \right),
|\delta_g(E)|\le|A_g|.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_log_modulation · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Current effective status: ✅ PASS For a positive real field \(\psi>0\), let
$$u=\ln\psi, \qquad \psi=e^u.
\nabla\psi=e^u\nabla u,
\Delta\psi=e^u(\Delta u+|\nabla u|^2),
\frac{\Delta\psi}{\psi} = \Delta u+|\nabla u|^2.$$
The assigned executable check is reported under its declared assumptions.
Checker: check_log_laplacian_identity · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS If
$$\partial_tu = \Delta u+|\nabla u|^2,$$
The assigned executable check is reported under its declared assumptions.
Checker: check_log_flow_reduction · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS With
$$\psi=e^u,
\partial_t\psi = e^u\partial_tu = e^u(\Delta u+|\nabla u|^2) = \Delta\psi.
\boxed{\partial_t\psi=\Delta\psi}.$$
The registered Cole-Hopf substitution reduces the encoded nonlinear equation under its stated assumptions.
Checker: check_cole_hopf · Scope: STANDARD MATHEMATICS · Lean: PROVED · Empirical: NOT APPLICABLE
Current effective status: ✅ PASS Baseline status: ○ OPEN
$$\dot\delta_\gamma=v_\gamma, \qquad \dot v_\gamma=-c_s^2k^2\delta_\gamma-k^2\Phi,
\dot\delta_b=v_b, \qquad \dot v_b=-\mathcal R c_s^2k^2\delta_\gamma-k^2\Phi.$$
The first-order velocity system is equivalent to the registered second-order oscillator system.
Checker: check_cm9_first_order_equivalence · Scope: INTERNAL CONSISTENCY · Lean: PROVED · Empirical: NOT TESTED
Status history: OPEN → PASS via derived_overrides.yaml:check_cm9_first_order_equivalence.
Current effective status: ✅ PASS Baseline status: ○ OPEN
$$D(k) = \exp\!\left(-\frac{k^2}{k_D^2}\right),
k_D^{-2} = \int_0^{t_\star}D_{\rm curv}(t)\,dt.$$
The registered curvature-diffusion equation integrates to the stated Gaussian damping envelope.
Checker: check_cm11_gaussian_damping · Scope: MODEL CONDITIONAL · Lean: OPEN · Empirical: NOT TESTED
Status history: OPEN → PASS via derived_overrides.yaml:check_cm11_gaussian_damping.