RationalBinary.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.RationalHitting.StackLanguage.eval_copy9 line 8
def OAI.RationalHitting.StackLanguage.fractionReduce line 19
Source documentation
Euclid followed by two binary divisions, destructively producing the coprime numerator and positive denominator magnitudes.
```
def fractionReduce : Program (Fin 12) :=
…
```
Mentions: OAI.RationalHitting.StackLanguage.Program
lemma OAI.RationalHitting.StackLanguage.eval_fractionReduce line 25
def OAI.RationalHitting.StackLanguage.unaryLength line 120
Source documentation
Consume a word, emitting its unary length, independently of its bits.
```
def unaryLength (a b : K) : Program K := .loop a (.seq (.drop a) (.push b true))
```
Mentions: OAI.RationalHitting.StackLanguage.Program
lemma OAI.RationalHitting.StackLanguage.eval_unaryLength line 122
def OAI.RationalHitting.StackLanguage.encodedWord line 148
Source documentation
Canonical output's self-delimiting natural-number encoding, applied to an already canonical little-endian binary word.
```
def encodedWord (w : List Bool) : List Bool :=
…
```
def OAI.RationalHitting.StackLanguage.encodeWord line 151
lemma OAI.RationalHitting.StackLanguage.eval_encodeWord line 155
lemma OAI.RationalHitting.StackLanguage.digits_bool_bits line 176
lemma OAI.RationalHitting.RationalCanonical.divInt_num_abs line 187
lemma OAI.RationalHitting.RationalCanonical.divInt_den line 193

lemma OAI.RationalHitting.RationalCanonical.divInt_sign line 198

Source documentation

The sign used by the canonical binary rational encoder.

lemma divInt_sign (a b : ℤ) (hb : b≠0) :
    decide ((Rat.divInt a b).num<0) =
      if a=0 then false else (decide (a<0) ^^ decide (b<0)) := by
…

lemma OAI.RationalHitting.StackLanguage.encodedWord_bits line 223
lemma OAI.RationalHitting.StackLanguage.eval_encodeWord_rename line 226
lemma OAI.RationalHitting.StackLanguage.eval_fractionReduce_rename line 234
def OAI.RationalHitting.StackLanguage.fractionSign line 250
Source documentation
Registers 12 and 13 hold signed-magnitude signs; 15 stores the canonical result's sign and remains disjoint from the twelve arithmetic registers.
```
def fractionSign : Program (Fin 16) :=
…
```
Mentions: OAI.RationalHitting.StackLanguage.Program
lemma OAI.RationalHitting.StackLanguage.eval_fractionSign line 255
def OAI.RationalHitting.StackLanguage.reduceReg line 273
lemma OAI.RationalHitting.StackLanguage.reduceReg_inj line 274
def OAI.RationalHitting.StackLanguage.denominatorReg line 276
def OAI.RationalHitting.StackLanguage.numeratorReg line 277
lemma OAI.RationalHitting.StackLanguage.denominatorReg_inj line 278
lemma OAI.RationalHitting.StackLanguage.numeratorReg_inj line 279
def OAI.RationalHitting.StackLanguage.rationalEncode line 283
Source documentation
Full signed canonical rational output. No gcd, comparison or sign oracle occurs in this fixed finite binary-stack program.
```
def rationalEncode : Program (Fin 16) :=
…
```
Mentions: OAI.RationalHitting.StackLanguage.Program

theorem OAI.RationalHitting.StackLanguage.eval_rationalEncode line 296

Source documentation

Exact final canonical binary fraction, with a cubic bit-time stack implementation. This supplies the output-format obligation of the uniform list generator.

theorem eval_rationalEncode (s : Store (Fin 16)) (a b : ℤ) (hb : b≠0)
    (h0 : s 0=a.natAbs.bits) (h5 : s 5=b.natAbs.bits)
    (h12 : s 12=[decide (a<0)]) (h13 : s 13=[decide (b<0)]) (h15 : s 15=[])
    (hs : ∀ i : Fin 16, i.val<12 → i≠0 → i≠5 → s i=[])
    (B : ℕ) (ha : a.natAbs.bits.length≤B) (hd : b.natAbs.bits.length≤B) :
    ∃ t ≤ 3100*(B+1)^3, Eval rationalEncode s
      (update (update (update s 0 []) 5 []) 14 (encodeRat (Rat.divInt a b)++s 14)) t := by
…

Mentions: OAI.RationalHitting.StackLanguage.Store, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.rationalEncode, OAI.RationalHitting.encodeRat