def
definition
alphaProvenanceCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.AlphaDerivationExplicit on GitHub at line 55.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
used by
formal source
52 /-- RS threshold is positive -/
53 threshold_pos : 0 < phi - 3 / 2
54
55noncomputable def alphaProvenanceCert : AlphaProvenanceCert where
56 codata_in_band := codata_in_band
57 phi_is_golden := phi_golden_ratio
58 phi_gt_one := by linarith [phi_gt_onePointFive]
59 threshold_pos := by linarith [phi_gt_onePointFive]
60
61theorem alphaProvenance_inhabited : Nonempty AlphaProvenanceCert := ⟨alphaProvenanceCert⟩
62
63end AlphaDerivationExplicit
64end Foundation
65end IndisputableMonolith
papers checked against this theorem (showing 30 of 35)
-
FedMPO boosts federated multimodal graph accuracy by up to 5.65%
"Extensive experiments on 3 tasks across 6 datasets demonstrate... gains of up to 4.10% and 5.65%"
-
One learning rate transfers across all LLM scales
"optimal learning rate follows … T^{-0.32} … magic exponent"
-
One-loop lattice correction refines alpha_s from static energy
"We present early results for 1-loop lattice perturbation theory improvement of the Wilson loop and show how it improves the α_s extraction. We present a preliminary reanalysis of the TUMQCD (2+1)-flavor QCD data."
-
Bath embedding yields molecular spectra accurate to 0.1 eV at low cost
"ibDET provides accurate spectral properties with much reduced cost... errors... around 0.1 eV"
-
Allocations beat 1/4 MMS bound for large agent counts
"Theorem 1.1... α > 11/40 for n ≥ n_α... asymptotic solution to 2(12α−3)ln(3α)=(1−3α)(3ln3−4)"
-
Megawatt resonator aims to detect vacuum nonlinearity
"sideband amplitudes a± = i χ a0 a1* a2 ... χ = sqrt(π/2) ξ K F / |sin θ| ... SNR formula (23) with integration time τ"
-
Neural operators beat MLPs at function interpolation using fewer parameters
"A TFNO ensemble reaches a held-out root-mean-square error of 198.2 keV"
-
Southern dense cores share C/O ratios of 0.5-0.7
"best fit model ... C/O ratios of 0.5-0.7 ... chemical ages ... 0.6 and 5 Myr"
-
Duality maps black holes to nuclei and caps stable charge at 82
"α_s = 0.7, σ = 0.1 GeV² (as used in description of quarkonia), and m = 0.33 GeV. ... the eigenvalues ε_n are proportional to √n; assuming that n equals the integer part of A^(2/3), the cavity radii r* then scale as R_0 A^(1/3), with R_0 ≈ 1 fm"
-
Complex kernels expose dominant harmonics in high-dimensional data
"Both the kernel bandwidth σ and the complex parameter ω are selected via grid search."
-
Spin-density wave creates second plateau in 3D Hall effect
"M0 = 9.02 meV, M1 vx vy = −1.58 eV·nm², Mz = 13.1 meV·nm², Dz = −4.58 meV·nm², carrier density n0 = 1.7×10^17 cm⁻³"
-
Cosmology shifts to Big Bang 2.0 needing new physics
"Estimations based on quantum field theory suggest the vacuum energy should be ∼10^113 joules per cubic meter, whereas observations indicate ∼10^−9 joules per cubic meter. This discrepancy of ∼10^120 is the 'cosmological constant problem'."
-
Twistor strings produce glueball trajectories with Lüscher intercept
"√σ ≈ 0.412136 GeV, mu ≈ 0.134247 GeV, ms ≈ 0.221086 GeV, mc ≈ 1.44844 GeV, mb ≈ 4.78122 GeV (five fitted parameters)"
-
DFT parameters feed scale-bridging simulations of cobalt ferrite magnetism
"Current challenges, e.g., U-parameter sensitivity, realistic surface chemistry, spin-lattice coupling, and large-scale integration are discussed."
-
More participants fail to boost UAV federated RL performance
"Spearman rank correlation coefficients between final success rate and KER... ρ = 0.37 (Chemical), ρ = 0.70 (Fire)."
-
Simulations match galaxy luminosities from far-UV to submm
"The colibre model is calibrated by adjusting up to four subgrid parameters ... that control the strengths of stellar and AGN feedback in order to reproduce simple observed galaxy scaling relations at z=0: the galaxy stellar mass function (GSMF) and the galaxy size-stellar mass relation (SSMR)."
-
Feshbach-Villars equation extended to two spin-0 particles
"We take the fine structure constant α=e²/(ℏc)=0.0072973525643≃1/137.035999177."
-
Multi-task network runs real-time driver monitoring on embedded hardware
"Safeness Score = λ₁ S_perclos − λ₂ S_mouth − λ₃(1−S_head) − λ₄(1−S_action) ... where λᵢ denotes the weight assigned to each contribution."
-
Graphene enables custom THz light devices
"graphene ... displays ... a frequency independent absorption/layer of απ ≈ 2.3 %, being α the fine constant"
-
Symmetry counting gives closed-form surface code error rates
"L ≈ A(p/p_th)^{d_e} with A ≈ 2.09·10^-1 and p_th ≈ 7.33·10^-2 fit empirically from path counting"
-
Spinning charged particles orbit chaotically off the equator near black holes
"We introduce for convenience the dimensionless quantities ... E, L, S, and magnetic parameter B ... The radius of ISCO decreases with the increase of the magnetic field B or spin S."
-
f(T) models approach ΛCDM but violate strong energy condition
"Using parameterization of the deceleration parameter q(z) and the corresponding H(z) expression, we constrain the model parameters with the recent Hubble parameter and BAO data through a Markov Chain Monte Carlo (MCMC) approach."
-
Flow-matching super-resolves ground astro images without fakes
"AdamW (lr=1e-4), 300 epochs, batch size 32, λ_SNR=50, η₀=0.5, σ_PSF=2"
-
Pauli-Fierz energy at zero momentum scales as Λ^{3/2}
"4√π/√3 gΛ^{3/2} ≤ E^{g,Λ}_G ≤ 4√(3π) gΛ^{3/2} for all g>0 and Λ > (3/(8π)) g^{-2}."
-
Bivariate Hawkes processes near criticality limit to rough Volterra system
"Mittag-Leffler kernels K_i defined through their Laplace transform: cKᵢ(z) = 1/(1 + δ̃ᵢ z^αᵢ), with αᵢ ∈ (1/2, 1) free parameters fitted to empirical equity microstructure (H ≈ 0.1)."
-
Infrared cutoffs in parton showers shape hadron-level results
"We conclude by studying the models' tunability and identifying the best-fit parameters for each... αs(mZ) ∈ [0.106, 0.130], p²T,min ∈ [0.5, 1.5], Clmax ∈ [2.5, 4.5]."
-
Hadrons modify photon paths in lensing without phenomenological models
"δ = π(1 − √(2/(2−K))) + (2m/b)(1 + 1/(1 − (ω_h/ω_∞)²))"
-
Deepfakes show unstable trajectories on latent energy surfaces
"The framework is operationalized via a learned diagonal mass matrix M(q), step size η, evolution length T=4, regularization weights λ, λ_geo, λ_photo, and a hinge margin γ — all tuned hyperparameters with no closed-form derivation."
-
Milky Way trends predict galaxy abundances across cosmic time
"We adopt the rise-fall star-formation history... allow the following to vary: t_start, τ1, τ2, SFE, and the outflow mass-loading factor η."
-
Risk-gated AI cuts wireless control response time by 23-27%
"Threshold parameters τ_commit, τ_reject, τ_degraded, δ, d_min, b_min, ε_trust ... All thresholds are frozen before evaluation."