Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.Gap4OperatorDecoyReceipt

show as:
view Lean formalization →

Certifies Gap 4's decoy path: every free scalar curvature coupling still produces a convergent curved eigenvalue family. That Tendsto is the known false path; typed residual countermodels show the spectrum is not ledger-close. Campaign auditors cite the receipt and terminal guard before the axiom-audit module.

claimFor each free scalar curvature coupling, the curved eigenvalue family converges ($\mathrm{Tendsto}$). This convergence is a decoy: typed residual countermodels show the spectrum is not ledger-close. The module records Gap-4 decoy-blocker certification and a terminal ledger guard.

background

Lane 4 of the Seven-Gaps QG campaign is operator convergence: connect a discrete lattice perturbation spectrum to the continuum Lichnerowicz operator. DiscreteLichnerowicz does this only on the flat 3-torus, for 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.

CurvedOperatorUnderdetermination states the blocker: that certified flat spectrum cannot determine a curved-background coupling. The natural false path is to pick free scalar couplings, build curved eigenvalue families, and prove continuum convergence anyway.

This module is the machine-checked receipt for that decoy. Campaign and full-theory ledgers record scoped increments only; they do not flip full-strength QGScopeAudit closures.

proof idea

Not a single theorem: a receipt bundle. For representative free couplings it builds curved spectrum families and proves convergence (Tendsto) of the eigenvalue data. Parallel lemmas inhabit those families by explicit countermodels. Typed-residual statements then show the countermodel spectra fail ledger-closeness (spectrum not ledger-close), including a closed form of that residual. Rate bounds cover both couplings. The decoy Gap-4 blocker is certified, and a terminal ledger guard plus status object package the outcome for the campaign ledger.

why it matters in Recognition Science

Closes the bookkeeping on Gap 4's known false path so the campaign cannot mistake curved Tendsto for operator closure. Upstream, flat discrete Lichnerowicz plus curved underdetermination already limit the certified spectrum; this module proves that free-coupling convergence still does not yield a ledger-close curved operator. Downstream it is imported by Gap4OperatorDecoyReceiptAudit, whose axiom audit requires headline theorems to print inside [propext, Classical.choice, Quot.sound]. Feeds the Seven-Gaps campaign ledger style (proved increment vs open full physical closure) without flipping full-theory pillar flags.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (14)