LargeCapacity.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ArithmeticTensorSquares.Capacity.attachmentCapacity line 11
Source documentation
Nat truncated subtraction/division equals max(0,floor((h-d)/2)) for the manuscript's nonnegative integral heights.
```
def attachmentCapacity (height : Nat → Nat) (d q : Nat) : Nat :=
…
```
def OAI.ArithmeticTensorSquares.Capacity.BandTest line 16
Source documentation
Exactly the three numeric inequalities of prop:band-test, in one orientation. K=2M-1; height=column lengths and width=row lengths.
```
def BandTest (height width : Nat → Nat) (M r : Nat) : Prop :=
…
```
lemma OAI.ArithmeticTensorSquares.Capacity.height_floor_bound line 21
lemma OAI.ArithmeticTensorSquares.Capacity.prefix_eight_bound line 23
theorem OAI.ArithmeticTensorSquares.Capacity.capacity_large_numeric line 51
Source documentation
Complete numeric large-parameter result. The doubled size identity and 2r≤3M+4 are the exact consequences of the manuscript's admissible parameters. No support/occurrence hypothesis is present or concluded.
```
theorem capacity_large_numeric (μ : YoungDiagram) (M r : Nat)
    (hM : 22 ≤ M) (hr : 0 < r)
    (hsize : 2*μ.card = M*(M+1)+4*r)
    (hrange : 2*r ≤ 3*M+4)
    (hcols : 2*M-1 ≤ colPrefix μ 4)
    (hrows : 2*M-1 ≤ rowPrefix μ 4) :
    BandTest μ.colLen μ.rowLen M r ∨ BandTest μ.rowLen μ.colLen M r := by
…
```
Mentions: OAI.ArithmeticTensorSquares.Capacity.colPrefix, OAI.ArithmeticTensorSquares.Capacity.rowPrefix, OAI.ArithmeticTensorSquares.Capacity.BandTest