OAI/Combinatorics/YoungDiagram/LiteralCapacity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArithmeticTensorSquares.Capacity.literalAttachmentCapacity line 12

   Source documentation

   Integer Euclidean division by positive2 is the literal integer floor. Unlike Nat subtraction, this expression retains negative h-d before clamping.

   def literalAttachmentCapacity (height : Nat → Nat) (d q : Nat) : Int :=
   …

2. def OAI.ArithmeticTensorSquares.Capacity.LiteralBandTest line 15
3. lemma OAI.ArithmeticTensorSquares.Capacity.attachment_term_eq line 20
4. lemma OAI.ArithmeticTensorSquares.Capacity.literalAttachmentCapacity_eq line 24
5. lemma OAI.ArithmeticTensorSquares.Capacity.bandTest_literal_iff line 36
6. lemma OAI.ArithmeticTensorSquares.Capacity.twice_triangular line 40
7. theorem OAI.ArithmeticTensorSquares.Capacity.capacity_large line 50

   Source documentation

   The literal band criterion for the parity-compatible triangular index and remainder, with both first-four prefix bounds.

   theorem capacity_large (n : Nat) (μ : YoungDiagram) (hcard : μ.card = n)
       (hM : 22 ≤ UniversalTensorSquares.largestIndex n)
       (hr : 0 < UniversalTensorSquares.remainderPairs n)
       (hcols : 2*UniversalTensorSquares.largestIndex n-1 ≤ colPrefix μ 4)
       (hrows : 2*UniversalTensorSquares.largestIndex n-1 ≤ rowPrefix μ 4) :
       LiteralBandTest μ.colLen μ.rowLen
         (UniversalTensorSquares.largestIndex n) (UniversalTensorSquares.remainderPairs n) ∨
       LiteralBandTest μ.rowLen μ.colLen
         (UniversalTensorSquares.largestIndex n) (UniversalTensorSquares.remainderPairs n) := by
   …

   Mentions: OAI.UniversalTensorSquares.largestIndex, OAI.UniversalTensorSquares.remainderPairs, OAI.ArithmeticTensorSquares.Capacity.colPrefix, OAI.ArithmeticTensorSquares.Capacity.rowPrefix, OAI.ArithmeticTensorSquares.Capacity.LiteralBandTest