QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit ab8f277c5704 Build record

Three views, one set of Lean identities

From dependencies to mathematical ideas

The graph below still records generated module imports and declaration ownership, not elaborated theorem dependencies. The new atlas is a curated lens, not a replacement proof graph.

Formal topology · clickable library branches

Underlying Lean Graph of Libraries

This graph exposes the structure underneath the textbook. It shows which Lean modules support later modules, which public declarations live on each branch, and where chapters, paper reconstructions, example cases, and lexicographic circuit improvements attach to the library.

143 Lean modules 4,524 public declaration leaves 382 internal import relations

How to read the topology

Technical constructions become positions in a shared formal graph

A state-preparation method and a block-encoding method may look like unrelated gate tricks. The graph instead asks which semantic constraint they solve, which representation lemmas they share, and which new edge or reusable branch the proof contributes.

Foundations

Shared foundations

Finite matrices, resources, circuit syntax, semantics, register order, and reusable linear-algebra bridges.

Methodological reading. Choose a stable finite semantic model, make indexing conventions explicit, and factor representation lemmas before proving cases.

State prep

State Preparation

Targets, normalization, exact and approximate preparation, primitive rotations, UCRY trees, structured loaders, and sparse routes.

Methodological reading. Constrain one column of a unitary: search the unitary orbit of the all-zero ket while preserving normalization and implementation evidence.

Block encoding

Block Encoding and papers

Clean-block projections, dilations, LCU constructions, Robin operators, paper reconstructions, and same-target circuit improvements.

Methodological reading. Constrain a projected subblock of a larger unitary. Ancillas and failure branches are degrees of freedom in a unitary dilation, not informal debris.

Evidence

Harness, evidence, and publication

Candidate contracts, source-to-Lean semantic round-trip audits, executable mirrors, resource scores, literature maps, publication gates, and automation records.

Methodological reading. Freeze the semantic fibre, reconstruct theorem meaning from Lean without source prose, review any delta, and only then compare certified resources.

Case lens · proof digestion · compression corridor

What changed in the proof graph

The topological contribution is a change of factorization. The old route first forgets the generating function and expands it into explicit samples. The new route inserts a bridge from Bernstein subdivision to tensor-network memory, so the proof reaches the circuit compiler without passing through an exponentially large amplitude-list object.

Reference factorization

Expand first, then synthesize

Hermite profileexplicit amplitude listbinary mass treeUCRY circuit

Structure-aware factorization

Preserve the source representation until local compilation

Hermite profileBernstein / de Casteljauone-boundary finite-state chainbounded-bond TT / MPSlocal norm + canonicalizationisometry → SO / Givensclean Ry / CNOT circuit
BRIDGE

Approximation theory ↔ tensor networks

Bernstein subdivision turns a continuous polynomial representation into the local transition matrices of a tensor train.

SHORTCUT

Source function → circuit without materializing the full amplitude list

The proof no longer factors through one independent stored number for every grid point.

HUB

Tensor-train compilation becomes reusable

Norm contraction, canonicalization, local isometry completion and primitive compilation can support future structured state-preparation families.

REORGANIZATION

Complexity is indexed by internal width

For this family the useful structural parameter is D=2k+6, while 2^{n_p} is the ambient vector length.

Checked module corridor.
QuantumBlockEncoding.HermitePolynomial → QuantumBlockEncoding.HermiteBernstein → QuantumBlockEncoding.HermiteBoundaryInjection → QuantumBlockEncoding.HermiteFiniteChain → QuantumBlockEncoding.HermiteFiniteNorm → QuantumBlockEncoding.ConstructiveHermitePreparation

Evidence boundary. This is a curated explanatory lens over the checked module/import graph. The interactive Lean Graph still claims only generated module-import edges and declaration containment; theorem-level proof-term dependency and automatic graph compression remain future evidence layers.

Read the Hermite construction

Interactive explorer

Open a module, then inspect its declaration leaves

Drag the canvas to pan, use the wheel or controls to zoom, click a module to open its branch, and click a declaration leaf to see its statement role and source link. Search can isolate one technique, theorem family, paper, or case.

Loading the checked library graph…

Long-term structural metrics · read-only diagnostics

Library Factorization Profile

For a declared family of proof targets \(T\), let \(S_t\) be the full dependency support of target \(t\). The objective is not to make a graph cosmetically small. We measure how much mathematical support is represented once and reused across many certified targets, while retaining every original node and edge needed for Lean replay.

26 current module-frontier targets 142 unique support modules 3.93× support sharing factor 23 maximum target reuse

Unique support and expanded support

Define \(U=|\bigcup_{t\in T}S_t|\) and \(I=\sum_{t\in T}|S_t|\). Equivalently, if \(r(v)=|\{t\in T:v\in S_t\}|\), then \(I=\sum_v r(v)\). Here \(U\) counts maintained support nodes once; \(I\) is the support mass obtained by expanding every target separately.

Structural sharing

We report \(F_{\rm share}=I/U\) and \(G_{\rm reuse}=1-U/I\), together with the coverage \(C_{\rm shared}=|\{v:r(v)\ge2\}|/U\). These describe sharing; they do not certify that two proofs are semantically interchangeable.

Reuse concentration

The pairwise sharing mass is \(P_{\rm share}=\sum_v\binom{r(v)}2 =\sum_{s<t}|S_s\cap S_t|\). It distinguishes a genuinely central lemma reused by many targets from many local lemmas each reused only twice. We also retain the full reuse histogram and \(\max_v r(v)\).

Topology contribution of new work

For a new paper or construction we want a vector: new nodes, new edges, reuse of old support, newly shared nodes, cross-family bridge edges, and changes in sharing statistics. This helps distinguish a marginal new leaf from a lemma that reorganizes several State Preparation or Block Encoding proof families.

Current measured layer. The displayed numbers use only the generated Lean module import DAG, excluding the root barrel module and taking non-barrel frontier modules as temporary targets. When theorem-level proof-term dependencies are exported, the same definitions will be applied to explicit theorem/case/paper target sets. Historical values must record both the evidence layer and target-selection policy.
Anti-gaming rule. These metrics are a diagnostic vector, not a scalar objective. Minimizing node count or maximizing fan-out alone is invalid: one giant opaque lemma could score well while making the mathematical library worse. Any refactor must preserve exact types, replayable dependencies, source provenance, checker admission, and reader-meaningful boundaries. ZDD/MIP or quotienting remains downstream of theorem-level dependency extraction and empirical evidence that such a representation helps.

Next topology layer

From an import graph to a compressed proof graph

Compress repeated subproofs

Detect isomorphic proof subgraphs, promote their common invariant to one reusable lemma, and measure how much later formalization becomes shorter and more stable.

Quotient equivalent routes

Separate genuine mathematical choices from syntactic proof variation. Equivalent branches can be grouped while preserving source fidelity and exact Lean provenance.

Read the matrix geometry

State preparation fixes a unitary column; block encoding fixes a projected subblock of a dilation. Ancilla, clean-workspace, sparsity, and oracle requirements define different feasible fibres over those constraints.

Interpret evolution correctly

Lexicographic improvement is search inside a correctness fibre: target equality first, then gate count, depth, auxiliary qubits, and oracle calls. A new topology is valuable when it creates reusable understanding, not merely a smaller isolated circuit.

Current evidence boundary. Import edges and public declaration containment are generated from this checkout. The theorem-level dependency DAG and its compression quotient remain an explicit roadmap item, so this page does not overstate what has already been extracted from Lean proof terms.