def definition def or abbrev

`locality_status`

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

formal statement (Lean)

 130def locality_status : String :=

proof body

Definition body.

 131  "✓ LocalConfigSpace defined (RG1)\n" ++
 132  "✓ Neighborhood axioms: mem_of_mem_N, intersection_closed, refinement\n" ++
 133  "✓ Basic lemmas: has_neighborhood, self_mem_neighborhood, common_refinement\n" ++
 134  "✓ Neighborhood filter construction\n" ++
 135  "✓ Discrete and trivial examples\n" ++
 136  "\n" ++
 137  "LOCALITY STRUCTURE (RG1) COMPLETE"
 138
 139#eval locality_status
 140
 141end RecogGeom
 142end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.

Neighborhood in IndisputableMonolith.Complexity.CellularAutomata decl_use
eval in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
refinement in IndisputableMonolith.Papers.DraftV1 decl_use
eval in IndisputableMonolith.Relativity.Fields.Scalar decl_use