SidePins.lean`

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.SidePins.root line 13
Source documentation
The optional first-stage root split by prescribed side.
```
def root (r : Option V) (b : Bool) : Option {v : V // side v=b} :=
…
```
lemma OAI.TorsionFreeZeroDivisors.SidePins.root_none line 17
lemma OAI.TorsionFreeZeroDivisors.SidePins.root_some line 19
lemma OAI.TorsionFreeZeroDivisors.SidePins.root_save line 23
lemma OAI.TorsionFreeZeroDivisors.SidePins.free_total line 30
lemma OAI.TorsionFreeZeroDivisors.SidePins.respects line 42
def OAI.TorsionFreeZeroDivisors.StageRoot.cyclic line 70
Source documentation
The possible interval is designated once, not independently at each stage.
```
def cyclic (root : Option P) (p : P) : Bool := decide (root≠some p)
…
```
lemma OAI.TorsionFreeZeroDivisors.StageRoot.intervals_card line 73
def OAI.TorsionFreeZeroDivisors.StageRoot.vertex line 80
Source documentation
Only the first stage fixes the marked initial vertex.
```
def vertex (root : Option P) (j : ℕ) : Option (ActiveV (S) mult j) :=
…
```
lemma OAI.TorsionFreeZeroDivisors.StageRoot.vertex_isSome line 87
def OAI.TorsionFreeZeroDivisors.StageRoot.power line 96
Source documentation
The root split over the two prescribed sides has exactly the source saving.
```
def power (side : ∀ j, ActiveV (S) mult j → Bool) (root : Option P)
    {TA TB : Type} (a : TA) (b : TB) (j : ℕ) : ℤ :=
…
```
lemma OAI.TorsionFreeZeroDivisors.StageRoot.power_eq line 102
theorem OAI.TorsionFreeZeroDivisors.StageRoot.power_nonpos line 114
lemma OAI.TorsionFreeZeroDivisors.RootPins.pin_some_iff line 131
lemma OAI.TorsionFreeZeroDivisors.SidePins.root_eq_some line 140
def OAI.TorsionFreeZeroDivisors.StageRoot.source line 166
Source documentation
The actual marked initial vertex of the designated interval, if any.
```
def source (r : Option P) : Option V := r.map fun p => (S).origin ((paths p).head (hp p))
```
lemma OAI.TorsionFreeZeroDivisors.StageRoot.vertex_source line 168
lemma OAI.TorsionFreeZeroDivisors.StageRoot.pin_compatible line 181
abbrev OAI.TorsionFreeZeroDivisors.ActualStagePair.pinA line 217
abbrev OAI.TorsionFreeZeroDivisors.ActualStagePair.pinB line 218
abbrev OAI.TorsionFreeZeroDivisors.ActualStagePair.A line 220
abbrev OAI.TorsionFreeZeroDivisors.ActualStagePair.B line 226
lemma OAI.TorsionFreeZeroDivisors.ActualStagePair.power_eq line 234
lemma OAI.TorsionFreeZeroDivisors.ActualStagePair.edges_eq line 245
lemma OAI.TorsionFreeZeroDivisors.ActualStagePair.edges_bound line 258
def OAI.TorsionFreeZeroDivisors.ActualStagePair.count line 272
theorem OAI.TorsionFreeZeroDivisors.ActualStagePair.count_pos line 279
Source documentation
Restricting actual embeddings on the two prescribed sides witnesses the joint stage count, with a SINGLE global label projection.
```
theorem count_pos (s : ℝ) (cmp : Comparisons (E:=E) (traversalLength len m))
…
```
theorem OAI.TorsionFreeZeroDivisors.ActualStagePair.mean_bound line 299
Source documentation
The actual rooted, mixed-side stage first moment, with its exact signed vertex exponent and the source's common denominator loss.
```
theorem mean_bound (s : ℝ) (cmp : Comparisons (E:=E) (traversalLength len m))
…
```
lemma OAI.TorsionFreeZeroDivisors.ActualPatternEvent.mem_profiles_iff line 347
abbrev OAI.TorsionFreeZeroDivisors.ActualPatternEvent.Match line 365
def OAI.TorsionFreeZeroDivisors.ActualPatternEvent.samples line 369
lemma OAI.TorsionFreeZeroDivisors.ActualPatternEvent.samples_eq line 377
abbrev OAI.TorsionFreeZeroDivisors.ActualPatternEvent.sourcePinA line 388
abbrev OAI.TorsionFreeZeroDivisors.ActualPatternEvent.sourcePinB line 390
def OAI.TorsionFreeZeroDivisors.ActualPatternEvent.Occurs line 396
Source documentation
Literal realization of an enlarged fixed pattern and its bin profile. The prescribed-side embeddings are into the actual two independent matchings. The comparisons refer to normalized traversals of the same suppressed graph.
```
def Occurs (s : ℝ) (cmp : Comparisons (E:=E) (traversalLength len m))
…
```
theorem OAI.TorsionFreeZeroDivisors.ActualPatternEvent.count_pos line 412
Source documentation
Existence of the actual pattern witnesses every stage count. This does not posit simultaneous independence of the chain-multiplicity stages.
```
theorem count_pos (s : ℝ) (hs : 0<s) (cmp : Comparisons (E:=E) (traversalLength len m))
…
```
theorem OAI.TorsionFreeZeroDivisors.ActualPatternEvent.bin_bounds line 430
Source documentation
A realizable bin profile automatically has the universal lower and upper weight bounds; those numerical bounds are not extra assumptions on an event.
```
theorem bin_bounds (s : ℝ) (hs : 0<s) (cmp : Comparisons (E:=E) (traversalLength len m))
…
```
def OAI.TorsionFreeZeroDivisors.ActualPatternEvent.Unbinned line 447
Source documentation
The unbinned event quantifies no artificial stage data: the bin witness is forced by the literal label words.
```
def Unbinned (s : ℝ) (cmp : Comparisons (E:=E) (traversalLength len m))
…
```
lemma OAI.TorsionFreeZeroDivisors.ActualPatternEvent.occurs_profile line 452
lemma OAI.TorsionFreeZeroDivisors.ActualPatternEvent.unbinned_iff_profile line 470
theorem OAI.TorsionFreeZeroDivisors.ActualPatternEvent.probability_bound line 486
Source documentation
One genuinely realized fixed-bin pattern is exponentially unlikely. All numerical stage bounds are derived from its two literal matching means; no independence between multiplicity stages is asserted.
```
theorem probability_bound (s : ℝ) (hs : 0<s)
    (cmp : Comparisons (E:=E) (traversalLength len m)) (d : Underlying s len → ℤ)
…
```
theorem OAI.TorsionFreeZeroDivisors.ActualPatternEvent.unbinned_probability_bound line 550
Source documentation
Union over all canonical weight bins of an actual pattern.
```
theorem unbinned_probability_bound (s : ℝ) (hs : 0<s) (hslarge : 3003≤ s)
    (cmp : Comparisons (E:=E) (traversalLength len m))
…
```