def definition def or abbrev

`TransferOperator`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  25noncomputable def TransferOperator (K : Kernel) : (LatticeMeasure → ℂ) →L[ℂ] (LatticeMeasure → ℂ) :=

proof body

Definition body.

  26  K.T
  27
  28/-- OS reflection positivity surrogate: existence of a transfer kernel with a
  29    uniform overlap lower bound β ∈ (0,1]. This encodes a spectral positivity
  30    guard compatible with Dobrushin-type contraction. -/

depends on (19)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
compatible in IndisputableMonolith.Complexity.SAT.Backprop decl_use
K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
T in IndisputableMonolith.Foundation.Breath1024 decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use
Kernel in IndisputableMonolith.ILG.PressureForm decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
uniform in IndisputableMonolith.Information.ShannonEntropy decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
overlap in IndisputableMonolith.YM.Dobrushin decl_use
Kernel in IndisputableMonolith.YM.OS decl_use
LatticeMeasure in IndisputableMonolith.YM.OS decl_use