gap4_curvature_coupling_blocker
plain-language theorem explainer
For any nonzero curvature proxy ρ, the single- and double-coupling curved Lichnerowicz extensions agree on the entire zero-curvature specialization yet differ at every resolution when ρ ≠ 0, while both eigenvalue families satisfy the same C/N² curvature-correction rate bound. Gravity and discrete-spectrum workers cite this as the certified Gap 4 blocker: flat spectrum plus generic consistency cannot fix the curved coupling. The proof is a four-component term packaging two extension lemmas and two rate-bound instances.
Claim. For every real $\rho \neq 0$: (i) the single-coupling and double-coupling curvature extensions agree on every lattice tensor field at every resolution when the curvature proxy is zero; (ii) those two operator families are unequal as maps at every resolution when the curvature proxy equals $\rho$; (iii) the discrete/continuum eigenvalue branches with coupling coefficient $1$ obey the quantitative curvature-correction rate bound $|(\lambda^{\mathrm{disc}}_{\mathrm{curved}}-\lambda^{\mathrm{disc}}_{\mathrm{flat}})-(\lambda^{\mathrm{cont}}_{\mathrm{curved}}-\lambda^{\mathrm{cont}}_{\mathrm{flat}})|\le C/N^2$; (iv) the same rate bound holds for coupling coefficient $2$.
background
Gap 4 concerns the curved Lichnerowicz operator on lattice tensor fields. The certified spectrum theorem in DiscreteLichnerowicz only treats axis modes of the componentwise flat lattice Laplacian, with continuum value introduced from the flat reduction $\Delta_L=-\Delta$. It carries no Riemann-curvature endomorphism, so it cannot fix a curved-background coupling.
This module builds two explicit zeroth-order curvature-coupled operator families (single and double coupling). Both reduce to $-\mathrm{discLap}_3$ for every field and resolution at zero curvature, yet they disagree on a concrete nonzero TT polarization whenever the scalar curvature proxy $\rho$ is nonzero. Their eigenvalue branches are the flat discrete/continuum eigenvalues plus $\mathrm{coupling}\cdot\rho$.
CurvatureCorrectionRateBound is the quantitative certificate: the curved-minus-flat correction on the lattice stays within $C/N^2$ of the continuum curved-minus-flat correction. Relative to the existing flat convergence theorem, full curved spectral convergence is equivalent to convergence of that omitted correction term.
proof idea
Pure term-mode packaging of four already-proved facts into a single conjunction.
First component: extensions_agree_on_entire_flat_specialization, which states that single and double curvature extensions coincide for curvature proxy $0$ on every resolution and every lattice tensor field.
Second component: extensions_distinct_at_nonzero_curvature applied to the given $\rho\neq 0$, yielding operator inequality at every $N$.
Third and fourth: curvedEigenvalueFamily_rateBound instantiated at couplings $1$ and $2$. Those lemmas discharge CurvatureCorrectionRateBound for the corresponding discrete and continuum curved eigenvalue families (flat eigenvalue plus coupling times $\rho$).
No further tactic work; the blocker is the conjunction itself.
why it matters
This is the final certified Gap 4 blocker. Downstream, gap4_curvature_coupling_blocker_certified in FullTheoryLedger re-exports it and keeps gap4_operator_recovery false until a genuine curvature endomorphism is derived. Gap4OperatorDecoyReceipt uses the same data for curvedSpectrumConverges_coupling_two and decoy_rateBound_both_couplings, showing both decoy couplings inhabit the generic consistency machinery.
In the Recognition gravity program the point is sharp: the flat spectrum theorem plus $C/N^2$ correction bounds underdetermine the curved Lichnerowicz coupling. Closing Gap 4 requires deriving the physical curvature endomorphism from curved discrete geometry and proving its correction matches the continuum Riemann coupling. The scalar $\rho$ here is only a minimal non-identifiability proxy, not that physical operator.
No direct T0–T8 or RCL content; the result is a gravity-side obstruction inside the SevenGaps ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.