RCLCombiner_isCoupling_iff
Why this theorem is linked from AoI-Aware Multi-Robot Sensing and Transport on Connected Graphs unclear
Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.
greedy water-filling algorithm that assigns robots according to marginal AoI reduction attains an optimal allocation (separable discretely convex problem)
Relation between the paper passage and the cited Recognition theorem.
plain-language theorem explainer
The equivalence shows that the RCL polynomial combiner with parameter c is a coupling combiner precisely when c is nonzero. Branch-selection arguments in the Recognition framework cite it to exclude the additive branch of the composition-law family. The proof rewrites the coupling predicate through the interaction-defect characterization and dispatches both directions by substitution plus a test-point evaluation.
Claim. Let $P_c(u,v) := 2u + 2v + c uv$. A combiner $P$ is coupling when it is not separately additive. Then $P_c$ is coupling if and only if $c ≠ 0$.
background
The Recognition Composition Law family is $F(xy) + F(x/y) = 2F(x) + 2F(y) + c F(x)F(y)$, realized by the polynomial combiner $P(u,v) = 2u + 2v + c uv$. The module distinguishes the bilinear branch ($c ≠ 0$, representative $J(x) = ½(x + x^{-1}) - 1$) from the additive branch ($c = 0$, representative ½(ln x)²). The strengthened (L4*) requires the combiner to be coupling rather than separately additive, which forces the bilinear branch.
proof idea
The proof rewrites the statement with isCouplingCombiner_iff_interactionDefect_nonzero. The forward direction assumes a pair with nonzero defect, supposes c = 0 for contradiction, substitutes the defect formula interactionDefect_RCLCombiner and obtains zero by ring. The reverse direction applies RCLCombiner_nonzero_couples at the test point (1,1) to exhibit a nonzero defect.
why it matters
This supplies the central equivalence for the downstream branch_selection theorem, which is the Lean rendering of the branch-selection result in RS_Branch_Selection.tex. It isolates the bilinear representative J of the RCL family, aligning with the J-uniqueness step (T5) of the forcing chain and the Recognition Composition Law. Residual α-coordinate freedom is deferred to separate calibration conditions outside this operator-level statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 30 of 68)
-
Fibonacci ring aggregation outperforms FedAvg in federated learning
"Corollary 4.2 (Fibonacci Directional Bias Preserved) ... aL ∈[α/2,(α+1)/2]"
-
Kuramoto flow fully described by Morse theory
"The flow of ψ in Q_I is topologically equivalent to the flow of the Perfect Morse potential M on T^d (Theorem 10.1)"
-
Convex factors let energy models scale to larger reasoning tasks
"nonnegative factor summation preserves convexity of the relaxed global objective... convex composition rules out spurious relaxed local minima"
-
Multi-gate residuals stabilize deep nets without extra comms cost
"gated mechanism replaces the rigid unitary gain with a learnable dissipative coefficient (1−gl) via a convex combination"
-
Deterministic (Δ+1)-coloring runs in 2^O(√log Δ) log n rounds
"oriented (η, γ)-list color space reduction … ∀v ∈ V : |L′_v| / β′(v) ≥ 1/γ · |L_v| / β(v)"
-
Ribbon knot Alexander polynomial factors as A(t) A(1/t) from singularities
"P=R-½I; Q=R^T+½I"
-
Annulus diagrams model noncrossing partitions for affine types
"The poset gNCA_c … graded lattice, rank function n minus number of non-annular blocks … cover relations via simple connectors … augmentation P ∪ κ"
-
Conservative reward estimator curbs overestimation in offline RL
"ˆQπ conservatively estimates the true Q-function … Qπ(s1,a1)−ˆQπ(s1,a1) > Qπ(s2,a2)−ˆQπ(s2,a2) when ¯π(a1|s1)<¯π(a2|s2)"
-
Rényi divergence keeps spectral estimates stable under frequency outliers
"Dα[S:eS] = 1/(1-α) min_{S'} [α D1[eS:S'] + (1-α) D1[S:S']] attained at S' = α eS + (1-α) S (Theorem 2)"
-
Colliders plus gravitational waves test radiative EWSB to 10^8 GeV
"exact and analytical solutions for the vacuum structure and scalar interactions... (mϕ, θ) parameterization"
-
Generalized means create infinite thermodynamic speed limits
"The TSLs with the arithmetic mean... and the one with the logarithmic mean... are the same as the ones in the previous studies [21,22]."
-
Log-likelihood strongly concave near true tree parameters
"Z_u = q(θ̂_v Z_v, θ̂_w Z_w) with q(x,y)=(x+y)/(1+xy); Hessian off-diagonals decay as (C9 δ)^⌊(dist(e,f)−1)/4⌋ (Prop. 3.2, Thm. 2.2)"
-
Fused geometry and appearance metric predicts synthetic data transfer
"We define SADGE as a bilinear interaction because it is the simplest function that captures complementarity while staying monotone and low-capacity. ... SADGE = a Ĝ + b  + c Ĝ  where a, b, c ≥ 0"
-
Importance sampling misallocates token credit in LLM RL
"This mismatch ... over-amplifying already high-probability tokens ... rich-get-richer dynamics"
-
Free energy minimization yields convergent policy composition
"The softmax gating rule emerges exactly from the proximal operator of the entropic barrier; as ε→0 the rule recovers argmax (sparse) or Gumbel-softmax (dense) gating."
-
Perturbing latents reawakens erased concepts in diffusion models
"Lorth = E [sum I[v_m^e ≠ v_d] |<v_m^e , v_d>| / (||v_m^e|| ||v_d||) + ξ]"
-
Reciprocal cost yields rank-one Hessian in log coordinates
"Theorem 2.1. Let F satisfy composition law F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y) and unit log-curvature lim 2F(e^t)/t²=1. Then F(x)=J(x)."
-
Trajectory selection gives 10x faster training and better out-of-domain web agents
"D(i, j) = max(δ(si, sj), δ(yi, yj)) with δ = 1 − BERTScore"
-
Sign-aware aggregation sustains unlearning across sequential VLM requests
"sign conflict occurs at parameter dimension i when ˆτ(a)_i · ˆτ(b)_i < 0"
-
Convex potential targets population-level balance in MoE
"RCLCombiner_isCoupling_iff ... branch_selection (c ≠ 0 forces bilinear branch)"
-
RI rankings compete with lasso for variable selection
"CRI.Z replaces reallocation term with identity, yielding w²_G = (VrU⊤_r y)⊙(VrU⊤_r y)"
-
Homotopy training lifts unrolled imaging PSNR by 2.5 dB
"g_α(x)=(1−α)½∥y−Hx∥²₂ + α½∥y_t−H_t x∥²₂ ... α:1→0 during training"
-
Adaptive gate skips retrieval for 70-90 percent of RAG queries
"Lemma 1 (order-equivalence). For any strictly decreasing ϕ, thresholding U_mar at τ is equivalent to thresholding the mean gap"
-
Single polynomial parametrizes all Riccati hierarchy solutions
"gi = xi xm for i < m, gm = x_m²"
-
Local positivity yields turnpike in mean field games
"the symmetry property(ii) is a symmetry property that is clear within the quadratic Hamiltonian framework by identity D¯u=-D¯m/¯m... (BB*)A*=A(BB*)"
-
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"