OAI/Analysis/CircleDomains/Rigidity/RawLevelNullTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The raw barrier has Haar-null free trace on the nondegenerate components of an actual compact quotient level union. The topology comes from finite physical length. Arc existence uses only the connected-open specialization of Lorimer (1981), recorded in ArcNullImage.

  1. theorem OAI.CircleDomainRigidity.raw_barrier_null_component_traces line 18