Daniel Fredriksen · Quantyra Inc. · ORCID 0009-0002-9123-7435
Read the manuscript PDF · LaTeX source · Reproduce the checks · Review and limitations
Version 0.1.0, published as an informal methods preprint with internal mathematical and executable checks. Paper version DOI: 10.5281/zenodo.23754698; paper concept DOI: 10.5281/zenodo.23754697. Lean certification is in progress against the frozen paper; the current claim inventory and audit receipts are in lean/CLAIMS.json and lean/evidence. At Lean source commit a335d89, the interleaved-to-canonical block assignment and phase helpers passed the dedicated Google Cloud build and exact axiom audit; the receipt records that run. At 26a7479, explicit inverses prove the layout bijection, its map of the binary basis is a permutation, and the generic integer-sum reindexing theorem passes the integrated build and exact axiom audit; the receipt records this run. At 33130b7, the recorded pair phase is related to its inverse-reindexed even/odd coordinate assignment; its integrated build and exact axiom checker pass. The source-to-closed-form composition, normalization/boundedness, cost bounds and all seven manuscript theorem labels remain open.
The paper constructs an estimator for one output probability of a specified two-layer Boolean cubic-phase circuit. An output-derived displacement space can have a small restricted cubic control count even when specified global controls grow. Using established stabilizer norm estimation reduces the readout factor from 4^k to 2^k, with all source, discovery, arithmetic, random-bit and precision costs included.
General discovery retains a full-rank-anchor promise and 2^O(q^2) cost. The implementation accepts a verified canonical native encoding; it is not a general circuit-equivalence recognizer. The larger sampling constant loses on the executed small-control examples. No practical superiority, quantum advantage, universal simulation, peer review or formal certification is claimed.
The package contains the self-contained paper, bibliography, required source dependencies, exact test receipt, historical comparison notes and provenance inventory. The current manuscript is canonical here. The private research repository remains private; all files needed by the documented reproduction command are included.
python src/check_sector_norm_sampling.py
python tools/check_package.py
tectonic --keep-logs manuscript/main.texThe first command regenerates the evidence receipt, including machine-dependent timings. Follow REPRODUCING.md for clean-checkout verification without overwriting the frozen receipt.
Cite: Daniel Fredriksen, Classical Simulation of Two-Layer Quantum Circuits via Output-Dependent Cubic Structure, version 0.1.0, Zenodo, 2026, doi:10.5281/zenodo.23754698. CITATION.cff contains the preferred paper citation.
The publication sequence uses a PDF-first Zenodo preprint record for the paper. GitHub's automatic Zenodo archive is its separately identified source/software companion. The independently archived source/software companion has concept DOI 10.5281/zenodo.23754674. The Lean plan starts only after those gates.
The manuscript, bibliography, prose and evidence are CC BY 4.0; code in src/ and tools/, and build/check configuration, is Apache 2.0. See LICENSE, NOTICE, SOURCES.md, INTEGRITY.md and PROVENANCE.json.
At Lean source commit 85e375a, the source Walsh sum is proved equal to its generated interleaved-coordinate pair-phase representation with transformed character; the dedicated Google Cloud integrated build and exact axiom audit pass (evidence). This extends the helper formalization but does not certify a labeled paper theorem or establish closed-form Gaussian evaluation, normalization, boundedness, or costs. The first published paper and DOI remain unchanged.
At Lean source commit f4094e5, Lean also evaluates the explicit interleaved pair-phase sum when its character is expressed in canonical pair/radical coordinates, by reducing it to the existing canonicalCharacterWalshSum_closed theorem. The exact Lean source archive passes the integrated 2,175-job build and exact helper axiom audit (hash-verified evidence). The bridge from the recorded transformed wire character to those canonical coordinates, the normalized sector identity and all seven labeled paper theorem proofs remain open.
At Lean source commit 4dc88e3, canonicalBlockOfInterleaved is proved equal to the coordinate reindexing induced by interleavedIndexFromCanonical, and re-interleaving a canonical vector is proved to be the inverse coordinate reindexing. The exact source archive passes the dedicated Google Cloud 2,175-job build and integrated exact axiom checker; hash-verified evidence records the run. The declarations use propext and Quot.sound. The recorded transformed wire-character bridge, closed-form source composition, normalization, boundedness, costs and every labeled paper theorem remain open.
At Lean source commit 420ac47, an arbitrary interleaved wire character is converted to canonical pair/radical coefficients through the layout permutation, and the corresponding interleaved Walsh sum is evaluated in closed form. The exact source archive passes the dedicated Google Cloud 2,175-job build and integrated axiom checker; hash-verified evidence records the run. The source-specific composition, normalization, boundedness, costs and every labeled paper theorem remain open.
At Lean source commit 5852639, the recorded coordinate order is proved to split into paired coordinates and residual coordinates whose total dimension is the source dimension. The exact archive passes the dedicated Google Cloud 2,175-job build and integrated audit; hash-verified evidence records the run. Package CI is green. This is a structural helper only; the source-specific composition into the closed-form sum, normalization, boundedness, costs and all labeled manuscript theorems remain open.
At Lean source commit fc4bc81, the dimension witness also exposes the equality between the recorded pair count and the fresh pair parameter needed for source composition. The exact archive passes the dedicated Google Cloud 2,175-job build and audit; hash-verified evidence records the replay, and package CI is green. The source-specific composition, normalization, boundedness, costs and all labeled manuscript theorems remain open.
At Lean source commit 6ec77db, two additional helper theorems show that the exact source Walsh magnitude does not depend on which valid recorded-dimension witnesses are chosen, and characterize zero by the induced radical-character support in the generated coordinates. The dedicated Google Cloud full build (2,175 jobs), integrated audit and expected-axiom checker pass; hash-verified evidence records the run. This still does not prove the paper's affine support/rank characterization, normalized sector identity, matched-sector bound, source costs, or any of the seven labeled paper theorem claims.
At Lean source commit 9aaec54, the source-Walsh zero test is restated as an existential over individual residual coordinates of the transported character. The exact source archive passes the dedicated Google Cloud 2,175-job build, integrated audit and exact checker; hash-verified evidence records the run. This gives the coordinatewise constraints for the still-open affine support/rank characterization; no labeled paper theorem is certified.
At Lean source commit 901b1ff, nonzero source-Walsh support is proved equivalent to the simultaneous vanishing of all residual transformed-character coordinates. The exact archive passes the dedicated Google Cloud full build (2,175 jobs), integrated audit and exact expected-axiom checker; hash-verified evidence records the run. The affine image/rank identification, normalized sector identity, boundedness, costs and all seven labeled paper theorem proofs remain open.
At Lean source/audit commit d52fcb7, the generated residual-coordinate vector is decomposed into a fixed offset XOR a linear map of the wire character. The source Walsh support is proved to be the fiber where that linear component equals the offset. The exact GCP archive passes the 2,175-job build, integrated audit and exact axiom checker; hash-verified evidence records the run. Identifying the kernel with im(Bq), proving rank/nonemptiness, and establishing normalization, boundedness, costs and labeled paper theorems remain open.
At Lean source/audit commit 6ca49ab, the residual-character component is proved linear: it preserves XOR and maps zero to zero. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The kernel/image/rank equality with the source polar form and support origin remain open.
At Lean source/audit commit 1f1bf47, the residual-character projection is proved surjective for the matrix the construction actually generates: an injective square binary matrix action is inverted by its Gaussian row program, binary transpose duality turns that into transpose surjectivity, and the polar-elimination transpose instantiates the residual result. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The coordinate map is still assumed bijective, and the kernel/image/rank equality with the source polar form, support origin, normalization, boundedness, costs and all seven labeled paper theorems remain open.
At Lean source/audit commit f163981, the coordinate-map hypothesis assumed by every previous residual result is discharged: polar elimination records distinct, pairwise disjoint endpoint pairs, so the recorded coordinate order is a permutation and the recorded coordinate map is bijective. Residual projection surjectivity therefore holds for the actual source construction, and combining it with the affine residual-equation characterization proves that the exact source Walsh support is nonempty, with no coordinate, matrix or dimension hypothesis in the statement. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The kernel is still not identified with the source quadratic polar image, so polar rank, support fiber dimension, normalization, boundedness, costs and all seven labeled paper theorems remain open.
At Lean source/audit commit 9408aca, the residual kernel is described explicitly and the support is proved to be one of its cosets. Each residual coordinate is one source coordinate of the transformed character at a recorded radical index, the layout permutation is the identity on the radical block, the kernel is the solution set of that many explicit coordinate equations, and two characters share a residual image exactly when their difference is in the kernel. Transported to the exact source sum, this makes the Walsh support a coset: given one wire character with nonzero sum, another has nonzero sum exactly when the difference lies in the kernel. With the previously certified nonemptiness the support is therefore a nonempty coset of an explicitly described kernel. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The kernel is still not identified with the source quadratic polar image, so the paper Walsh lemma, polar rank, support dimension, normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit 503cc56, one inclusion of the kernel identification is proved. The radical indices are identified with the unpaired indices of the polar elimination, the polar functional is represented by its coordinate vector under Walsh pairing, a transpose coordinate is the character paired against the matching column, and the recorded pair form vanishes against any unpaired coordinate unit for every first argument. Combining these with surjectivity of the elimination matrix shows every source polar vector is annihilated by the residual projection: the image of the source quadratic polar form is contained in the kernel cutting out the exact source Walsh support. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The reverse inclusion is not proved, so the kernel is not yet identified with the polar image and the polar rank, support dimension, normalization, boundedness, costs and all seven labeled paper theorems remain open.
At Lean source/audit commit 7528be5, the pair-form coordinate algebra needed for the converse inclusion is certified: the recorded pair form is additive in its second argument and represented by its coordinate vector, it reads the partner coordinate at either endpoint of a recorded pair for an arbitrary first argument, and an explicit partner vector inverts those values while vanishing off the pairs. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The converse inclusion is not assembled from these parts here, so the kernel is still not identified with the polar image and the polar rank, support dimension, normalization, boundedness, costs and all seven labeled paper theorems remain open.
At Lean source/audit commit 3171dd6, the kernel identification is complete: every unpaired index is a radical index, the partner vector inverts the pair form on the paired block, and the kernel of the residual projection is therefore proved to be exactly the image of the source quadratic polar form. Transported to the exact source sum, the Walsh support is a coset of that image, and with the certified nonemptiness it is exactly such a coset. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. In the manuscript Walsh lemma this is the clause identifying the support as the affine space l_0 + im B_q. That lemma is still not certified: polar rank evenness, the support dimension, the normalized magnitude, the quadratic sign on the support and computability by binary elimination are unproved, and the correspondence between the formalized source Walsh sum and the paper transform of the output-dependent quadratic is not established. All seven labeled paper theorems remain open.
At Lean source/audit commit a4e0173, the residual kernel is parametrized and its free coordinates counted. Kernel membership is exactly vanishing of the transformed character on the unpaired block, every assignment vanishing there is realized by a unique kernel element, the unpaired block is proved to have the residual dimension, and the paired block that parametrizes the kernel therefore has twice the recorded pair count many coordinates, an even number. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. This count is of free coordinates in an explicit bijective parametrization stated through the recorded pair list, not a linear-algebraic rank of the paper polar form, since binary vectors here carry no module or dimension structure; the paper rank-evenness and support-dimension clauses are therefore not certified. The normalized magnitude, the quadratic sign on the support, binary-elimination computability, the bridge from the formalized source Walsh sum to the paper transform, normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit c93b120, the paired block is enumerated and the kernel dimension bound is pinned. Recorded positions below twice the pair count carry pair endpoints, such an endpoint is never unpaired, every coordinate index is one or the other, and consequently two residual kernel elements whose transformed characters agree on every pair endpoint are equal. With the parametrization at a4e0173 this says the kernel is determined by and freely assignable on the paired block. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The free block is enumerated by recorded positions and sized through the recorded pair list, not computed as a rank of the paper polar form, so the paper rank-evenness and support-dimension clauses remain uncertified; the chosen cardinality bridge is not yet built. The normalized magnitude, the quadratic sign, binary-elimination computability, the source-Walsh-to-paper-transform bridge, normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit 13348ec, the kernel paired-block bijection is closed. The paired coordinates are enumerated injectively by recorded position, those positions avoid the unpaired block, and an explicit extension carries any paired-block assignment to a character that takes the assigned values there and vanishes off the pairs. Every paired-block assignment is therefore realized by a unique residual kernel element, so the source polar image is in bijective correspondence with assignments on a block of twice the recorded pair count many coordinates. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The paper rank-evenness and support-dimension clauses remain uncertified: the bijection is with an index block sized through the recorded pair list, the paper rank is that of the bilinear polar form, and binary vectors here carry no module or rank structure, so tying the two is an unbuilt statement bridge. The normalized magnitude, the quadratic sign, binary-elimination computability, the source-Walsh-to-paper-transform bridge, normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit bc2b0ac, the kernel paired-block correspondence is restated as a single bijection: the map sending a residual kernel element to the values of its transformed character on the paired block is bijective onto assignments on that block, with injectivity and surjectivity supplied by the earlier determination and extension results. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. This is packaging for composition, not new mathematics. The paper rank-evenness and support-dimension clauses stay uncertified, and the open modelling decision behind that, together with why its two routes assert different things, is now recorded in the semantic contract. The normalized magnitude, the quadratic sign, binary-elimination computability, the source-Walsh-to-paper-transform bridge, normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit d49f040, the exact magnitude of nonzero source Walsh values is proved: it is two to the power of the dimension less the recorded polar-elimination pair count, obtained by restricting the already-certified canonical magnitude identity to the support. Dividing by two to the dimension gives two to the minus half the paired block size, the shape of the manuscript magnitude clause. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The clause is not certified: the exponent here is the recorded pair count while the paper uses half the polar form rank, and those agree only once the rank is identified with twice the pair count, which is the open modelling decision recorded in the semantic contract. The quadratic sign, binary-elimination computability, the source-Walsh-to-paper-transform bridge, normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit e524527, the exact value and sign structure on the support are proved: a nonzero exact source Walsh coefficient is two to the dimension less the recorded pair count times a sign determined by the recorded constant and the hyperbolic signature of the paired coordinates, and that signature is the parity of products of paired coordinates, hence quadratic in them. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The paper quadratic-sign clause is not certified: quadraticity is exhibited in the recorded interleaved coordinates, not in the paper own support parametrization, and that coordinate bridge is unbuilt. The magnitude, rank-evenness and support-dimension clauses remain blocked on the rank identification in the semantic contract; binary-elimination computability, the source-Walsh-to-paper-transform bridge, normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit f932679, residual kernel preimages are computed rather than merely shown to exist. An executable inverse runs the CNOT sequence of a matrix Gaussian row program, is proved a right inverse of any injective binary matrix action, instantiates at the polar-elimination transpose, and exhibits the kernel element realizing a paired-block target as its value. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The paper computability clause is not certified: it covers the support, its origin and the sign, and only kernel preimages are computed here. The support origin still routes through a coordinate inverse obtained from a surjectivity proof rather than computed, and the sign is not packaged as a computation. The magnitude, rank-evenness and support-dimension clauses remain blocked on the rank identification in the semantic contract and the sign clause on the support-coordinate bridge; the source-Walsh-to-paper-transform bridge, normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit 4aa343d, the inverse of the recorded coordinate permutation is computed by position lookup in the recorded coordinate order, with both round trips and the reindexing cancellation proved. This removes the noncomputable step the support-origin construction had routed through, since the only previously available inverse came from a surjectivity proof. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The paper computability clause is still not certified: the ingredients for a computed support origin are now in place but the origin is not assembled, and the sign is not yet packaged as a checked computation. The magnitude, rank-evenness and support-dimension clauses remain blocked on the rank identification in the semantic contract and the sign clause on the support-coordinate bridge; the source-Walsh-to-paper-transform bridge, normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit 038f5dc, residual preimages and the support sign are computed. The preimage is assembled from the canonical radical placement, the interleaved layout, the computed coordinate inverse and the executable Gaussian inverse, and is proved to project onto the given residual target; the sign is packaged as a named function and the exact coefficient value restated through it. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The paper computability clause is still not certified: these computations are not attached to the manuscript own support objects, since the source-Walsh-to-paper-transform correspondence is unbuilt, and no bit-cost bound is proved. The magnitude, rank-evenness and support-dimension clauses remain blocked on the rank identification in the semantic contract and the sign clause on the support-coordinate bridge; normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit baf371d, the formalized source Walsh sum is tied to a difference transform: for a degree-at-most-three phase and any displacement, the computed degree-at-most-two derivative ANF exists and its source Walsh sum is the signed sum of the phase difference against the character. The earlier support, magnitude and sign results are therefore about the Walsh transform of a first difference of the source phase. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. This is the shape of the correspondence, not the correspondence with the manuscript transform: the displacement is not yet fixed from the circuit and the normalization convention is unchecked, so the computability clause subject is still not the computed object. The magnitude, rank-evenness and support-dimension clauses remain blocked on the rank identification in the semantic contract, the sign clause on the support-coordinate bridge, and no bit-cost bound is proved; normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit b839295, the transform correspondence is composed with the circuit. For a cubic descriptor with surjective pairing, the construction produces the displacement solving the pairing against the output unit and a degree-at-most-two quadratic whose formalized source Walsh sum is the signed sum of the second-layer phase difference along that displacement against the character, so the certified support, magnitude and sign results concern the Walsh transform of the manuscript own output-dependent quadratic. The normalized magnitude is also stated multiplicatively, needing no rationals. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The paper Walsh lemma is still uncertified: rank-evenness, support-dimension and magnitude rest on the open rank identification in the semantic contract, the sign clause on the support-coordinate bridge, and computability on an unproved bit-cost bound. Normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit 6e62752, coordinates on the exact source Walsh support are fixed. The residual kernel element for a paired-block assignment is computed, and given any support point the translate of each such element again lies in the support while every support point differs from it by a kernel element, so the support is a translate of an explicitly parametrized space with the paired-block assignments as coordinates. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. This supplies the prerequisite for the support-coordinate bridge but does not express the sign in those coordinates, so the paper quadratic-sign clause stays uncertified; the rank-evenness, support-dimension and magnitude clauses remain blocked on the rank identification in the semantic contract and computability on an unproved bit-cost bound. Normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit 4b08afc, the support sign is expressed as an explicit quadratic form: the recorded constant xored with the parity of the products of the canonical left and right coordinates of the transformed character. The pair analogue of the all-false coefficient law and the signature evaluation, which depends on no axioms, supply it. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The paper quadratic-sign clause is still not certified: the form is in the canonical coordinates while the support parametrization is by paired-block assignments, and the composition between them is unproved, while the paper states quadraticity against its own support basis matrix which needs the rank identification in the semantic contract. The rank-evenness, support-dimension and magnitude clauses remain blocked on that identification and computability on an unproved bit-cost bound; normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit 9e529c9, the canonical coordinate map composing the recorded reindexing, dimension cast and interleaved layout is proved linear in the character, as are its left and right blocks, so shifting the character shifts its paired coordinates additively. This is the algebraic input for expressing the sign in the support coordinates: the sign is a parity of products of canonical coordinates and support points are a fixed point shifted by a computed kernel element, so linearity splits the form into a base part and the perturbation. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The paper sign clause is still uncertified: evaluating a computed kernel element canonical blocks in terms of its paired-block assignment remains, and comparison against the paper own support basis needs the rank identification in the semantic contract. Rank-evenness, support-dimension, magnitude, computability costs, normalization, boundedness and all seven labeled theorems remain open.
At Lean source/audit commit 10cacb9, the formalization side of the sign clause is complete. The interleaved layout is computed on the canonical left and right block indices, giving twice the pair index and twice it plus one, and the canonical coordinates of an extended paired-block assignment are shown to return that assignment at the even and odd positions of each pair. With the certified sign form and the canonical linearity, the sign on the support is a constant plus a sum of products of affine functions of the support coordinates, hence quadratic in them. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The paper sign clause is still not certified: quadraticity holds in the formalization own support coordinates, while the paper states it against its own support basis matrix, and relating them needs the rank identification in the semantic contract, which also gates rank-evenness, support-dimension and magnitude. Computability costs, normalization, boundedness and all seven labeled theorems remain open.
At Lean source/audit commit 88d2260, the first cost statement for a computed object is certified: each row operation expands to at most three CNOT records, a row program to at most three times its operation count, and the inverse that binary elimination runs therefore uses at most three times the dimension times the dimension plus one many gates. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. This is an operation count in the style of the existing elimination cost bounds, not the bit-cost trace the paper computability clause needs: the semantic contract requires bit operations across parsing, elimination, substitution, enumeration, random draws, Gauss sums, arithmetic, accumulation and rounding, and the support, origin and sign computations remain unbounded. The rank-evenness, support-dimension, magnitude and quadratic-sign clauses remain blocked on the rank identification; normalization, boundedness, costs and all seven labeled theorems remain open.
At Lean source/audit commit ad6ea01, the arithmetic step of the growing family displayed probability bound is certified: the scaled integer inequality behind the value being strictly below one quarter, for every dimension at least one. The exact dedicated-GCP 2,175-job build, integrated audit and expected-axiom checker pass; hash-verified evidence records the run. The scope is narrow by design: it does not identify the family output probability with that value, which is the substance of the proposition and needs the output-probability semantics, the family construction, its support and rank claims and its control count. This is the only declaration touching that proposition and it touches only the final inequality of its proof. Every labeled paper theorem remains uncertified.
At Lean source/audit commit 148d800, the polar rank is identified as a theorem rather than a definitional stance: the polar image is counted through the existing bijection onto the paired block as two to the power of twice the pair count, binary vectors are transported to Fin n -> ZMod 2, the polar form becomes a linear map there with that same image as its range, and Mathlib finite-field submodule cardinality converts the count into a module rank equal to twice the recorded pair count, with rank evenness as a corollary. The exact dedicated-GCP 2,238-job build, integrated audit and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-148d800-20261031/. This is the statement bridge the Walsh lemma rank evenness, support dimension, magnitude and sign clauses were waiting on, but those clauses are not yet restated through it, the computability cost trace is still unbuilt, and no published theorem is certified.
At Lean source/audit commit d31393f, the four rank-dependent clauses of the Walsh lemma are restated through the proved polar rank: polarRank_even_nat for rank evenness, sourceWalshSupport_card_eq_two_pow_rank for the support dimension two to the rank, sourceWalshSum_support_natAbs_rank for the magnitude two to the dimension less rank over two, and sourceWalshSupportSign_quadratic_rank for the quadratic sign with rank-over-two coordinate pairs. The exact dedicated-GCP 2,239-job build, integrated audit and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-d31393f-20261031/. These are statement restatements assembled from already kernel-checked results plus the rank identification: the formalization still does not connect its paired-block coordinates to the paper own support basis matrix, the computability cost trace is unbuilt, and no published theorem is certified.
At Lean source/audit commit 1644a52, the exact source Walsh support is parametrized by the manuscript's r coordinates: supportCoordinateEquiv gives an equivalence from the support to the recorded paired block, sourceWalshSum_support_iff_coordinates makes the support exactly the image of that parametrization, and sourceWalshSum_supportPoint_natAbs restates the magnitude clause on it. The exact dedicated-GCP 2,240-job build, integrated audit and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-1644a52-20261031/. This is the support and magnitude half of the coordinate bridge: those coordinates are not yet presented as the columns of the manuscript basis matrix D, the quadratic sign is not yet expressed in them, the computability cost trace is unbuilt, and no published theorem is certified.
At Lean source/audit commit 2768e2c, the polar image is presented with the manuscript's basis columns, annihilator and right inverse: kernelCoordinateElement and supportBasisColumn give the coordinate elements and columns, supportBasisColumns_span_polarImage proves they are exactly the kernel of residualAnnihilator, and residualRightInverse_spec proves the computed preimage is a right inverse of it. The keystone transpose_eq_pairedBlockExtend_of_kernel shows that on the transformed character a kernel element is exactly the paired-block extension of its coordinates. The exact dedicated-GCP 2,241-job build, integrated audit and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-2768e2c-20261031/. The manuscript basis matrix D is still not defined in the formalization, the quadratic sign is not expressed in these coordinates, the computability cost trace is unbuilt, and no published theorem is certified.
At Lean source/audit commit 4e062fd, the support sign is a function of the coordinate tuple: sourceWalshSupportSign_coordinates proves that for the polar-elimination matrix as pairing matrix and a support character l0 xor kernelCoordinateElement y, the sign equals the recorded constant xored with the parity over coordinate pairs of (alpha_i xor y(2i)) && (beta_i xor y(2i+1)), with alpha and beta the canonical coordinates of the affine base. The proof composes transpose_kernelCoordinateElement with the linearity of the canonical coordinate map and the paired-block coordinate lemmas. The exact dedicated-GCP 2,242-job build, integrated audit and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-4e062fd-20261031/. The manuscript basis matrix D is still not an object in the formalization, the computability cost trace is unbuilt, and no published theorem is certified.
At Lean source/audit commit 7066a44, the manuscript basis matrix is an explicit object: supportBasisMatrix is an n-by-n binary matrix whose first 2 * pairCount columns are the polar-image basis columns and whose remaining columns are zero, extendCoordinates is the padded tuple it acts on, matrixApply_eq_vectorFoldlXor proves matrix application is the fold of the columns, and supportBasisMatrix_column identifies each column with the corresponding basis column. The exact dedicated-GCP 2,243-job build, integrated audit and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-7066a44-20261031/. The action identity — that the matrix applied to the padded tuple returns the coordinate element — is not proved: it needs a Boolean fold-distribution lemma over the nested column fold. So the matrix exists and its columns are identified, but the support is not yet an affine image statement in matrix form; the computability cost trace is still absent and no published theorem is certified.
At Lean source/audit commit 8b20376, the matrix action identity closes. Reassociating the summand pointwise with Bool.and_assoc before distributing lets the constant tuple entry factor out of the inner sum, and �ooleanListSum_swap then swaps the double sum; matrixApply_supportBasisMatrix_extend proves the basis matrix applied to the padded tuple returns kernelCoordinateElement y. Two consequences follow: supportBasisMatrix_extend_annihilated proves the annihilator kills that image, and sourceWalshSum_support_matrix proves the exact support is the affine image of the matrix, the matrix form of l0 + im(D). The exact dedicated-GCP 2,244-job build, integrated audit (820 reports) and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-8b20376-20261031/. This still does not identify the formalization matrix with the paper literal D, carries no matching-offset or sector structure, leaves the computability cost trace unbuilt, and certifies no published theorem.
At Lean source/audit commit 5805957, the bit-operation cost model begins. WalshCost charges three bits per CNOT record, one AND and one XOR per matrix entry, and one AND and one XOR per sign coordinate pair; inverseProgramBitOps_le charges the elimination within its proved gate bound, inverseProgramBitOps_le_poly makes that quadratic, and walshModelledStagesBitOps_le bounds the three modelled stages together by thirteen times the squared dimension plus one. The exact dedicated-GCP 2,245-job build, integrated audit (825 reports) and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-5805957-20261031/. This is three stages of the contract's trace, not the trace: parsing and replay, phase substitution, candidate enumeration, random draws, Gauss sums, integer and rational arithmetic, accumulation, rounding, source size, precision and confidence are all absent, and the per-operation charges are stated modelling choices. No published theorem is certified.
At Lean source/audit commit 26e8098, the cost model covers every stage the semantic contract lists with a CostParameters record tracking source bits, dimension, phase count, cap, precision, confidence and control dimension: parsing and replay, elimination at the proved gate bound, phase substitution, candidate enumeration over 4(q+1)2^(q^2), random draws over 32·4^b·(2h+3), real quadratic Gauss sums, and integer and rational arithmetic, accumulation and rounding. programBitOps_le_eliminationBitOps ties the one refined stage to the charged program, sourceStagesBitOps_le puts the non-exponential stages inside a polynomial envelope scaled by the working precision, and totalBitOps_le is the composed trace bound. The exact dedicated-GCP 2,246-job build, integrated audit (834 reports) and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-26e8098-20261031/. The stage charges are stated modelling choices and only elimination has a proved refinement from an executable program; the paper's displayed bound, the estimator accuracy statements, the identification with the paper literal D and the sector structure remain unproved. No published theorem is certified.
At Lean source/audit commit �89eb22, a second cost stage is refined from an executable computation: evalPhaseCosted carries the phase evaluator value together with the monomial operation count of its fold, oldl_monomialCount proves the count exact, and evalPhaseCosted_ops_le and substitution_refined_bitOps_le place it inside the model substitution charge and the model total. The exact dedicated-GCP 2,247-job build, integrated audit (839 reports) and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-489eb22-20261031/. The count is carried by a counting wrapper around the same fold shape rather than a merged instrumented loop; enumeration, random draws, Gauss sums and rounding remain specifications; the estimator accuracy statement is not proved; and no published theorem is certified.
At Lean source/audit commit e6061ba, the finite-draw probability model begins: a draw variable is a real function on a finite nonempty outcome type, uniformMean is the uniform average, and uniformMean_nonneg, uniformMean_le_one, uniformMean_mem_unit and uniformSecondMoment_le_mean prove the bounded-mean and second-moment facts the variance argument needs. The exact dedicated-GCP 2,248-job build, integrated audit (843 reports) and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-e6061ba-20261031/. The variance identity and the one-quarter bound did not close, so the variance statement is absent; concentration, the median argument, the rounding step and the paper equatorial variable itself are absent, so thm:estimator and lem:moments remain unproved. No published theorem is certified.
At Lean source/audit commit 59fd107, the variance identity and the one-quarter bound close: sum_sq_dev expands the squared deviation inside the finite sum, uniformVariance_eq gives Var = E[X²] − μ², and uniformVariance_le_quarter gives the classical one-quarter bound for a [0,1]-valued draw variable. signedReadout defines Y = 2Z − 1 and uniformMean_signedReadout proves its mean is twice the mean less one. The exact dedicated-GCP 2,248-job build, integrated audit (847 reports) and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-59fd107-20261031/. The paper equatorial draw variable is not defined and its expectation is not proved; concentration, the median argument and rounding are absent, so thm:estimator and lem:moments remain uncovered. No published theorem is certified.
At Lean source/audit commit d309548, Markov concentration is proved on the finite draw model: markov_count gives the counting form and markov_prob the probability form. The exact dedicated-GCP 2,249-job build, integrated audit (849 reports) and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-d309548-20261031/. The paper equatorial draw variable is still not defined — a search of the development finds no sector state, no Clifford observable and no psi, because the matched-sector proposition has no coverage — so its expectation is not proved; Chebyshev on the squared deviation, the median argument and the rounding step are also absent. No published theorem is certified.
At Lean source/audit commit 71328b4, the paper sector state psi_a is defined — the first sector-layer object in the development, where a search had found no sector state, no Clifford observable and no psi. sectorState builds it in exact amplitudes from the support point R a + D y, the first phase, the matrix pairing character J beta and the exact dyadic 2^(-r/2) = 2^(-pairCount); sectorState_eq is the unfolding lemma. The definition was frozen and then independently reviewed twice before any code; both reviews rejected the first draft (sector label type, a spurious matrix application, beta instead of J beta, missing J, incomplete hypotheses) and both approved the corrected form. The exact dedicated-GCP 2,250-job build, integrated audit (851 reports) and expected-axiom checker passed with no sorryAx; evidence is archived in lean/evidence/gcp/sector-71328b4-20261031/. Definition only: the correspondence with the paper object, the observable O_a, the matched vector, the overlap clauses and the estimator statements remain unproved. No published theorem is certified.
At Lean source/audit commit 4e8f07a, the paper sector state is proved to be a unit vector — the first theorem in the sector layer. sectorState_unit_norm sums the squared complex moduli of the exact amplitudes over the coordinate index and gets one, with sectorState_normSq recording the pointwise modulus 2^(-2·pc) and exactComplex_dyadicPow bridging the exact dyadic 2^(-k) to 1/2^k in ℂ. Because the sector rank is r = 2·pc, the paper normalization 2^(-r/2) is a dyadic and no square root is needed. The statement was frozen and independently reviewed twice before any code; both reviews approved with changes, requiring the phase-independence and index-level caveats and predicting the coercion/import failures that did occur. The exact dedicated-GCP 2,251-job build, integrated audit and expected-axiom checker passed on all 856 declarations with no sorryAx; evidence is archived in lean/evidence/gcp/unit-norm-4e8f07a-20261101/. Scope: normalization only — the modulus is phase independent, the object is not identified with the paper own psi_a, and the coordinate map is not proved injective. The observable, matched vector, overlap clauses and estimator statements remain unproved, and no published theorem is certified.
At Lean source/audit commit 5e9600d, the sector support point is proved to be a bijective parametrization, which is the precondition both earlier reviews named. sectorSupportPoint names the point R a + D y; residualAnnihilator_sectorSupportPoint shows the annihilator recovers the sector label from it; supportCoordinates_injective recovers every recorded coordinate from the image; and sectorSupportPoint_bijective makes (a, y) ↦ R a + D y a bijection onto the character space. So the unit-norm theorem is no longer only a statement about a formal index type. The statement was frozen and reviewed twice before any code; both reviews approved with changes (naming, point-not-state injectivity, scope wording) and all were applied. The exact dedicated-GCP 2,252-job build, integrated audit and expected-axiom checker passed on all 865 declarations with no sorryAx; evidence is archived in lean/evidence/gcp/sector-injective-5e9600d-20261101/. Scope: formal labels only — no identification with the manuscript D, C, R or psi_a, no eta-coset claim, and no orthogonality: distinct points are named distinctly, which makes orthogonality statable, not proved. No published theorem is certified.
At Lean source/audit commit 910fac3, sector states at distinct labels are proved orthogonal by disjoint support. The lane had recorded this step as the same-index average ∑_y conj (psi_a y) · psi_a' y = 0; that is false and fails at pc = 0, where the coordinate type is a singleton and the sum is a single nonzero product, and it does not survive a cubic f0 at higher rank either. The manuscript's sectors are orthogonal because they occupy disjoint affine cosets, so the module proves that instead: sectorAmplitude extends the state by zero off its coset, sectorAmplitude_disjoint derives disjointness from the annihilator recovering the label, and sectorStates_orthogonal concludes orthogonality termwise over the character space. The statement was frozen and reviewed twice before any code; both reviews independently confirmed the counterexample and approved the replacement. Exact dedicated-GCP 2,253-job build, audit and expected-axiom checker passed on all 870 declarations with no sorryAx; evidence in lean/evidence/gcp/sector-orthogonal-910fac3-20261101/. Scope: structural — the amplitudes never enter the disjointness argument, so nothing here validates the phase, and the eta offset, observable, matched vector and overlap clauses remain unproved. No published theorem is certified.
At Lean source/audit commit a95804c, the sector state is lifted to the character space where a Fourier factor could act on it, and the character-basis diagonal phase D_f1 is defined. sectorAmplitude_sum_normSq transports the unit-norm sum from the coordinate index to the character space — needed because F_J cannot act on the y-indexed vector — and sectorDiag is D_f1, with helper facts that it preserves support, every squared modulus, the unit norm and disjointness. The statement was frozen and reviewed twice before any code; both reviews required the same narrowing, applied here: the character-space norm is the content, D_f1 is scaffolding, and the preservation facts are helpers because they hold for any unimodular phase. Exact dedicated-GCP 2,254-job build, audit and expected-axiom checker passed on all 881 declarations with no sorryAx; evidence in lean/evidence/gcp/observable-diagonal-a95804c-20261101/. This is not the observable and not its action on a sector state: no Fourier factor, Z_e, eta, 2^(-n/2) normalization, matched-sector identity or overlap clause is proved, the phase is uncertified, and no published theorem is certified.
At Lean source/audit commit 3092e76, the Fourier factor F_J is defined on character-space vectors with the paper normalization (√2/2)^n = 2^(-n/2), and — the point of the increment — it is tied to the certified replay by characterFourier_replay: on a SharedDyadicState it computes exactly what nativePythonFourier_normalized_sum says the replayed native program computes. The operator was genuinely missing, because a SharedDyadicState cannot represent a function that vanishes off a coset and the sector amplitude is exactly such a function. characterFourier_delta_complex gives the paper kernel 2^(-n/2)(-1)^(l·Jc) as a complex corollary. The statement was frozen and reviewed twice before any code; one review rejected the frozen version as an unlinked second transform and required the bridge, the binaryBasis foldr convention and the reframing, all applied. Exact dedicated-GCP 2,255-job build, audit and expected-axiom checker passed on all 888 declarations with no sorryAx; evidence in lean/evidence/gcp/fourier-factor-3092e76-20261101/. Scope: this is the operator and its action on a basis vector — no Fourier-of-Fourier, no unitarity, no Z_e, no eta, no action on a sector state, and the coset Gauss sum is untouched. No published theorem is certified.
At Lean source/audit commit b3f5477, the Fourier factor is reindexed onto the sector coset: characterFourier_sectorAmplitude states that F_J applied to a sector state equals the paper normalization times the signed sector amplitudes summed over the coordinate space, with the sum left unevaluated. The supporting foldr_reindex_of_injective is a hand-built sum-over-the-image lemma, needed because ExactAmplitude carries no additive monoid instance so every sum in the development is a List.foldr over binaryBasis; dropFirst replaces the core List.erase, which needs a BEq instance the vector type lacks. The statement was frozen and reviewed twice before any code; both reviews required the factor be named iterateHadamardScale n exactOne rather than a dyadic that does not exist for odd n, that the result be labelled as naming the sum rather than computing it, and that the quotient-versus-ℂ route decision be recorded. Exact dedicated-GCP 2,256-job build, audit and expected-axiom checker passed on all 897 declarations with no sorryAx; evidence in lean/evidence/gcp/fourier-sector-b3f5477-20261101/. Scope: the reindexing only — no Gauss-sum evaluation, no 2^(r/2) scaling, no neighbouring-coset support, no theta_a, no F_J F_J, no Z_e, no eta, no overlap clause. No published theorem is certified.
At Lean source/audit commit d7d272d, the Pauli Z factor Z_e is defined: characterZ e multiplies the amplitude at computational basis label l by (-1)^(l e), diagonal in the computational basis, with characterZ_apply, exactSigned_involutive and characterZ_involutive. The statement was frozen and reviewed twice before any code, and the reviews cut the increment: the Fourier-on-a-delta norm was dropped as a one-line consequence of characterFourier_delta_complex that does not advance unitarity, the zero-preservation lemma was dropped as the existing exactSigned_zero, and the wire index was corrected from an arbitrary vector to Fin n. Both reviews also established why the recorded F_J F_J half is blocked: it needs general character orthogonality ∑_l (-1)^(l·v) = 2^n [v=0] under a symmetric invertible pairing, which is absent from the development and already listed as an unproved dependency of thm:estimator. Exact dedicated-GCP 2,257-job build, audit and expected-axiom checker passed on all 901 declarations with no sorryAx; evidence in lean/evidence/gcp/ze-definition-d7d272d-20261102/. Scope: one factor of the observable. No Fourier involution, no unitarity, no F_J Z_e F_J, no orthogonality, no Gauss sum, no eta, no overlap clause, and no published theorem certified.