Reusable theorem templates

This chapter collects proof architectures that recur across gate logics. Each template separates the easy upper-bound identity from the difficult lower-bound obligation. The templates are not claims that every gate hierarchy satisfies the hypotheses.

Permalink · Source line 5042

Let \(H\le G\) have restricted and ambient costs with \({\ell_{\mathrm{amb}}}(g^{-1})={\ell_{\mathrm{amb}}}(g)\). Choose \(g\in G\) and \(h_1,\ldots,h_m\in H\) such that

Then

Permalink · Source line 5045

The proof is immediate. The research content lies in bounding \(\beta\).

Permalink · Source line 5073

Suppose a catalyst costs \(c_{\mathrm{open}}+c_{\mathrm{close}}\) and each of \(m\) consumers saves at least \(s_i\) restricted cost. Then

where \(r\) is repair or interference cost. A threshold occurs when the right side first becomes positive.

This template explains the three-cross rule in the linear atom and guides searches in phase, Gaussian, and routing models.

Permalink · Source line 5076

Let \(S\) be a finite symmetric generating set and

Then

Permalink · Source line 5088

This template provides an exact spectral restatement. To turn it into a lower bound without enumeration, one needs control of the endpoint projector coefficients.

Permalink · Source line 5109

Let \(F\) be a function on circuit states satisfying

for every allowed restricted gate \(s\). Then

Potential design steps:

Permalink · Source line 5112

1. choose a decomposition into cuts, packets, or degree layers;

2. prove a gate changes the total charge by at most its cost;

3. ensure cancellations cannot create free progress on many layers;

4. evaluate the target exactly.

Permalink · Source line 5124

Static sums of ranks are often too coarse in ambient models; time-expanded or target-relative potentials may be required.

Permalink · Source line 5130

Let \(X\) be an algebraic family of elementary gates whose irreducible components have dimension at most \(r\). Let \(V\) be an irreducible target variety of dimension \(N\).

Permalink · Source line 5133

If every target in \(V\) has a restricted construction of length at most \(N/r\), then generic restricted and ambient lengths coincide at that value, provided the same parameter bound applies to the ambient alphabet.

Permalink · Source line 5139

Assume every target has restricted cost at most \(M\). A defect of size at least \(d\) implies ambient cost at most \(M-d\). If the \((M-d)\)-gate ambient locus has dimension at most \(N-d\), then

This is the general mechanism behind algebraic rarity.

Permalink · Source line 5142

Suppose there are at most \(B\) gate directions and at most \(q^r\) parameter choices per gate over \({\mathbb F}_q\). Then the number of words of length at most \(L\) is at most

If the target family has \(q^N\) points and defect \(d\) forces \(L\le (N-d)/r\), this yields a density bound of order \(q^{-d}\) up to a fixed combinatorial factor.

The estimate counts words, not distinct endpoints, and is therefore an upper bound without injectivity assumptions.

Permalink · Source line 5149

Let a large restricted group contain a smaller one through a homomorphic embedding \(\iota\), and suppose a homomorphic retraction \(\pi\) satisfies \(\pi\iota=\operatorname{id}\). Require that every large restricted generator maps to a small restricted word of no greater cost. Then

If the ambient embedding preserves gate cost,

This transfers a catalytic atom to architectures containing it as a retract.

Permalink · Source line 5158

For block-lower matrices

projection to diagonal blocks forces the costs of \(A\) and \(D\), while rank of the cross block forces at least \({\operatorname{rank}} X\) cross transmissions. If \(X\) is a partial monomial matrix, the lower bound is attained by direct construction.

The same logic extends to trees of blocks whenever every coupling layer has an exact rank certificate and the projections are homomorphisms.

Permalink · Source line 5173

Suppose a restricted complexity is tree tight and satisfies

for \(A\) of size \(m\) and \(B\) of size \(n\). If ambient complexity satisfies the corresponding upper bound, then

For tensor powers,

This is the standard route from a finite atom to an \(N\log N\) defect.

Permalink · Source line 5186

If

then

is subadditive and

exists by Fekete's lemma. This defines a regularized ambient cost and exposes possible tensor activation.

Permalink · Source line 5206

Let gates carry costs in \({\mathbb R}_+^k\). A lower bound may be a vector inequality

or a family of scalar inequalities indexed by dual weights \(w\in{\mathbb R}_+^k\):

A complete Pareto proof may require enough supporting weights to separate the restricted and ambient convex lower hulls.

Permalink · Source line 5221

Let \(W\) act on data \(D\) and ancilla \(A\). To certify a dirty catalyst, prove the operator identity

on the full joint space, not only on one ancilla input. For a clean catalyst, prove

for all \({\lvert \psi\rangle}\). The distinction changes both the target equations and lower bounds.

Permalink · Source line 5232

Given projectors \(P_q\), define off-sector transfer blocks

A restricted gate preserves all diagonal sectors. An ambient gate changes a controlled collection of blocks. A candidate potential is a weighted sum of ranks or norms of obligations relative to the final target. The proof must charge both creation and useful consumption of off-sector coherence.

Permalink · Source line 5244

A finite first-threshold theorem should contain:

Permalink · Source line 5251

1. no defects below size \(n_0\);

2. at least one defect at \(n_0\);

3. exact classification of every defect at \(n_0\) modulo declared equivalence;

4. analytic generation of the exceptional motifs;

5. equality between the analytic set and computational census;

6. witness and completeness certificates.

Permalink · Source line 5252

This is the standard achieved by the six-wire linear core and is the target standard for future gate logics.

Permalink · Source line 5260

Before promoting a catalytic identity to a theorem, record:

Permalink · Source line 5263