15 Boolean Analysis — Gate Merge

15.1 Overview

This module provides infrastructure for merging two gate arrays, indexed by \(\mathrm{Fin}\, m_1\) and \(\mathrm{Fin}\, m_2\), into a single array indexed by \(\mathrm{Fin}\, (m_1 + m_2)\). It records the two projection equations for the merged array, lemmas showing that circuit reindexing reroutes evaluation correctly through the merged gates, and lemmas establishing that DNF width, variable injectivity, and no-duplication properties are preserved under merging.

15.2 Declarations

Definition 15.1 Merge of two gate arrays

✓

Given gate arrays \(g_1 : \mathrm{Fin}\, m_1 \to \alpha \) and \(g_2 : \mathrm{Fin}\, m_2 \to \alpha \), the merged array \(\mathrm{mergeGates}\, g_1\, g_2 : \mathrm{Fin}\, (m_1+m_2) \to \alpha \) takes its values from \(g_1\) on indices \(0,\dots ,m_1-1\) and from \(g_2\) on indices \(m_1,\dots ,m_1+m_2-1\).

Lemma 15.2 Left projection of merge

✓

For every \(i : \mathrm{Fin}\, m_1\), evaluating the merged array at the left-embedded index \(\mathrm{castAdd}\, m_2\, i\) recovers \(g_1\, i\), i.e. \(\mathrm{mergeGates}\, g_1\, g_2\, (\mathrm{castAdd}\, m_2\, i) = g_1\, i\).

Lemma 15.3 Right projection of merge

✓

For every \(i : \mathrm{Fin}\, m_2\), evaluating the merged array at the right-embedded index \(\mathrm{natAdd}\, m_1\, i\) recovers \(g_2\, i\), i.e. \(\mathrm{mergeGates}\, g_1\, g_2\, (\mathrm{natAdd}\, m_1\, i) = g_2\, i\).

Lemma 15.4 Reindex into left half evaluates the original

✓

For a circuit \(c\) on \(m_1\) gates and Boolean gate values \(g_1, g_2\), reindexing \(c\) along the left embedding \(\mathrm{castAdd}\, m_2\) and evaluating against the merged array yields the original evaluation: \((\mathrm{reidx}\, c\, (\mathrm{castAdd}\, m_2)).\mathrm{eval}\, (\mathrm{mergeGates}\, g_1\, g_2) = c.\mathrm{eval}\, g_1\).

Lemma 15.5 Reindex into right half evaluates the original

✓

For a circuit \(c\) on \(m_2\) gates and Boolean gate values \(g_1, g_2\), reindexing \(c\) along the right embedding \(\mathrm{natAdd}\, m_1\) and evaluating against the merged array yields the original evaluation: \((\mathrm{reidx}\, c\, (\mathrm{natAdd}\, m_1)).\mathrm{eval}\, (\mathrm{mergeGates}\, g_1\, g_2) = c.\mathrm{eval}\, g_2\).

Lemma 15.6 Width bound on the left part of a merge

✓

If every \(g_1\, k\) has width at most \(l\), then for each \(i : \mathrm{Fin}\, m_1\) the merged gate at the left-embedded index satisfies \((\mathrm{mergeGates}\, g_1\, g_2\, (\mathrm{castAdd}\, m_2\, i)).\mathrm{width} \le l\).

Lemma 15.7 Width bound on the right part of a merge

✓

If every \(g_2\, k\) has width at most \(l\), then for each \(i : \mathrm{Fin}\, m_2\) the merged gate at the right-embedded index satisfies \((\mathrm{mergeGates}\, g_1\, g_2\, (\mathrm{natAdd}\, m_1\, i)).\mathrm{width} \le l\).

Lemma 15.8 Width bound preserved under merging

✓

If every gate of \(g_1\) and every gate of \(g_2\) has width at most \(l\), then every gate of the merged array \(\mathrm{mergeGates}\, g_1\, g_2\) has width at most \(l\).

Lemma 15.9 Variable injectivity preserved under merging

✓

If, in each DNF gate of \(g_1\) and of \(g_2\), any two literals of a common term that share the same variable are equal, then the same holds for every gate of the merged array \(\mathrm{mergeGates}\, g_1\, g_2\).

Lemma 15.10 No-duplication preserved under merging

✓

If every term of every DNF gate of \(g_1\) and of \(g_2\) has no duplicate literals (\(\mathrm{Nodup}\)), then every term of every gate of the merged array \(\mathrm{mergeGates}\, g_1\, g_2\) likewise has no duplicate literals.