theorem
proved
RCLCombiner_isCoupling_iff
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.BranchSelection on GitHub at line 145.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
interactionDefect_RCLCombiner -
IsCouplingCombiner -
isCouplingCombiner_iff_interactionDefect_nonzero -
RCLCombiner -
RCLCombiner_nonzero_couples -
of -
required -
is -
of -
is -
of -
is -
of -
is -
calibration -
and
used by
formal source
142 simpa using hc
143
144/-- **The RCL combiner is a coupling combiner iff `c ≠ 0`.** -/
145theorem RCLCombiner_isCoupling_iff (c : ℝ) :
146 IsCouplingCombiner (RCLCombiner c) ↔ c ≠ 0 := by
147 rw [isCouplingCombiner_iff_interactionDefect_nonzero]
148 constructor
149 · rintro ⟨u, v, huv⟩
150 intro hc
151 apply huv
152 rw [interactionDefect_RCLCombiner, hc]
153 ring
154 · intro hc
155 exact ⟨1, 1, RCLCombiner_nonzero_couples c hc⟩
156
157/-! ## Branch Selection Theorem -/
158
159/-- **Branch selection by non-degeneracy.**
160
161If the RCL polynomial combiner is required to be a coupling combiner
162(the strengthened (L4*) of the companion paper), then the parameter
163`c` is forced to be nonzero. Equivalently, the additive branch
164(`c = 0`, with calibrated representative `½(ln x)²`) is excluded.
165
166This is the branch-selection theorem of `RS_Branch_Selection.tex` in
167its Lean form. The bilinear branch is forced; `J` is the
168`α = 1` representative of the bilinear `α`-family. The residual
169`α`-coordinate freedom is acknowledged in §5 of the paper and is
170addressed by separate generator-calibration / higher-derivative /
171action-functional conditions, none of which are part of the
172operator-level Aristotelian content. -/
173theorem branch_selection (c : ℝ)
174 (hCoupling : IsCouplingCombiner (RCLCombiner c)) :
175 c ≠ 0 :=
papers checked against this theorem (showing 30 of 43)
-
Affordance cues and progress signals lift robot success to 91.8%
"fine-grained affordance queries comprise four subqueries <Global>, <Local>, <Spatial>, and <Dynamic>"
-
f-divergence MI matrices are PSD for nonnegative power-series generators
"replica embedding turns monomial (t-1)^m into Gram matrices; nonnegative mixtures preserve PSD"
-
Degree-10 polynomial divides no Newman polynomial
"solving the system of linear inequations ... 0 ≤ c_k ≤ 1 ... using the mixed-integer linear programming package Gurobi"
-
Accelerated Sinkhorn reaches O(n^{7/3}ε^{-5/3}) for partial transport
"Lemma 1. Define the Lipschitz constant L = ||A||_{1→2}^2 / μ_f where μ_f = γ / (||r||_1 + ||c||_1 − s)."
-
LLM posteriors form curved manifolds in representation space
"parameter posteriors are encoded as curved manifolds in representation space... Standard linear steering moves representations off-manifold, inducing unintended, coupled changes, whereas geometry-aware methods preserve the target belief family"
-
Bonding descriptors raise ML accuracy for materials properties
"bonding heterogeneity (skew, kurtosis of BWDF) and effective interaction number (EIN ICOHP) reduce lattice thermal conductivity; significant MAE gains for max pfc, klat, moduli"
-
Necessity-operator closures factorize fuzzy formal contexts
"we will consider the frame ([0,1],≤,&G) … ⊤-normalized context … g↑N ≤ g↑π … intervals of concepts"
-
Dynamic inhibition sets neural assembly sizes
"inhibition process based on the ratio between excitatory and inhibitory neurons ... pi=0.2"
-
Probability gradients plus asymmetric decay stabilize soft clipping
"Left Boundary: A positive integer power function of πθ... Right Boundary: A reciprocal radical power function of πθ... Cleft = (1−εlow)−n π−(n+1)θold ... Cright = (1+εhigh)1/m π1/m−1θold"
-
Alphabet growth boosts shuffled privacy only on collapse to delta_1
"Diluting/persistent dichotomy: family diluting iff worst ν_adbd,d ⇒ δ1 (equivalently I*→0); persistent otherwise, no extra d-gain"
-
Stationary velocity field makes flow matching adaptive for robots
"g⋆(a,ε,γ)=(ε−a)c(γ) with c(1)=0... transforming ground-truth action sequences into natural stationary equilibrium points"
-
Bandit-guided distributed design cuts regret in black-box experiments
"Kriging Believer variance deflation σ^(j)²(x) = σ^(0)²(x) − Σ k(x,x^(l))² / (σ²(x^(l)) + σ_n²)"
-
Wrapper makes any network normalization-equivariant
"WNE is parameter-free; it exactly parameterizes the NE class without constraining internal layers."
-
Quadratic cost correction lifts VLA success 28.8% in dynamic scenes
"From a single quadratic cost, joint minimization yields a unified solution that decomposes orthogonally into two distinct channels. The pace channel compresses execution along the planned direction, while the path channel applies an orthogonal spatial offset"
-
Web video pretraining yields strong zero-shot monocular 3D
"Multi-View Signal Proxy (MVS) ... Pt,t+1 = rH / rF ... MVS(v) = average Pt,t+1"
-
VALOR lifts B2B revenue 2.7x by ranking persuadable accounts
"Treatment-Gated Interaction Module... bilinear gating operation: Interaction(X, T) = (W_x X + b_x) ⊙ σ(W_t T + b_t)"
-
Neural network learns SBL updates that beat classical MM rules
"γ^{j+1} = (T1(γ^j)/T2(γ^j))^p γ^j ... valid descent step for common majorizer"
-
Penalizing singular subspace rotations improves LLM OOD performance
"the pretrained singular basis is not identical to the Fisher eigenspace, its strong overlap with Fisher-projected gradient energy indicates that dominant singular directions provide a useful low-rank structural proxy for loss-sensitive curvature directions."
-
Brain-like networks map internal states to native explanations
"structural plasticity usage score U_ij = normalised mutual information"
-
Algebraic latent transitions lift VLA success from 48% to 85% on MetaWorld
"joint flow-matching objective... co-generate latent transition trajectories and robot action trajectories"
-
Contractive law adapts Koopman models online safely
"Jinfo := log det(Ĝk + εI) … D-optimal active learning objective"
-
Similarity regularization speeds LLM pretraining by over 30%
"enlarging multi-classification margins … m_k ≥ m_k + δ∥ϵ+∥ + √2 L_P γ"
-
Every (n-2) subspace of R^n holds vector with ratio >= n/2-1
"Lemma 4 … Tr(A) ≤ 2 … rank(A) ≤ 2 … ||A||∞ ≤ 1"
-
Joint location-scale minimization degenerates on product manifolds
"The balance equation compares the two scaled squared factor distances through a bounded relative contrast... α↦hα(Z;m) is nondecreasing, and it is strictly increasing whenever A>0 and B>0."
-
Symmetric generators tighten equivalence-query round bounds
"RCLCombiner ... interactionDefect ... IsCouplingCombiner ... branch_selection"
-
Autoencoder gains injectivity guarantee via separation regularization
"Definition 2 ((δ,ϵ)-separation)... dN(f(x),f(y))/dM(x,y) > ϵ ... Theorem 1: f is injective iff (δ,ϵ)-separated"
-
Condition number bounds clustering error from objective gap
"Phase transitions: Δ/D > 2 + 2/√c_b (k-means) vs. 2 + 1/c_b (linear loss); exact recovery when κ_means < c_b/4 or κ_med < c_b (Theorem 4.1)"
-
Integer transfer rules solve conservation laws exactly
"Theorem 2.5 (Transfer-operator equivalence under quantisation)... distinct classical fluxes collapse to identical dynamics whenever they induce the same integer transfer rule"
-
Quality-Aware Exploration Budget Allocation for Cooperative Multi-Agent Reinforcement Learning
"RSQ_i = μ_i² / (μ_i² + σ_i² + ε); h(RSQ_i) = clip(1 + λ(RSQ_i − RSQ_ref), h_min, h_max)"
-
LQ-GM-PID supplies closed-form bridge diffusions
"V_t(x) = ½(x−ν_t)ᵀ β_t (x−ν_t) ... Riccati equations and closed-form optimal feedback."