structure definition def or abbrev

`ClayBridge`

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

formal statement (Lean)

 222structure ClayBridge where
 223  /-- Map RS complexity to Clay's Turing model -/
 224  to_clay : RecognitionComplete → (ℕ → ℕ)
 225  /-- Clay sees only Tc, missing Tr -/
 226  projection : ∀ RC, to_clay RC = RC.Tc
 227  /-- This makes P vs NP ill-posed in Clay's framework -/
 228  ill_posed : ∀ RC, RC.Tc ≠ RC.Tr →
 229    -- Clay cannot distinguish the full complexity
 230    to_clay RC = RC.Tc
 231
 232/-- The bridge theorem: connecting to Clay's formulation -/

used by (3)

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

clay_bridge_theorem in IndisputableMonolith.Complexity.ComputationBridge decl_use
CompleteModel in IndisputableMonolith.Complexity.ComputationBridge decl_use
main_resolution in IndisputableMonolith.Complexity.ComputationBridge decl_use

depends on (4)

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
model in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
RecognitionComplete in IndisputableMonolith.Complexity.ComputationBridge decl_use
Map in IndisputableMonolith.Measurement decl_use