RepresentationIntegerParameters.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Exact integer computation of the representation parameters

Distinct-sum counts determine the ordering and low-prime bit lengths. Logarithms remain analysis quantities and are not evaluated by the program.

def OAI.LowSpaceSubsetSum.mixerOrderFromCounts line 16
Source documentation
Sort by decreasing distinct-sum count, with the same index tie rule as the deficiency ordering in the analysis.
```
def mixerOrderFromCounts (counts : Fin 3 → ℕ) : Equiv.Perm (Fin 3) :=
…
```
def OAI.LowSpaceSubsetSum.rationalLowParameter line 20
Source documentation
The floor of the rational cutoff, with natural truncation at zero.
```
def rationalLowParameter (n half : ℕ) : ℕ :=
…
```
def OAI.LowSpaceSubsetSum.lowParameterFromCount line 23
def OAI.LowSpaceSubsetSum.extraParameterFromLow line 26
theorem OAI.LowSpaceSubsetSum.rationalLowParameter_eq line 29
theorem OAI.LowSpaceSubsetSum.floor_half_logb_count line 40
theorem OAI.LowSpaceSubsetSum.sort_eq_of_le_iff line 47
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawMixers_card_mixerSize line 63
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.mixerOrder_eq_integer line 67
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.floor_lowExponent_eq_integer line 82
Source documentation
The exact floor of each low exponent is computed by integer arithmetic and the bit length of the distinct-sum count.
```
theorem floor_lowExponent_eq_integer (z : Layout n) (i : Fin 3) :
    ⌊R.lowExponent z i⌋₊ = lowParameterFromCount n R.halfSize
      (distinctSumCount R.originalWeights (R.orderedMixers z i)) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.lowParameterFromCount, OAI.LowSpaceSubsetSum.distinctSumCount
theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeParameter_eq_integer line 97