OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/TM2Composition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time composition uses concrete finite TM2 compiler. It lifts the heterogeneous machine programs and performs a two-pass stack transfer with a proved linear intermediate-word cost.

  1. def OAI.ContinuumCoulomb.TM2Composition.computable line 15

    Source documentation

    Actual polynomial-time composition, with the intermediate length bound proved from the first machine's execution rather than postulated.

    noncomputable def computable {α β γ : Type}
    {ea : α → List Bool} {eb : β → List Bool} {ec : γ → List Bool}
    {f : α → β} {g : β → γ}
    (hf : TM2ComputableInPolyTime ea eb f) (hg : TM2ComputableInPolyTime eb ec g) :
    TM2ComputableInPolyTime ea ec (g ∘ f) :=
…