NullBoundary.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The boundary form of the relative null-layer obstruction

The old universal-frame argument used a boundary generator in degree zero and therefore applied only above zero. In §5 of paper 082-03 the relative frame can instead be joined to the isolated layer through a boundary color at any lower integer degree. This is the saturation contradiction at that degree. Establishing the occupied boundary for a relative family is a separate support argument, not a published hypothesis.

theorem OAI.HarmonicArtin.ParabolicIntersections.null_boundary_contradiction line 27
Source documentation
Saturation kills every exterior boundary count below the isolated layer. Thus a boundary count preserved throughout the permitted orbit prevents the isolated null-layer configuration, at any integer height.
```
theorem null_boundary_contradiction (D : IsolatedIterationData M)
    (k : ℤ) (hk : k < D.q) (v : S ⊕ Unit)
    (hv : v ∉ Sum.inl '' D.I)
    (hinc : ∃ u ∈ Sum.inl '' D.I,
      fusionFoldedCartan (fusionLabelSize M) (coxeterFusionEdge M) v u < 0)
    (hoccupied : ∀ z, D.valid z →
      0 < fusionOrbitMultiplicity (fusionLabelSize M) (coxeterFusionEdge M)
        (coxeterFusionEdge_symm M) (coxeterFusionEdge_diag M)
        (fun e => le_trans (by norm_num) (fusionLabelSize_ge_four M e)) z D.s k v)
    (z : List ((S ⊕ Unit) × Bool)) (hz : D.valid z) (hc : D.capped z) : False := by
…
```
Mentions: OAI.HarmonicArtin.IsolatedIterationData, OAI.HarmonicArtin.fusionFoldedCartan, OAI.HarmonicArtin.fusionLabelSize, OAI.HarmonicArtin.coxeterFusionEdge, OAI.HarmonicArtin.fusionOrbitMultiplicity, OAI.HarmonicArtin.coxeterFusionEdge_symm, OAI.HarmonicArtin.coxeterFusionEdge_diag, OAI.HarmonicArtin.fusionLabelSize_ge_four