structure definition def or abbrev

`MatrixBridge`

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

formal statement (Lean)

  19structure MatrixBridge (ι : Type) [Fintype ι] [DecidableEq ι]
  20  (K : TransferKernel ι) (V : MatrixView ι) where
  21  intertwine : K.T = CLM.ofLM (Matrix.toLin' V.A)
  22

used by (6)

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

MatrixBridge in IndisputableMonolith.Relativity.Geometry.MatrixBridge decl_use
MatrixBridgeAccepts in IndisputableMonolith.Relativity.Geometry.MatrixBridge decl_use
matrixBridge_accepts_identity in IndisputableMonolith.Relativity.Geometry.MatrixBridge decl_use
buildKernelFromMatrix in IndisputableMonolith.YM.Kernel decl_use
kernel3x3_with_bridge in IndisputableMonolith.YM.Kernel decl_use
KernelHasMatrixView in IndisputableMonolith.YM.Kernel decl_use

depends on (14)

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
V in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
T in IndisputableMonolith.Foundation.Breath1024 decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
V in IndisputableMonolith.Foundation.SpectralEmergence decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
MatrixBridge in IndisputableMonolith.Relativity.Geometry.MatrixBridge decl_use
V in IndisputableMonolith.RRF.Core.Glossary decl_use
CLM in IndisputableMonolith.YM.Kernel decl_use
MatrixView in IndisputableMonolith.YM.Kernel decl_use
TransferKernel in IndisputableMonolith.YM.Kernel decl_use