FiberedPersistence.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Persistence in the actual congruence-fiber graph family

The arithmetic small-loop theorem, finite-component circle index and exact family restriction are combined here. Boundary walks remain explicit geometric arguments; they are not labeled as published inputs. The only published inputs in the resulting detector are the stated circle pairing and countable first-variable additivity.

abbrev OAI.CoarseAssembly.CircleFamily line 25
def OAI.CoarseAssembly.boundaryCircleFamily line 27
def OAI.CoarseAssembly.fiberedBoundaryLoops line 35
def OAI.CoarseAssembly.fiberedBoundaryStage line 43
theorem OAI.CoarseAssembly.fiberedBoundaryLoops_coarsen line 52
theorem OAI.CoarseAssembly.fiberedBoundaryStage_coarsen line 63
theorem OAI.CoarseAssembly.fiberedBoundaryStage_detected line 82
Source documentation
Every integer scale has a detector of the same boundary family, using the proved eventual small-loop theorem for the actual finite graphs.
```
theorem fiberedBoundaryStage_detected (input : PublishedCircleInput)
    (hadd : CountableAdditivityInput CircleFamily)
    (hboundary : ∀ j, 2 ≤ j → walkCharge fiberCharge (boundary j) = 1)
    (r : ℕ) (hr : 1 ≤ r) :
    letI := componentUnionMetric S chosenHolonomyUnit
…
```
Mentions: OAI.CoarseAssembly.PublishedCircleInput, OAI.CoarseAssembly.CircleFamily, OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.fiberCharge, OAI.CoarseAssembly.componentUnionMetric
def OAI.CoarseAssembly.fiberedBoundaryClass line 115
theorem OAI.CoarseAssembly.fiberedBoundaryClass_infinite_order line 125
Source documentation
The same global class has no nonzero integer annihilator. The boundary walks and their charge-one proofs are geometric arguments still to be instantiated; the small-loop and analytic restriction bridges are proved.
```
theorem fiberedBoundaryClass_infinite_order (input : PublishedCircleInput)
    (hadd : CountableAdditivityInput CircleFamily)
    (hboundary : ∀ j, 2 ≤ j → walkCharge fiberCharge (boundary j) = 1)
    (n : ℤ) (hn : n ≠ 0) :
    letI := componentUnionMetric S chosenHolonomyUnit
…
```
Mentions: OAI.CoarseAssembly.PublishedCircleInput, OAI.CoarseAssembly.CircleFamily, OAI.CoarseAssembly.walkCharge, OAI.CoarseAssembly.fiberCharge, OAI.CoarseAssembly.componentUnionMetric
theorem OAI.CoarseAssembly.fiberedBoundaryClass_rational_ne_zero line 144