Machine emission of terminated-unary natural codes — proof internals

This module instantiates the generic canonical binary loop with one-bit output emission. The proof tracks concrete counter and output tapes at every loop index, then composes scratch clearing and the terminating zero-bit emitter.

def Complexity.CircuitCode.Machine.natCodeWorkAt {n : ℕ} (work : Fin n → Tape) (counterIdx : Fin n) (value : ℕ) : Fin n → Tape

Replace the scratch counter by the canonical binary tape for value.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.Machine.natCodeOutputAt (out : Tape) : ℕ → Tape

Concrete output tape after appending count one-bits.

Equations

• Complexity.CircuitCode.Machine.natCodeOutputAt out 0 = out
• Complexity.CircuitCode.Machine.natCodeOutputAt out count.succ = (Complexity.CircuitCode.Machine.natCodeOutputAt out count).writeAndMove Complexity.Γ.one Complexity.Dir3.right

theorem Complexity.CircuitCode.Machine.emitNatCodeLoopTM_reachesIn_frame_internal {n : ℕ} (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (ys : List Bool) (hinp : TM.Parked inp₀) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hlimit : (work₀ limitIdx).HasBinaryNat value) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → TM.Parked (work₀ i)) (hout : TM.OutAcc ys out₀) : (emitNatCodeLoopTM counterIdx limitIdx).reachesIn (emitNatCodeLoopTime value) { state := (emitNatCodeLoopTM counterIdx limitIdx).qstart, input := inp₀, work := work₀, output := out₀ } { state := (emitNatCodeLoopTM counterIdx limitIdx).qhalt, input := inp₀, work := natCodeWorkAt work₀ counterIdx value, output := natCodeOutputAt out₀ value }

The binary loop emits exactly the unary body and stops with the scratch counter equal to the preserved limit.

theorem Complexity.CircuitCode.Machine.emitNatCodeLoopTM_reachesIn_endpoint_internal {n : ℕ} (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (ys : List Bool) (hinp : TM.Parked inp₀) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hlimit : (work₀ limitIdx).HasBinaryNat value) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → TM.Parked (work₀ i)) (hout : TM.OutAcc ys out₀) : ∃ (c' : Cfg n (emitNatCodeLoopTM counterIdx limitIdx).Q), (emitNatCodeLoopTM counterIdx limitIdx).reachesIn (emitNatCodeLoopTime value) { state := (emitNatCodeLoopTM counterIdx limitIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (emitNatCodeLoopTM counterIdx limitIdx).halted c' ∧ c'.input = inp₀ ∧ c'.work = Function.update work₀ counterIdx ((Tape.init (List.map Γ.ofBool value.bits)).move Dir3.right) ∧ TM.OutAcc (ys ++ List.replicate value true) c'.output

Public-shape exact endpoint for the unary-body loop.

theorem Complexity.CircuitCode.Machine.emitNatCodeLoopTM_hoareTime_internal {n : ℕ} (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp : TM.Parked inp₀) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hlimit : (work₀ limitIdx).HasBinaryNat value) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → TM.Parked (work₀ i)) : (emitNatCodeLoopTM counterIdx limitIdx).HoareTime (TM.EmitPred inp₀ work₀ ys) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = natCodeWorkAt work₀ counterIdx value ∧ TM.OutAcc (ys ++ List.replicate value true) out) (emitNatCodeLoopTime value)

Time-bounded endpoint contract for the unary body loop.

theorem Complexity.CircuitCode.Machine.emitNatCodeLoopTM_hoareTimeSpace_internal {n : ℕ} (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp : TM.Parked inp₀) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hlimit : (work₀ limitIdx).HasBinaryNat value) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → TM.Parked (work₀ i)) (hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace) (hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1) : (emitNatCodeLoopTM counterIdx limitIdx).HoareTimeSpace (TM.EmitPred inp₀ work₀ ys) (TM.EmitPred inp₀ (natCodeWorkAt work₀ counterIdx value) (ys ++ List.replicate value true)) (emitNatCodeLoopTime value) inputLength (initialSpace + 2 * value.size + 4)

Time-and-all-prefix-space contract for the unary-body loop.

theorem Complexity.CircuitCode.Machine.emitNatCodeTM_hoareTime_internal {n : ℕ} (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp : TM.Parked inp₀) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hlimit : (work₀ limitIdx).HasBinaryNat value) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → TM.Parked (work₀ i)) : (emitNatCodeTM counterIdx limitIdx).HoareTime (TM.EmitPred inp₀ work₀ ys) (TM.EmitPred inp₀ work₀ (ys ++ NatCode.encode value)) (emitNatCodeTime value)

End-to-end terminated-unary emission restores every input/work tape and appends exactly NatCode.encode value within the advertised time bound.

theorem Complexity.CircuitCode.Machine.emitNatCodeTM_hoareTimeSpace_internal {n : ℕ} (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp : TM.Parked inp₀) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hlimit : (work₀ limitIdx).HasBinaryNat value) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → TM.Parked (work₀ i)) (hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace) (hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1) : (emitNatCodeTM counterIdx limitIdx).HoareTimeSpace (TM.EmitPred inp₀ work₀ ys) (TM.EmitPred inp₀ work₀ (ys ++ NatCode.encode value)) (emitNatCodeTime value) inputLength (emitNatCodeSpace initialSpace value)

End-to-end time-and-all-prefix-space contract for natural-code emission.

theorem Complexity.CircuitCode.Machine.emitNatCodeTM_isTransducer_internal {n : ℕ} (counterIdx limitIdx : Fin n) : (emitNatCodeTM counterIdx limitIdx).IsTransducer

The natural-code emitter obeys the one-way-output transducer discipline.