MultibarIndex.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.Multibar.increment line 8

Source documentation

Add one D slot in block j. Every nonzero block differential starts at such a tuple.

def increment : (r : ℕ) → Blocks r → Fin (r+1) → Blocks r
  | 0, i, _ => Nat.succ i
  | r+1, (i, tail), j =>
      Fin.cases (i+1, tail) (fun j => (i, increment r tail j)) j

/-- Number of D entries strictly before block j, the ordinary totalization offset. -/

Mentions: OAI.DerivedBar.Multibar.Blocks

def OAI.DerivedBar.Multibar.blockOffset line 14

Source documentation

Number of D entries strictly before block j, the ordinary totalization offset.

def blockOffset : (r : ℕ) → Blocks r → Fin (r+1) → ℕ
  | 0, _, _ => 0
  | r+1, (i, tail), j => Fin.cases 0 (fun j => i + blockOffset r tail j) j

/-- The degree drops by one under a nonzero face in any block. -/

Mentions: OAI.DerivedBar.Multibar.Blocks

theorem OAI.DerivedBar.Multibar.total_increment line 19
Source documentation
The degree drops by one under a nonzero face in any block.
```
theorem total_increment (r : ℕ) (b : Blocks r) (j : Fin (r+1)) :
    total r (increment r b j) = total r b + 1 := by
…
```
Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.total, OAI.DerivedBar.Multibar.increment
theorem OAI.DerivedBar.Multibar.exponent_increment line 33
Source documentation
The exponent changes by r-j when a face removes a D slot in block j.
```
theorem exponent_increment (r : ℕ) (b : Blocks r) (j : Fin (r+1)) :
    exponent r (increment r b j) = exponent r b + (r-j.val) := by
…
```
Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.exponent, OAI.DerivedBar.Multibar.increment
theorem OAI.DerivedBar.Multibar.face_sign line 52
Source documentation
Equality of the actual scalar coefficients for each signed block face. The left side applies the rescaling followed by the shifted multibar sign; the right side applies the absolute bar sign followed by the target rescaling. ell is the local bar-face number, and the offset blockOffset counts earlier D slots.
```
theorem face_sign {k : Type*} [Field k] (r : ℕ) (b : Blocks r)
    (j : Fin (r+1)) (ell : ℕ) :
    (-1 : k)^(exponent r (increment r b j)) *
        (-1 : k)^(r + blockOffset r b j + ell) =
      (-1 : k)^(j.val + blockOffset r b j + ell) * (-1 : k)^(exponent r b) := by
…
```
Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.exponent, OAI.DerivedBar.Multibar.increment, OAI.DerivedBar.Multibar.blockOffset
def OAI.DerivedBar.Multibar.leadingBase line 65
Source documentation
Raise the first block length.
```
def leadingBase : (r : ℕ) → Blocks r → Blocks r
  | 0, i => Nat.succ i
  | _+1, (i, tail) => (i+1, tail)
```
Mentions: OAI.DerivedBar.Multibar.Blocks
theorem OAI.DerivedBar.Multibar.pattern_leadingBase line 69

def OAI.DerivedBar.Multibar.parse line 77

Source documentation

Parse any word into its unique consecutive D blocks.

def parse : (p : List Bool) → Blocks (count p)
  | [] => (0 : ℕ)
  | false :: p => leadingBase (count p) (parse p)
  | true :: p => (0, parse p)

/-- Every D/X word has a block-length description, including zero-length blocks. -/

Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.count, OAI.DerivedBar.Multibar.leadingBase

theorem OAI.DerivedBar.Multibar.pattern_parse line 83
Source documentation
Every D/X word has a block-length description, including zero-length blocks.
```
@[simp] theorem pattern_parse (p : List Bool) : pattern (count p) (parse p) = p := by
…
```
Mentions: OAI.DerivedBar.Multibar.pattern, OAI.DerivedBar.Multibar.count, OAI.DerivedBar.Multibar.parse
theorem OAI.DerivedBar.Multibar.finite_bounded line 90
Source documentation
Block indices of bounded total degree form a finite type.
```
theorem finite_bounded (r m : ℕ) : Finite {b : Blocks r // total r b ≤ m} := by
…
```
Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.total
theorem OAI.DerivedBar.Multibar.finite_degree line 109
Source documentation
The fixed-r multibar uses finitely many block tensors in every total degree.
```
theorem finite_degree (r n : ℕ) : Finite {b : Blocks r // r + total r b = n} := by
…
```
Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.total