Lowering finite joins to binary cyclic AND/OR circuits

This module expands every finite join into a local binary-OR accumulator and maps binary meet directly to binary AND. Each join block begins with a self-referential OR gate; its least fixed point is the empty set, so nullary join is implemented without adding a constant operation. The expansion adds no charged AND gates.

@[reducible]

def Algebraic.Fusion.JoinMeetLowering.blockGateCount : JoinMeet.Op → ℕ

Number of binary gates in one expanded operation block.

Equations

• Algebraic.Fusion.JoinMeetLowering.blockGateCount Algebraic.JoinMeet.Op.meet = 1
• Algebraic.Fusion.JoinMeetLowering.blockGateCount (Algebraic.JoinMeet.Op.join count) = count + 1

theorem Algebraic.Fusion.JoinMeetLowering.blockGateCount_meet : blockGateCount JoinMeet.Op.meet = 1

theorem Algebraic.Fusion.JoinMeetLowering.blockGateCount_join (count : ℕ) : blockGateCount (JoinMeet.Op.join count) = count + 1

def Algebraic.Fusion.JoinMeetLowering.rootLocal (op : JoinMeet.Op) : Fin (blockGateCount op)

Local output gate of an expanded operation block.

Equations

• Algebraic.Fusion.JoinMeetLowering.rootLocal Algebraic.JoinMeet.Op.meet = ⟨0, Algebraic.Fusion.JoinMeetLowering.rootLocal._proof_1⟩
• Algebraic.Fusion.JoinMeetLowering.rootLocal (Algebraic.JoinMeet.Op.join count) = Fin.last count

@[reducible, inline]

abbrev Algebraic.Fusion.JoinMeetLowering.ExpandedGate {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) : Type

Dependent collection of all gates in all expanded blocks.

Equations

• Algebraic.Fusion.JoinMeetLowering.ExpandedGate source = ((gate : Fin g) × Fin (Algebraic.Fusion.JoinMeetLowering.blockGateCount (source.lines gate).op))

noncomputable def Algebraic.Fusion.JoinMeetLowering.gateCount {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) : ℕ

Number of gates in the binary expansion.

Equations

• Algebraic.Fusion.JoinMeetLowering.gateCount source = Fintype.card (Algebraic.Fusion.JoinMeetLowering.ExpandedGate source)

noncomputable def Algebraic.Fusion.JoinMeetLowering.gateEquiv {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) : ExpandedGate source ≃ Fin (gateCount source)

Chosen numbering of the dependent expanded-gate collection.

Equations

• Algebraic.Fusion.JoinMeetLowering.gateEquiv source = Fintype.equivFin (Algebraic.Fusion.JoinMeetLowering.ExpandedGate source)

noncomputable def Algebraic.Fusion.JoinMeetLowering.expandedGate {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) (gate : Fin g) (localGate : Fin (blockGateCount (source.lines gate).op)) : Fin (gateCount source)

Number a particular local gate of a particular source block.

Equations

• Algebraic.Fusion.JoinMeetLowering.expandedGate source gate localGate = (Algebraic.Fusion.JoinMeetLowering.gateEquiv source) ⟨gate, localGate⟩

noncomputable def Algebraic.Fusion.JoinMeetLowering.rootGate {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) (gate : Fin g) : Fin (gateCount source)

Number the output gate of a source block.

Equations

• Algebraic.Fusion.JoinMeetLowering.rootGate source gate = Algebraic.Fusion.JoinMeetLowering.expandedGate source gate (Algebraic.Fusion.JoinMeetLowering.rootLocal (source.lines gate).op)

noncomputable def Algebraic.Fusion.JoinMeetLowering.translateWire {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) : Wire n g → Wire n (gateCount source)

Translate an original input-or-gate wire to the corresponding binary input-or-block-root wire.

Equations

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

def Algebraic.Fusion.JoinMeetLowering.binaryLine {n g : ℕ} (op : AndOr.Op) (left right : Wire n g) : Line AndOr.signature n g

A binary line with the two specified wires.

Equations

• Algebraic.Fusion.JoinMeetLowering.binaryLine op left right = { op := op, wires := fun (i : Fin (1 + 1)) => Fin.cases left (fun (i : Fin (0 + 1)) => Fin.cases right Fin.elim0 i) i }

@[simp]

theorem Algebraic.Fusion.JoinMeetLowering.binaryLine_wire_zero {n g : ℕ} (op : AndOr.Op) (left right : Wire n g) : (binaryLine op left right).wires 0 = left

@[simp]

theorem Algebraic.Fusion.JoinMeetLowering.binaryLine_wire_one {n g : ℕ} (op : AndOr.Op) (left right : Wire n g) : (binaryLine op left right).wires 1 = right

theorem Algebraic.Fusion.JoinMeetLowering.binaryLine_eval_or {n g : ℕ} {Γ : Type u_1} (left right : Wire n g) (inputs : Fin n → Set Γ) (state : Fin g → Set Γ) : (binaryLine AndOr.Op.or left right).eval (AndOr.setInterpretation Γ) inputs state = Wire.elim inputs state left ∪ Wire.elim inputs state right

Evaluation of a binary OR line.

theorem Algebraic.Fusion.JoinMeetLowering.binaryLine_eval_and {n g : ℕ} {Γ : Type u_1} (left right : Wire n g) (inputs : Fin n → Set Γ) (state : Fin g → Set Γ) : (binaryLine AndOr.Op.and left right).eval (AndOr.setInterpretation Γ) inputs state = Wire.elim inputs state left ∩ Wire.elim inputs state right

Evaluation of a binary AND line.

def Algebraic.Fusion.JoinMeetLowering.blockLineOf {n g h : ℕ} (line : Line JoinMeet.signature n g) (encode : Fin (blockGateCount line.op) → Fin h) (translate : Wire n g → Wire n h) : Fin (blockGateCount line.op) → Line AndOr.signature n h

Expand one source line, given a numbering of its local block gates and a translation of its source wires.

Equations

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

noncomputable def Algebraic.Fusion.JoinMeetLowering.blockLine {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) (gate : Fin g) : Fin (blockGateCount (source.lines gate).op) → Line AndOr.signature n (gateCount source)

Binary line at a local gate of one expanded source block.

Equations

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

noncomputable def Algebraic.Fusion.JoinMeetLowering.circuit {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) : CyclicCircuit AndOr.signature n (gateCount source)

Binary AND/OR expansion of a finite-join/meet cyclic circuit.

Equations

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

@[simp]

theorem Algebraic.Fusion.JoinMeetLowering.circuit_line_expandedGate {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) (gate : Fin g) (localGate : Fin (blockGateCount (source.lines gate).op)) : (circuit source).lines (expandedGate source gate localGate) = blockLine source gate localGate

@[simp]

theorem Algebraic.Fusion.JoinMeetLowering.circuit_output {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) : (circuit source).output = rootGate source source.output

def Algebraic.Fusion.JoinMeetLowering.sourceWireValue {n : ℕ} {Γ : Type u_1} {g : ℕ} (inputs : Fin n → Set Γ) (state : Fin g → Set Γ) : Wire n g → Set Γ

Value carried by an original input-or-gate wire.

Equations

• Algebraic.Fusion.JoinMeetLowering.sourceWireValue inputs state = Cslib.Circuits.Wire.elim inputs state

def Algebraic.Fusion.JoinMeetLowering.joinPrefix {count : ℕ} {Γ : Type u_1} (arguments : Fin count → Set Γ) (position : Fin (count + 1)) : Set Γ

Union of those arguments whose indices occur before a local accumulator position. Position zero is bottom; position i + 1 includes arguments through i.

Equations

• Algebraic.Fusion.JoinMeetLowering.joinPrefix arguments position = {point : Γ | ∃ (index : Fin count), ↑index < ↑position ∧ point ∈ arguments index}

@[simp]

theorem Algebraic.Fusion.JoinMeetLowering.joinPrefix_zero {count : ℕ} {Γ : Type u_1} (arguments : Fin count → Set Γ) : joinPrefix arguments 0 = ∅

theorem Algebraic.Fusion.JoinMeetLowering.joinPrefix_succ {count : ℕ} {Γ : Type u_1} (arguments : Fin count → Set Γ) (index : Fin count) : joinPrefix arguments index.succ = joinPrefix arguments index.castSucc ∪ arguments index

One accumulator step adds exactly its next argument.

theorem Algebraic.Fusion.JoinMeetLowering.joinPrefix_last {count : ℕ} {Γ : Type u_1} (arguments : Fin count → Set Γ) : joinPrefix arguments (Fin.last count) = {point : Γ | ∃ (index : Fin count), point ∈ arguments index}

The root accumulator contains the union of all arguments.

def Algebraic.Fusion.JoinMeetLowering.blockValueOf {n g : ℕ} {Γ : Type u_1} (line : Line JoinMeet.signature n g) (rootValue : Set Γ) (arguments : Fin (JoinMeet.signature.Arity line.op) → Set Γ) : Fin (blockGateCount line.op) → Set Γ

Intended local values of one expanded source block.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Fusion.JoinMeetLowering.blockValueOf { op := Algebraic.JoinMeet.Op.join arity, wires := wires } rootValue arguments_2 = Algebraic.Fusion.JoinMeetLowering.joinPrefix arguments_2

def Algebraic.Fusion.JoinMeetLowering.blockValue {n g : ℕ} {Γ : Type u_1} (source : CyclicCircuit JoinMeet.signature n g) (inputs : Fin n → Set Γ) (state : Fin g → Set Γ) (gate : Fin g) : Fin (blockGateCount (source.lines gate).op) → Set Γ

Intended values in one block, computed from an original cyclic state.

Equations

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

noncomputable def Algebraic.Fusion.JoinMeetLowering.values {n g : ℕ} {Γ : Type u_1} (source : CyclicCircuit JoinMeet.signature n g) (inputs : Fin n → Set Γ) (state : Fin g → Set Γ) : Fin (gateCount source) → Set Γ

Intended state of the binary expanded circuit.

Equations

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

@[simp]

theorem Algebraic.Fusion.JoinMeetLowering.values_expandedGate {n g : ℕ} {Γ : Type u_1} (source : CyclicCircuit JoinMeet.signature n g) (inputs : Fin n → Set Γ) (state : Fin g → Set Γ) (gate : Fin g) (localGate : Fin (blockGateCount (source.lines gate).op)) : values source inputs state (expandedGate source gate localGate) = blockValue source inputs state gate localGate

theorem Algebraic.Fusion.JoinMeetLowering.blockValueOf_root {n g : ℕ} {Γ : Type u_1} (line : Line JoinMeet.signature n g) (rootValue : Set Γ) (arguments : Fin (JoinMeet.signature.Arity line.op) → Set Γ) (fixed : rootValue = JoinMeet.setInterpretation Γ line.op arguments) : blockValueOf line rootValue arguments (rootLocal line.op) = rootValue

The root of a local block has the supplied source value whenever that value satisfies the source operation.

theorem Algebraic.Fusion.JoinMeetLowering.blockValue_root {n g : ℕ} {Γ : Type u_1} (source : CyclicCircuit JoinMeet.signature n g) (inputs : Fin n → Set Γ) (state : Fin g → Set Γ) (fixed : ∀ (gate : Fin g), state gate = (source.atomAt inputs state gate).result (JoinMeet.setInterpretation Γ)) (gate : Fin g) : blockValue source inputs state gate (rootLocal (source.lines gate).op) = state gate

The root of every expanded block carries its original source-gate value whenever the source state satisfies its equations.

theorem Algebraic.Fusion.JoinMeetLowering.translatedWire_value {n g : ℕ} {Γ : Type u_1} (source : CyclicCircuit JoinMeet.signature n g) (inputs : Fin n → Set Γ) (state : Fin g → Set Γ) (fixed : ∀ (gate : Fin g), state gate = (source.atomAt inputs state gate).result (JoinMeet.setInterpretation Γ)) (wire : Wire n g) : Wire.elim inputs (values source inputs state) (translateWire source wire) = sourceWireValue inputs state wire

Reading a translated source wire in the expanded values returns the original wire value.

theorem Algebraic.Fusion.JoinMeetLowering.blockValueOf_fixed {n g h : ℕ} {Γ : Type u_1} (line : Line JoinMeet.signature n g) (encode : Fin (blockGateCount line.op) → Fin h) (translate : Wire n g → Wire n h) (inputs : Fin n → Set Γ) (targetState : Fin h → Set Γ) (rootValue : Set Γ) (arguments : Fin (JoinMeet.signature.Arity line.op) → Set Γ) (fixed : rootValue = JoinMeet.setInterpretation Γ line.op arguments) (encodeValue : ∀ (localGate : Fin (blockGateCount line.op)), targetState (encode localGate) = blockValueOf line rootValue arguments localGate) (translateValue : ∀ (index : Fin (JoinMeet.signature.Arity line.op)), Wire.elim inputs targetState (translate (line.wires index)) = arguments index) (localGate : Fin (blockGateCount line.op)) : blockValueOf line rootValue arguments localGate = (blockLineOf line encode translate localGate).eval (AndOr.setInterpretation Γ) inputs targetState

Local block values satisfy the expanded binary equations whenever encoded gates and translated wires have their intended values.

theorem Algebraic.Fusion.JoinMeetLowering.values_fixed {n g : ℕ} {Γ : Type u_1} (source : CyclicCircuit JoinMeet.signature n g) (inputs : Fin n → Set Γ) (state : Fin g → Set Γ) (fixed : ∀ (gate : Fin g), state gate = (source.atomAt inputs state gate).result (JoinMeet.setInterpretation Γ)) (targetGate : Fin (gateCount source)) : values source inputs state targetGate = ((circuit source).atomAt inputs (values source inputs state) targetGate).result (AndOr.setInterpretation Γ)

The expanded values satisfy every binary cyclic equation.

noncomputable def Algebraic.Fusion.JoinMeetLowering.restrictedState {n g : ℕ} {Γ : Type u_1} (source : CyclicCircuit JoinMeet.signature n g) (targetState : Fin (gateCount source) → Set Γ) : Fin g → Set Γ

State on original gates obtained by reading expanded block roots.

Equations

• Algebraic.Fusion.JoinMeetLowering.restrictedState source targetState gate = targetState (Algebraic.Fusion.JoinMeetLowering.rootGate source gate)

theorem Algebraic.Fusion.JoinMeetLowering.restrictedWire_value {n g : ℕ} {Γ : Type u_1} (source : CyclicCircuit JoinMeet.signature n g) (inputs : Fin n → Set Γ) (targetState : Fin (gateCount source) → Set Γ) (wire : Wire n g) : sourceWireValue inputs (restrictedState source targetState) wire = Wire.elim inputs targetState (translateWire source wire)

Original wire values in the restricted state are target wire values along the wire translation.

theorem Algebraic.Fusion.JoinMeetLowering.joinPrefix_subset {count : ℕ} {Γ : Type u_1} {h : ℕ} (arguments : Fin count → Set Γ) (state : Fin h → Set Γ) (encode : Fin (count + 1) → Fin h) (step : ∀ (index : Fin count), state (encode index.castSucc) ∪ arguments index ⊆ state (encode index.succ)) (position : Fin (count + 1)) : joinPrefix arguments position ⊆ state (encode position)

Prefix unions lie below accumulator gates whenever every accumulator step is pre-fixed.

theorem Algebraic.Fusion.JoinMeetLowering.sourceResult_subset_root {n g h : ℕ} {Γ : Type u_1} (line : Line JoinMeet.signature n g) (encode : Fin (blockGateCount line.op) → Fin h) (translate : Wire n g → Wire n h) (inputs : Fin n → Set Γ) (targetState : Fin h → Set Γ) (blockPrefixed : ∀ (localGate : Fin (blockGateCount line.op)), (blockLineOf line encode translate localGate).eval (AndOr.setInterpretation Γ) inputs targetState ⊆ targetState (encode localGate)) : JoinMeet.setInterpretation Γ line.op (Wire.elim inputs targetState ∘ translate ∘ line.wires) ⊆ targetState (encode (rootLocal line.op))

A pre-fixed expanded block makes the corresponding source operation pre-fixed at its block root.

theorem Algebraic.Fusion.JoinMeetLowering.restrictedState_prefixed {n g : ℕ} {Γ : Type u_1} (source : CyclicCircuit JoinMeet.signature n g) (inputs : Fin n → Set Γ) (targetState : Fin (gateCount source) → Set Γ) (prefixed : (circuit source).IsPrefixed (AndOr.setInterpretation Γ) inputs targetState) : source.IsPrefixed (JoinMeet.setInterpretation Γ) inputs (restrictedState source targetState)

Every pre-fixed binary expansion restricts to a pre-fixed finite-join/meet state.

theorem Algebraic.Fusion.JoinMeetLowering.joinPrefix_mono {count : ℕ} {Γ : Type u_1} {lower upper : Fin count → Set Γ} (subset : ∀ (index : Fin count), lower index ⊆ upper index) (position : Fin (count + 1)) : joinPrefix lower position ⊆ joinPrefix upper position

Prefix unions are monotone in all their arguments.

theorem Algebraic.Fusion.JoinMeetLowering.blockValueOf_subset_of_prefixed {n g h : ℕ} {Γ : Type u_1} (line : Line JoinMeet.signature n g) (encode : Fin (blockGateCount line.op) → Fin h) (translate : Wire n g → Wire n h) (inputs : Fin n → Set Γ) (targetState : Fin h → Set Γ) (rootValue : Set Γ) (arguments : Fin (JoinMeet.signature.Arity line.op) → Set Γ) (rootSubset : rootValue ⊆ targetState (encode (rootLocal line.op))) (argumentSubset : ∀ (index : Fin (JoinMeet.signature.Arity line.op)), arguments index ⊆ Wire.elim inputs targetState (translate (line.wires index))) (blockPrefixed : ∀ (localGate : Fin (blockGateCount line.op)), (blockLineOf line encode translate localGate).eval (AndOr.setInterpretation Γ) inputs targetState ⊆ targetState (encode localGate)) (localGate : Fin (blockGateCount line.op)) : blockValueOf line rootValue arguments localGate ⊆ targetState (encode localGate)

Intended local block values lie below any pre-fixed target block once the source root and arguments lie below their target representatives.

theorem Algebraic.Fusion.JoinMeetLowering.sourceWire_subset_target {n g : ℕ} {Γ : Type u_1} (source : CyclicCircuit JoinMeet.signature n g) (inputs : Fin n → Set Γ) (sourceState : Fin g → Set Γ) (targetState : Fin (gateCount source) → Set Γ) (sourceSubset : ∀ (gate : Fin g), sourceState gate ⊆ targetState (rootGate source gate)) (wire : Wire n g) : sourceWireValue inputs sourceState wire ⊆ Wire.elim inputs targetState (translateWire source wire)

Original source-wire values lie below translated target wires once source gate values lie below target roots.

theorem Algebraic.Fusion.JoinMeetLowering.values_least {Γ : Type u_1} {g : ℕ} {problem : SetProblem Γ} (source : CyclicCircuit JoinMeet.signature problem.inputCount g) (constructs : source.Constructs (JoinMeet.setInterpretation Γ)) (targetState : Fin (gateCount source) → Set Γ) (prefixed : (circuit source).IsPrefixed (AndOr.setInterpretation Γ) problem.inputs targetState) (targetGate : Fin (gateCount source)) : values source problem.inputs constructs.values targetGate ⊆ targetState targetGate

The canonical expanded values form the least pre-fixed binary state.

noncomputable def Algebraic.Fusion.JoinMeetLowering.constructs {Γ : Type u_1} {g : ℕ} {problem : SetProblem Γ} (source : CyclicCircuit JoinMeet.signature problem.inputCount g) (sourceConstructs : source.Constructs (JoinMeet.setInterpretation Γ)) : (circuit source).Constructs (AndOr.setInterpretation Γ)

Lower a proof-carrying finite-join/meet construction to the ordinary binary AND/OR cyclic basis.

Equations

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

theorem Algebraic.Fusion.JoinMeetLowering.listOfFn_sum_eq_fintype_sum {count : ℕ} (function : Fin count → ℕ) : (List.ofFn function).sum = ∑ index : Fin count, function index

Sum of a finite function agrees with the sum of its List.ofFn enumeration.

theorem Algebraic.Fusion.JoinMeetLowering.block_cost {n g h : ℕ} (line : Line JoinMeet.signature n g) (encode : Fin (blockGateCount line.op) → Fin h) (translate : Wire n g → Wire n h) : ∑ localGate : Fin (blockGateCount line.op), AndOr.andCost (blockLineOf line encode translate localGate).op = JoinMeet.meetCost line.op

One expanded block has exactly the charged cost of its source operation.

theorem Algebraic.Fusion.JoinMeetLowering.circuit_cost {n g : ℕ} (source : CyclicCircuit JoinMeet.signature n g) : (circuit source).cost AndOr.andCost = source.cost JoinMeet.meetCost

Lowering preserves charged meet/AND cost exactly.