Native modular subtraction generation

The complete complement-plus-carry construction is generated from unary width. All circuit gates, wire references and output selectors are charged.

Main results

• Cslib.Circuits.Boolean.Modular.subtractCode_eq_code: exact generated code.
• Cslib.Circuits.Boolean.Modular.computableInPolyTime_subtract: native constructor.

def Cslib.Circuits.Boolean.Modular.subtractCode (w : ℕ) : List (Op × List ℕ) × List ℕ

Generate the full modular subtractor, including the shared carry and discarded carry-out.

theorem Cslib.Circuits.Boolean.Modular.subtractCode_eq_code (w : ℕ) : subtractCode w = (subtract w).code

Raw generation preserves the complete typed subtractor.

theorem Cslib.Circuits.Boolean.Modular.computableInPolyTime_subtract : Turing.MultiTapeTM.ComputableInPolyTime (fun (w : ℕ) => (subtract w).code) Turing.MultiTapeTM.encUnary encCode

Full generation is polynomial-time in unary width, including binary gate and output indices.