Raw Clause Hamiltonian and Full Trace
Abstract
A full complex matrix exponential encodes the raw Boolean satisfying count.
Notation is local to each arbitrary n in Nat and raw F in Formula n. Assignment n is Fin n to Bool, and Formula n is the list of raw clauses over Fin n. Every abbreviation below is evaluated at these same n and F; their dependence on n and F is suppressed only in their short names. IA and IB are the identities on Bool and Assignment n, respectively; dB is their hidden dimension cast to Complex, while k and N are natural numbers.
P is the fixed visible projector, HB and H are the actual hidden and full Hamiltonians, and Ac and Bc are the centered visible and shifted hidden matrices. Z is the actual complex exponential trace. The following are definitions of notation, not additional hypotheses:
The inverse temperature beta is real. X, XA, XB, XAc and XBc are the CStar matrix exponents on Bool times Assignment n, Bool, Assignment n, Bool and Assignment n, respectively:
For any self-adjointness witness of the indicated exponent, GX, GA, GB, GAc and GBc denote the actual Gibbs density states. Each retains its displayed witness argument and the same suppressed n and F:
For every real t, U and UA are the actual matrix exponentials. C is the joint commutator for any visible complex matrix M:
R is the product of any visible density state rho with the hidden Gibbs state chosen using the same hB. Singular rho is allowed:
Theorem 1.1 (Dyadic partition and integer count recovery).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/ClauseHamiltonian.clause_partition_recovery (✓ std3). ∎
Source. Repository-derived.
Commentary.
Each raw clause determines the diagonal projector onto its violating assignments. The hidden Hamiltonian is n plus one times their sum. The full Hamiltonian is the visible one-state projector tensor the hidden identity, plus the visible identity tensor that hidden Hamiltonian. The inverse temperature is log two.
The partition is defined as the trace of the genuine complex matrix exponential, independently of the count. If m is the raw clause count and N sums two to the power (n plus one) times m minus the number of violated clauses over every assignment, the full partition is three N divided by two to the power (n plus one) m plus one.
The floor of two thirds of the real partition is exactly the number of satisfying assignments in the declared universe. The unsatisfying Boltzmann tail is between zero and one half. All universe sizes, including the zero-variable singleton, and all raw clause lists are covered.
Every clause is a Hermitian idempotent diagonal projector. Its diagonal depends only on its literal variables, whose number is at most the clause length. The exact normalized partial traces give the visible centered projector and the hidden Hamiltonian shifted by one half of the identity. Their tensor sum is the original full Hamiltonian, and every visible commutator remains in the complete visible matrix algebra. All clause projectors commute; an empty clause is the identity projector. The normalized conditional-expectation residual vanishes for every visible matrix. For every joint matrix and every real time, its evolved visible marginal is exactly the marginal evolved by the same centered visible Hamiltonian.
The short notation denotes the actual named Hamiltonian, projector, partition and count definitions specified above. identity carries its displayed finite carrier; tensor is the Kronecker product, scale is scalar multiplication, and adjoint is conjugate transpose. exp is the actual matrix exponential and re is the complex real part. castNat and castInt are the displayed natural and integer casts. ofMatrix is the CStar matrix image; underlyingMatrix extracts the ordinary matrix from a density state. eval and apply denote function and matrix entries.
The five self-adjointness witnesses concern minus log two times the full, visible, hidden, centered visible and shifted hidden Hamiltonians, respectively. gibbsState is the positive trace-one normalized exponential of that exponent. The full Gibbs state is the product of the centered visible Gibbs state and the hidden Gibbs state. Both scalar shifts leave their Gibbs states unchanged; the actual hidden marginal is the hidden Gibbs state. At zero variables it is the singleton identity.
Every visible density state, including singular ones, is supported inside the centered visible Gibbs state, and its product with the hidden Gibbs state is supported inside the full Gibbs state. extendedQuantumRelativeEntropy is the support-aware entropy; quantumRelativeEntropy is its finite trace-log branch. The actual visible marginal, equality of extended relative entropies, zero finite defect and zero reconstruction relative entropy all hold for this identical Hamiltonian.
This identity does not itself establish a canonical rational word, a query codec, an operational one-query protocol or efficient hidden Gibbs preparation.