def definition def or abbrev

`rsbridge_status`

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

formal statement (Lean)

 236def rsbridge_status : String :=

proof body

Definition body.

 237  "✓ RSConfigSpace: Ledger states as configuration space\n" ++
 238  "✓ RSLocalityFromRHat: R̂ operator defines locality (RG1)\n" ++
 239  "✓ RSMeasurement: Measurement maps as recognizers (RG2)\n" ++
 240  "✓ EightTickFiniteResolution: 8-tick gives finite resolution\n" ++
 241  "✓ eight_tick_implies_RG4: RS satisfies RG4\n" ++
 242  "✓ RS_instantiates_RG: master RG4 bridge statement\n" ++
 243  "✓ physical_space_is_quotient: Space as recognition quotient\n" ++
 244  "✓ JCostComparative: J-cost as comparative recognizer\n" ++
 245  "✓ toRecognitionDistance: J-cost gives metric structure\n" ++
 246  "\n" ++
 247  "RS BRIDGE COMPLETE"
 248
 249#eval rsbridge_status
 250
 251end RecogGeom
 252end IndisputableMonolith

depends on (20)

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
Measurement in IndisputableMonolith.Data.Import decl_use
eval in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use
EightTickFiniteResolution in IndisputableMonolith.RecogGeom.RSBridge decl_use
eight_tick_implies_RG4 in IndisputableMonolith.RecogGeom.RSBridge decl_use
JCostComparative in IndisputableMonolith.RecogGeom.RSBridge decl_use
physical_space_is_quotient in IndisputableMonolith.RecogGeom.RSBridge decl_use
RSConfigSpace in IndisputableMonolith.RecogGeom.RSBridge decl_use
RS_instantiates_RG in IndisputableMonolith.RecogGeom.RSBridge decl_use
RSLocalityFromRHat in IndisputableMonolith.RecogGeom.RSBridge decl_use
RSMeasurement in IndisputableMonolith.RecogGeom.RSBridge decl_use
toRecognitionDistance in IndisputableMonolith.RecogGeom.RSBridge decl_use
eval in IndisputableMonolith.Relativity.Fields.Scalar decl_use