Circuit.lean`

59 declarations, 0 contain sorry, 0 declared as axioms

A specialized evaluator supporting the simulation's factored and ordinary gates. Can treat the latter as special factored gates by allowing the selector/test function at a coordinate z to depend on z, including the extra coordinate d of augmented words.

structure OAI.Fifths.Circuit line 14
abbrev OAI.Fifths.Slot line 30
def OAI.Fifths.Slot.H line 32
def OAI.Fifths.Slot.A line 33
theorem OAI.Fifths.Slot.h_ne line 34
theorem OAI.Fifths.Slot.a_ne line 35
theorem OAI.Fifths.Slot.sep line 36
abbrev OAI.Fifths.Modulus.Pool line 42
def OAI.Fifths.Modulus.plus line 44
def OAI.Fifths.Modulus.multiple line 46
def OAI.Fifths.Modulus.spike line 47
theorem OAI.Fifths.Modulus.plus_at line 49
theorem OAI.Fifths.Modulus.plus_other line 52
theorem OAI.Fifths.Modulus.plus_zero line 54
theorem OAI.Fifths.Modulus.plus_twice line 59
theorem OAI.Fifths.Modulus.plus_comm line 64
theorem OAI.Fifths.Modulus.plus_cancel line 69
theorem OAI.Fifths.Modulus.plus_shift line 73
abbrev OAI.Fifths.Circuit.Node line 83
def OAI.Fifths.Circuit.outerDegree line 84
def OAI.Fifths.Circuit.P line 85
abbrev OAI.Fifths.Circuit.F line 86
abbrev OAI.Fifths.Circuit.Pool line 87
abbrev OAI.Fifths.Circuit.Vec line 88
def OAI.Fifths.Circuit.value line 91
Source documentation
Last raw bit index is width-1; extra coordinate index width.
```
def value (v : C.Node) : C.Vec := C.P.aug C.width (C.semantic v)
```
def OAI.Fifths.Circuit.YCount line 92
def OAI.Fifths.Circuit.G line 94
def OAI.Fifths.Circuit.test line 95
def OAI.Fifths.Circuit.EG line 96
def OAI.Fifths.Circuit.ET line 97
structure OAI.Fifths.Circuit.Good line 100
Source documentation
Circuits are specification-only objects prior to uniformity hypotheses.
```
structure Good : Prop where
…
```
structure OAI.Fifths.Circuit.Request line 110
Source documentation
A call changes only the requested slot, by the indicated multiple.
```
structure Request where
…
```
def OAI.Fifths.Circuit.Request.otherH line 117
def OAI.Fifths.Circuit.Request.otherA line 119
def OAI.Fifths.Circuit.Request.undo line 121
def OAI.Fifths.Circuit.Request.result line 122
inductive OAI.Fifths.Circuit.Pc line 126
instance OAI.Fifths.Circuit.(instance at line 130) line 130
def OAI.Fifths.Circuit.Pc.code line 134
structure OAI.Fifths.Circuit.Frame line 143
def OAI.Fifths.Circuit.clip line 156
Source comment
Natural stages saturate if applied in arbitrary intermediate phases at an out-of-range endpoint. On real path proofs will show bounds.
```
def clip (n : ℕ) (k : ℕ) : Fin (n+1) :=
…
```
theorem OAI.Fifths.Circuit.clip_ok line 158
def OAI.Fifths.Circuit.form line 161
def OAI.Fifths.Circuit.fEntry line 164
def OAI.Fifths.Circuit.fOuter line 165
def OAI.Fifths.Circuit.fCoord line 166
def OAI.Fifths.Circuit.fGuess line 167
def OAI.Fifths.Circuit.fFactor line 168
def OAI.Fifths.Circuit.fSample line 170
def OAI.Fifths.Circuit.fCheck line 172
def OAI.Fifths.Circuit.amount line 175
def OAI.Fifths.Circuit.atPc line 183
Source documentation
Each call pushes one measured frame. No intermediate vector is scoped as scratch across pushes. After checkA release the lookup work area; only one accumulated scalar is needed (plus u etc). We compute w' (small) before the reverse push.
```
def atPc (R : C.Pool) (f : C.Frame) (p : Pc) :
    C.Pool × FlowMove C.Frame :=
…
```
Mentions: OAI.Fifths.Circuit.Pc, OAI.Fifths.FlowMove
def OAI.Fifths.Circuit.packPool line 225
def OAI.Fifths.Circuit.packX line 228
def OAI.Fifths.Circuit.packFrame line 230
def OAI.Fifths.Circuit.flow line 234
def OAI.Fifths.Circuit.price line 238
Source documentation
Uniform fee estimates intentionally very loose.
```
def price (g : ℕ) :=
…
```
structure OAI.Fifths.Circuit.Meter line 241
theorem OAI.Fifths.Circuit.price_bounds line 247