Lidar Restricted Anticoncentration Refutation

Abstract

LidarRestrictedAnticoncentrationRefutation describes the forced-twin mechanism for QPU-restricted IQP circuits.

Theorem 1.1 (joint fractional bound).

$$\forall (m:\mathbb{N}),(((F4m).\mathrm{Nonempty})\to (\forall (Z:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))\times ((\mathrm{Fin}(6\cdot m))\to \mathbb{R})\to \mathbb{R}),((\mathrm{Integrable}(\mathrm{fun}w\mapsto \mathrm{Real}.\mathrm{sqrt}(Zw))(\mathrm{joint}m))\to ((\forall G\in F4m,(\int \theta ,\mathrm{Real}.\mathrm{sqrt}(Z(G,\theta ))d\mathrm{uniformAngles}m)\le (47/48:\mathbb{R}{)}^m)\to ((\int w,\mathrm{Real}.\mathrm{sqrt}(Zw)d\mathrm{joint}m)\le (47/48:\mathbb{R}{)}^m)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.joint_fractional_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated joint fractional bound relation for the finite twin-pair calculation.

Theorem 1.2 (factor nonempty).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to ((F4m).\mathrm{Nonempty})))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.factor_nonempty (✓ std3). ∎

Source. Repository-derived.

Commentary.

A four-factor exists: the connector-free factor uses the four internal neighbours of every vertex. The probability law on factors is therefore normalized.

Theorem 1.3 (literal joint probability).

$$\forall (m:\mathbb{N}),([\mathrm{NeZero}m]\to ((1<m)\to (\mathrm{MeasureTheory}.\mathrm{IsProbabilityMeasure}(\mathrm{joint}m))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.literal_joint_probability (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated literal joint probability relation for the finite twin-pair calculation.

Definition 1.4 (claim).

$$\mathrm{claim}⟺\neg \exists ab:\mathbb{R},0<a\wedge 0<b\wedge \forall m:\mathbb{N},3\le m\to \forall s:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool}),b\le \mathrm{tailProbability}mas$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.claim (✓ std3).

Citation. D. A. Lidar (2025). Digital-Analog-Digital Quantum Supremacy. DOI: 10.48550/arXiv.2512.07127. URL: https://arxiv.org/abs/2512.07127v1.

Commentary.

D. A. Lidar, Digital-Analog-Digital Quantum Supremacy, arXiv:2512.07127v1, p. 4, Conjecture 2, verbatim: Let {\mH_n} be a family of hardware graphs as in \cref{def:QPU-R-E}. For each n, draw \mG\sim \mathrm{Unif}[\mF_d(\mH_n)] and \theta\sim \mathrm{Unif}[0,2\pi)^n. For any fixed choice of single-qubit angles {v_i} in \cref{eq:HZ’}, there exist constants a,b>0 (depending only on d) such that for every s\in{0,1}^n, \Pr_{\mG,\theta} \bigl[ P_{\UIQP^{(\theta)}}(s)\ge a 2^{-n} \bigr] \ge b. The definition claim is the NEGATION of this conclusion for the displayed hardware family, d=4, fixed angles pi/7 and n=6m, m>=3. A universal conclusion for every hardware family must hold on this subsequence. The hardware is simple and five-regular, and F4 is nonempty. Thus a theorem of claim refutes the universal source statement. Formulas retain Lean application and binder notation; a centered dot in a constant lambda denotes an anonymous unused binder. Casts display their target types, and products and integrals bind their displayed variables.

Theorem 1.5 (result).

$$\mathrm{claim}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.result (✓ std3). ∎

Resolves. Problems/lidar-2025-qpu-restricted-anticoncentration-refutation (refuted) by D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.result.

Source. Repository-derived.

Acknowledgement. D. A. Lidar (2025). Digital-Analog-Digital Quantum Supremacy. DOI: 10.48550/arXiv.2512.07127. URL: https://arxiv.org/abs/2512.07127v1.

Commentary.

No fixed positive a and b work for the cyclic six-vertex-component family. The forced twin pairs yield a product marginal, and the uniform square-root moment contracts by 47/48 per component. Markov bounds each output tail by inverse sqrt(a) times (47/48)^m. This tends to zero and contradicts a positive uniform lower bound. Conjecture 1 is untouched; the source Theorem 2 remains a conditional statement whose general anticoncentration hypothesis is refuted.

Theorem 1.6 (circuit amplitude literal).

$$\forall (m:\mathbb{N}),(\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (\theta :(\mathrm{Fin}(6\cdot m))\to \mathbb{R}),(\forall (s:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool})),(\mathrm{circuit}G\theta s(\mathrm{fun}\cdot \mapsto \mathrm{false})=\sum z:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool}),(\mathrm{tensorOp}(\mathrm{fun}\cdot :\mathrm{Fin}(6\cdot m)\mapsto \mathrm{hadamard})(\mathrm{fun}i\mapsto \mathrm{if}si\mathrm{then}1\mathrm{else}0)(\mathrm{fun}i\mapsto \mathrm{if}zi\mathrm{then}1\mathrm{else}0))\cdot \mathrm{Complex}.\exp (-\mathrm{Complex}.I\cdot ((\mathrm{HZ}Gz+\sum i,\theta i\cdot D5.S3.\mathrm{QuantumBounds}.\mathrm{MerminMeasurementDependence}.\mathrm{boolSign}(zi)/2:\mathbb{R}):\mathbb{C}))\cdot (\mathrm{tensorOp}(\mathrm{fun}\cdot :\mathrm{Fin}(6\cdot m)\mapsto \mathrm{hadamard})(\mathrm{fun}i\mapsto \mathrm{if}zi\mathrm{then}1\mathrm{else}0)(\mathrm{fun}i\mapsto \mathrm{if}(\mathrm{fun}\cdot \mapsto \mathrm{false})i\mathrm{then}1\mathrm{else}0))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.circuit_amplitude_literal (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated circuit amplitude literal relation for the finite twin-pair calculation.

Definition 1.7 (graphAmplitude).

$$\forall (m:\mathbb{N}),(\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (z:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool})),(\mathrm{graphAmplitude}Gz=(\mathrm{tensorOp}(\mathrm{fun}\cdot :\mathrm{Fin}(6\cdot m)\mapsto \mathrm{hadamard})(\mathrm{fun}i\mapsto \mathrm{if}zi\mathrm{then}1\mathrm{else}0)(\mathrm{fun}i\mapsto \mathrm{if}(\mathrm{fun}\cdot \mapsto \mathrm{false})i\mathrm{then}1\mathrm{else}0))\cdot \prod e\in G,(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{RandomizedGraphNegativityRefutation}.\mathrm{czPhase}(s((0:(\mathrm{Fin}2)),1))(\mathrm{fun}\mathrm{czIndex}\mapsto \mathrm{if}\mathrm{czIndex}=0\mathrm{then}(ze.1)\mathrm{else}(ze.2))))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.graphAmplitude (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines graphAmplitude. Ordered edge pairs retain both orientations off the hardware-factor domain, whereas graphState identifies them.

Definition 1.8 (measurementRow).

$$\forall (m:\mathbb{N}),\forall (s:((\mathrm{Fin}(6\cdot m))\to \mathrm{Bool})),\forall (\phi :((\mathrm{Fin}(6\cdot m))\to \mathbb{R})),\mathrm{measurementRow}s\phi =(((\mathrm{tensorOp}(\mathrm{fun}i\mapsto (\mathrm{hadamard}\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{PrecessionSpinOneSeparableBound}.\mathrm{rotation}1((\phi i)))))(\mathrm{fun}i\mapsto (\mathrm{if}((si))\mathrm{then}1\mathrm{else}0)))\circ (\mathrm{fun}zi\mapsto (\mathrm{if}((zi))\mathrm{then}1\mathrm{else}0)))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.measurementRow (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines measurementRow.

Theorem 1.9 (factor output graph probability).

$$\forall (m:\mathbb{N}),(\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),((G\in F4m)\to (\forall (\theta :(\mathrm{Fin}(6\cdot m))\to \mathbb{R}),(\forall (s:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool})),(\mathrm{outputProbability}G\theta s=\mathrm{Complex}.\mathrm{normSq}(\sum z:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool}),\mathrm{graphAmplitude}Gz\cdot \mathrm{measurementRow}s(\mathrm{fun}i\mapsto \theta i+2\cdot (\mathrm{Real}.\mathrm{pi}/7))z))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.factor_output_graph_probability (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated factor output graph probability relation for the finite twin-pair calculation.

Theorem 1.10 (W false squared).

$$((\mathrm{hadamard}(\mathrm{if}\mathrm{false}\mathrm{then}1\mathrm{else}0)(\mathrm{if}\mathrm{false}\mathrm{then}1\mathrm{else}0)){)}^2=(1/2:\mathbb{C})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.W_false_squared (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated W false squared relation for the finite twin-pair calculation.

Theorem 1.11 (one qubit effect zero).

$$\forall (\alpha :\mathbb{R}),(\forall (r:\mathrm{Bool}),(\forall (r^{\prime }:\mathrm{Bool}),(((\mathrm{hadamard}(\mathrm{if}\mathrm{false}\mathrm{then}1\mathrm{else}0)(\mathrm{if}r\mathrm{then}1\mathrm{else}0))\cdot \mathrm{Complex}.\exp (-\mathrm{Complex}.I\cdot ((\alpha \cdot D5.S3.\mathrm{QuantumBounds}.\mathrm{MerminMeasurementDependence}.\mathrm{boolSign}r/2:\mathbb{R}):\mathbb{C})))\cdot \mathrm{star}((\mathrm{hadamard}(\mathrm{if}\mathrm{false}\mathrm{then}1\mathrm{else}0)(\mathrm{if}{r}^{\prime }\mathrm{then}1\mathrm{else}0))\cdot \mathrm{Complex}.\exp (-\mathrm{Complex}.I\cdot ((\alpha \cdot D5.S3.\mathrm{QuantumBounds}.\mathrm{MerminMeasurementDependence}.\mathrm{boolSign}{r}^{\prime }/2:\mathbb{R}):\mathbb{C})))=\mathrm{effect}\alpha r^{\prime }r)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.one_qubit_effect_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated one qubit effect zero relation for the finite twin-pair calculation.

Theorem 1.12 (graph probability effect zero).

$$\forall (m:\mathbb{N}),(\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (\phi :(\mathrm{Fin}(6\cdot m))\to \mathbb{R}),((\mathrm{Complex}.\mathrm{normSq}(\sum z:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool}),\mathrm{graphAmplitude}Gz\cdot \mathrm{measurementRow}(\mathrm{fun}\cdot \mapsto \mathrm{false})\phi z):\mathbb{C})=\sum z:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool}),\sum z^{\prime }:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool}),\mathrm{graphAmplitude}Gz\cdot \mathrm{star}(\mathrm{graphAmplitude}G{z}^{\prime })\cdot \prod i,\mathrm{effect}(\phi i)(z^{\prime }i)(zi))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.graph_probability_effect_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated graph probability effect zero relation for the finite twin-pair calculation.

Definition 1.13 (densityProbability).

$$\forall (A:\mathrm{Type}),[\mathrm{Fintype}A]\to \forall (k:\mathbb{N}),\forall (\rho :(\mathrm{Matrix}(A\times ((\mathrm{Fin}k)\to \mathrm{Bool}))(A\times ((\mathrm{Fin}k)\to \mathrm{Bool}))\mathbb{C})),\forall (E:(A\to (A\to \mathbb{C}))),\forall (\alpha :((\mathrm{Fin}k)\to \mathbb{R})),\mathrm{densityProbability}k\rho E\alpha =(\mathrm{Matrix}.\mathrm{trace}(\rho \cdot (\mathrm{Matrix}.\mathrm{kronecker}((\mathrm{Matrix}.\mathrm{of}E).\mathrm{transpose})((\mathrm{tensorOp}(\mathrm{fun}i\mapsto (\mathrm{Matrix}.\mathrm{vecMulVec}(\mathrm{fun}(r:(\mathrm{Fin}2))\mapsto (\mathrm{star}((\mathrm{hadamard}\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{PrecessionSpinOneSeparableBound}.\mathrm{rotation}1((\alpha i)))0r)))(\mathrm{star}(\mathrm{fun}(r:(\mathrm{Fin}2))\mapsto (\mathrm{star}((\mathrm{hadamard}\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{PrecessionSpinOneSeparableBound}.\mathrm{rotation}1((\alpha i)))0r))))))).\mathrm{submatrix}(\mathrm{fun}(z:((\mathrm{Fin}k)\to \mathrm{Bool}))\mapsto (\mathrm{fun}i\mapsto (\mathrm{if}((zi))\mathrm{then}1\mathrm{else}0)))(\mathrm{fun}(z:((\mathrm{Fin}k)\to \mathrm{Bool}))\mapsto (\mathrm{fun}i\mapsto (\mathrm{if}((zi))\mathrm{then}1\mathrm{else}0)))))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.densityProbability (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines densityProbability.

Definition 1.14 (complementEquiv).

$$\forall (m:\mathbb{N}),(\mathrm{complementEquiv}m=((\mathrm{finProdFinEquiv}.\mathrm{trans}(\mathrm{finCongr}(\mathrm{Nat}.{\mathrm{mul}}_{\mathrm{comm}}m4))).\mathrm{symm}.\mathrm{arrowCongr}(\mathrm{Equiv}.\mathrm{refl}\mathrm{Bool})).\mathrm{trans}(\mathrm{Equiv}.\mathrm{curry}(\mathrm{Fin}m)(\mathrm{Fin}4)\mathrm{Bool}))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.complementEquiv (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines complementEquiv.

Definition 1.15 (reindexedTwinAmplitude).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to \mathrm{Fin}4\to \mathrm{Bool})\to \mathrm{Bool}),(\forall (\mathrm{xz}:(\mathrm{Fin}m\to \mathrm{Bool}\times \mathrm{Bool})\times (\mathrm{Fin}(4\cdot m)\to \mathrm{Bool})),(\mathrm{reindexedTwinAmplitude}m\mathrm{qC}\mathrm{xz}=\mathrm{twinAmplitude}m\mathrm{qC}(\mathrm{xz}.1,\mathrm{complementEquiv}m\mathrm{xz}.2))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.reindexedTwinAmplitude (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines reindexedTwinAmplitude.

Theorem 1.16 (reindexed twin marginal).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to \mathrm{Fin}4\to \mathrm{Bool})\to \mathrm{Bool}),(\forall (x:\mathrm{Fin}m\to \mathrm{Bool}\times \mathrm{Bool}),(\forall (x^{\prime }:\mathrm{Fin}m\to \mathrm{Bool}\times \mathrm{Bool}),(D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceRight}(\mathrm{Matrix}.\mathrm{vecMulVec}(\mathrm{reindexedTwinAmplitude}m\mathrm{qC})(\mathrm{star}(\mathrm{reindexedTwinAmplitude}m\mathrm{qC})))x{x}^{\prime }=\prod i,\mathrm{pairDensity}(xi)(x^{\prime }i)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.reindexed_twin_marginal (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated reindexed twin marginal relation for the finite twin-pair calculation.

Definition 1.17 (retainedEffect).

$$\forall (m:\mathbb{N}),\forall (\phi :(\mathrm{Fin}m\to (\mathbb{R}\times \mathbb{R}))),\forall (x:(\mathrm{Fin}m\to (\mathrm{Bool}\times \mathrm{Bool}))),\forall (x^{\prime }:(\mathrm{Fin}m\to (\mathrm{Bool}\times \mathrm{Bool}))),\mathrm{retainedEffect}m\phi x{x}^{\prime }=(\mathrm{Matrix}.\mathrm{vecMulVec}(\mathrm{retainedRow}m\phi )(\mathrm{star}(\mathrm{retainedRow}m\phi )))x{x}^{\prime }$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.retainedEffect (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines retainedEffect.

Definition 1.18 (twinDensityProbability).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to \mathrm{Fin}4\to \mathrm{Bool})\to \mathrm{Bool}),(\forall (\phi :\mathrm{Fin}m\to \mathbb{R}\times \mathbb{R}),(\forall (\alpha :\mathrm{Fin}(4\cdot m)\to \mathbb{R}),(\mathrm{twinDensityProbability}m\mathrm{qC}\phi \alpha =\mathrm{densityProbability}(4\cdot m)(\mathrm{Matrix}.\mathrm{vecMulVec}(\mathrm{reindexedTwinAmplitude}m\mathrm{qC})(\mathrm{star}(\mathrm{reindexedTwinAmplitude}m\mathrm{qC})))(\mathrm{retainedEffect}m\phi )\alpha ))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.twinDensityProbability (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines twinDensityProbability.

Definition 1.19 (normalizedTwinDensity).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to \mathrm{Fin}4\to \mathrm{Bool})\to \mathrm{Bool}),(\forall (\phi :\mathrm{Fin}m\to \mathbb{R}\times \mathbb{R}),(\forall (\alpha :\mathrm{Fin}(4\cdot m)\to \mathbb{R}),(\mathrm{normalizedTwinDensity}m\mathrm{qC}\phi \alpha =(2:\mathbb{R}{)}^{6\cdot m}\cdot (\mathrm{twinDensityProbability}m\mathrm{qC}\phi \alpha ).\mathrm{re}))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.normalizedTwinDensity (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines normalizedTwinDensity.

Theorem 1.20 (normalized twin conditional mean).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to \mathrm{Fin}4\to \mathrm{Bool})\to \mathrm{Bool}),(\forall (\phi :\mathrm{Fin}m\to \mathbb{R}\times \mathbb{R}),((\int \alpha ,\mathrm{normalizedTwinDensity}m\mathrm{qC}\phi \alpha d\mathrm{Measure}.\mathrm{pi}(\mathrm{fun}\cdot \mapsto (\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi})))))=\prod i,(1+\mathrm{Real}.\cos (\phi i).1\cdot \mathrm{Real}.\cos (\phi i).2))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.normalized_twin_conditional_mean (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated normalized twin conditional mean relation for the finite twin-pair calculation.

Definition 1.21 (retainedRow).

$$\forall (m:\mathbb{N}),\forall (\phi :((\mathrm{Fin}m)\to (\mathbb{R}\times \mathbb{R}))),\forall (x:((\mathrm{Fin}m)\to (\mathrm{Bool}\times \mathrm{Bool}))),\mathrm{retainedRow}m\phi x=((\mathrm{tensorOp}(\mathrm{fun}(i:(\mathrm{Fin}(m+m)))\mapsto (\mathrm{Sum}.\mathrm{elim}(\mathrm{fun}j\mapsto (\mathrm{hadamard}\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{PrecessionSpinOneSeparableBound}.\mathrm{rotation}1((\phi j).1)))(\mathrm{fun}j\mapsto (\mathrm{hadamard}\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{PrecessionSpinOneSeparableBound}.\mathrm{rotation}1((\phi j).2)))(\mathrm{finSumFinEquiv}.\mathrm{symm}i))))(\mathrm{fun}\cdot \mapsto 0)(\mathrm{fun}i\mapsto (\mathrm{if}((\mathrm{Sum}.\mathrm{elim}(\mathrm{fun}j\mapsto (xj).1)(\mathrm{fun}j\mapsto (xj).2)(\mathrm{finSumFinEquiv}.\mathrm{symm}i)))\mathrm{then}1\mathrm{else}0)))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.retainedRow (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines retainedRow.

Definition 1.22 (twinProbability).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to \mathrm{Fin}4\to \mathrm{Bool})\to \mathrm{Bool}),(\forall (\phi :\mathrm{Fin}m\to \mathbb{R}\times \mathbb{R}),(\forall (\alpha :\mathrm{Fin}(4\cdot m)\to \mathbb{R}),(\mathrm{twinProbability}m\mathrm{qC}\phi \alpha =\mathrm{Complex}.\mathrm{normSq}(\sum x:\mathrm{Fin}m\to \mathrm{Bool}\times \mathrm{Bool},\sum z:\mathrm{Fin}(4\cdot m)\to \mathrm{Bool},\mathrm{reindexedTwinAmplitude}m\mathrm{qC}(x,z)\cdot \mathrm{retainedRow}m\phi x\cdot ((\mathrm{tensorOp}(\mathrm{fun}i\mapsto (\mathrm{hadamard}\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{PrecessionSpinOneSeparableBound}.\mathrm{rotation}1((\alpha i)))))(\mathrm{fun}\cdot \mapsto 0)(\mathrm{fun}i\mapsto (\mathrm{if}((zi))\mathrm{then}1\mathrm{else}0))))))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.twinProbability (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines twinProbability.

Theorem 1.23 (normSq finite sum).

$$\forall (I:\mathrm{Type}),([\mathrm{Fintype}I]\to (\forall (f:I\to \mathbb{C}),((\mathrm{Complex}.\mathrm{normSq}(\sum i,fi):\mathbb{C})=\sum i,\sum j,fi\cdot \mathrm{star}(fj))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.normSq_finite_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated normSq finite sum relation for the finite twin-pair calculation.

Theorem 1.24 (twin probability density).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to \mathrm{Fin}4\to \mathrm{Bool})\to \mathrm{Bool}),(\forall (\phi :\mathrm{Fin}m\to \mathbb{R}\times \mathbb{R}),(\forall (\alpha :\mathrm{Fin}(4\cdot m)\to \mathbb{R}),((\mathrm{twinProbability}m\mathrm{qC}\phi \alpha :\mathbb{C})=\mathrm{twinDensityProbability}m\mathrm{qC}\phi \alpha ))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.twin_probability_density (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated twin probability density relation for the finite twin-pair calculation.

Theorem 1.25 (normalized density nonneg).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to \mathrm{Fin}4\to \mathrm{Bool})\to \mathrm{Bool}),(\forall (\phi :\mathrm{Fin}m\to \mathbb{R}\times \mathbb{R}),(\forall (\alpha :\mathrm{Fin}(4\cdot m)\to \mathbb{R}),(0\le \mathrm{normalizedTwinDensity}m\mathrm{qC}\phi \alpha ))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.normalized_density_nonneg (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated normalized density nonneg relation for the finite twin-pair calculation.

Definition 1.26 (retainedSplit).

$$\forall (m:\mathbb{N}),(\mathrm{retainedSplit}m=(\mathrm{MeasurableEquiv}.\mathrm{sumPiEquivProdPi}(\mathrm{fun}\cdot :\mathrm{Sum}(\mathrm{Fin}m)(\mathrm{Fin}m)\mapsto \mathbb{R})).\mathrm{trans}(\mathrm{MeasurableEquiv}.\mathrm{arrowProdEquivProdArrow}\mathbb{RR}(\mathrm{Fin}m)).\mathrm{symm})$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.retainedSplit (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines retainedSplit. Formulas retain Lean application and binder notation; a centered dot in a constant lambda denotes an anonymous unused binder. Casts display their target types, and products and integrals bind their displayed variables.

Definition 1.27 (angleSplit).

$$\forall (m:\mathbb{N}),(\forall (e:(\mathrm{Sum}(\mathrm{Sum}(\mathrm{Fin}m)(\mathrm{Fin}m))(\mathrm{Fin}(4\cdot m)))\equiv (\mathrm{Fin}(6\cdot m))),(\mathrm{angleSplit}me=(\mathrm{MeasurableEquiv}.\mathrm{piCongrLeft}(\mathrm{fun}\cdot :(\mathrm{Sum}(\mathrm{Sum}(\mathrm{Fin}m)(\mathrm{Fin}m))(\mathrm{Fin}(4\cdot m)))\mapsto \mathbb{R})e.\mathrm{symm}).\mathrm{trans}((\mathrm{MeasurableEquiv}.\mathrm{sumPiEquivProdPi}(\mathrm{fun}\cdot :(\mathrm{Sum}(\mathrm{Sum}(\mathrm{Fin}m)(\mathrm{Fin}m))(\mathrm{Fin}(4\cdot m)))\mapsto \mathbb{R})).\mathrm{trans}((\mathrm{retainedSplit}m).\mathrm{prodCongr}(\mathrm{MeasurableEquiv}.\mathrm{refl}\cdot )))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.angleSplit (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines angleSplit.

Theorem 1.28 (split integral).

$$\forall (m:\mathbb{N}),(\forall (e:(\mathrm{Sum}(\mathrm{Sum}(\mathrm{Fin}m)(\mathrm{Fin}m))(\mathrm{Fin}(4\cdot m)))\equiv (\mathrm{Fin}(6\cdot m))),(\forall (f:((\mathrm{Fin}m\to \mathbb{R}\times \mathbb{R})\times (\mathrm{Fin}(4\cdot m)\to \mathbb{R}))\to \mathbb{R}),((\int \theta ,f(\mathrm{angleSplit}me\theta )d\mathrm{uniformAngles}m)=\int w,fwd((\mathrm{Measure}.\mathrm{pi}\mathrm{fun}\cdot :\mathrm{Fin}m\mapsto \mathrm{pairAngle}).\mathrm{prod}(\mathrm{Measure}.\mathrm{pi}\mathrm{fun}\cdot :\mathrm{Fin}(4\cdot m)\mapsto (\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi}))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.split_integral (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated split integral relation for the finite twin-pair calculation.

Theorem 1.29 (gate entry norm le one).

$$\forall (\alpha :\mathbb{R}),(\forall (b:\mathrm{Bool}),(\Vert ((\mathrm{hadamard}\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{PrecessionSpinOneSeparableBound}.\mathrm{rotation}1(\alpha ))0(\mathrm{if}(b)\mathrm{then}1\mathrm{else}0))\Vert \le 1))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.gate_entry_norm_le_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated gate entry norm le one relation for the finite twin-pair calculation.

Theorem 1.30 (normalizedDensity eq).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to \mathrm{Fin}4\to \mathrm{Bool})\to \mathrm{Bool}),(\forall (\phi :\mathrm{Fin}m\to \mathbb{R}\times \mathbb{R}),(\forall (\alpha :\mathrm{Fin}(4\cdot m)\to \mathbb{R}),(\mathrm{normalizedTwinDensity}m\mathrm{qC}\phi \alpha =(2:\mathbb{R}{)}^{6\cdot m}\cdot \mathrm{twinProbability}m\mathrm{qC}\phi \alpha ))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.normalizedDensity_eq (✓ std3). ∎

Source. Repository-derived.

Commentary.

This statement supplies the indicated normalizedDensity eq relation for the finite twin-pair calculation.

Theorem 1.31 (twin fractional moment).

$$\forall (m:\mathbb{N}),(\forall (\mathrm{qC}:(\mathrm{Fin}m\to \mathrm{Fin}4\to \mathrm{Bool})\to \mathrm{Bool}),((\int w,\mathrm{Real}.\mathrm{sqrt}(\mathrm{normalizedTwinDensity}m\mathrm{qC}w.1w.2)d((\mathrm{Measure}.\mathrm{pi}\mathrm{fun}\cdot :\mathrm{Fin}m\mapsto \mathrm{pairAngle}).\mathrm{prod}(\mathrm{Measure}.\mathrm{pi}\mathrm{fun}\cdot :\mathrm{Fin}(4\cdot m)\mapsto (\mathrm{ProbabilityTheory}.\mathrm{cond}\mathrm{volume}(\mathrm{Set}.\mathrm{Ico}0(2\cdot \mathrm{Real}.\mathrm{pi}))))))\le (47/48:\mathbb{R}{)}^m))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.twin_fractional_moment (✓ std3). ∎

Source. Repository-derived.

Commentary.

The conditional mean is the product of 1+cos(alpha)cos(beta). Conditional Cauchy-Schwarz, the polynomial upper bound on sqrt(1+t), and the independent uniform angles yield contraction by at most 47/48 per pair.

Definition 1.32 (graphProbability).

$$\forall (m:\mathbb{N}),(\forall (G:\mathrm{Finset}((\mathrm{Fin}(6\cdot m)\times \mathrm{Fin}(6\cdot m)))),(\forall (\theta :(\mathrm{Fin}(6\cdot m))\to \mathbb{R}),(\mathrm{graphProbability}G\theta =\mathrm{Complex}.\mathrm{normSq}(\sum z:(\mathrm{Fin}(6\cdot m)\to \mathrm{Bool}),\mathrm{graphAmplitude}Gz\cdot \mathrm{measurementRow}(\mathrm{fun}\cdot \mapsto \mathrm{false})\theta z))))$$

Formalization. D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.graphProbability (✓ std3).

Source. Repository-derived.

Commentary.

The displayed expression defines graphProbability.

Theorem 1.33 (graph sqrt shift).

$$\forall (m:\mathbb{N}),(\forall (G:(\mathrm{Finset}((\mathrm{Fin}(6\cdot m))\times (\mathrm{Fin}(6\cdot m))))),(\forall (d:(\mathrm{Fin}(6\cdot m))\to \mathbb{R}),((\int \theta ,(\mathrm{Real}.\mathrm{sqrt}((2:\mathbb{R}{)}^{6\cdot m}\cdot \mathrm{graphProbability}G(\mathrm{fun}i\mapsto \theta i+di)))d\mathrm{uniformAngles}m)=(\int \theta ,(\mathrm{Real}.\mathrm{sqrt}((2:\mathbb{R}{)}^{6\cdot m}\cdot \mathrm{graphProbability}G\theta ))d\mathrm{uniformAngles}m))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.graph_sqrt_shift (✓ std3). ∎

Source. Repository-derived.

Commentary.

The graph probability is periodic in every angle: its effect-matrix factors are invariant under adding two pi. A finite amplitude bound makes the square-root integrand bounded, so pi_periodic_shift gives invariance of its normalized product-angle integral under arbitrary coordinate shifts.

References

• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.W_false_squared
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.angleSplit
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.circuit_amplitude_literal
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.claim
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.complementEquiv
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.densityProbability
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.factor_nonempty
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.factor_output_graph_probability
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.gate_entry_norm_le_one
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.graphAmplitude
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.graphProbability
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.graph_probability_effect_zero
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.graph_sqrt_shift
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.joint_fractional_bound
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.literal_joint_probability
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.measurementRow
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.normSq_finite_sum
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.normalizedDensity_eq
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.normalizedTwinDensity
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.normalized_density_nonneg
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.normalized_twin_conditional_mean
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.one_qubit_effect_zero
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.reindexedTwinAmplitude
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.reindexed_twin_marginal
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.result
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.retainedEffect
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.retainedRow
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.retainedSplit
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.split_integral
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.twinDensityProbability
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.twinProbability
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.twin_fractional_moment
• Truth anchor: D5/S3/Quantum/Measurements/IQP/LidarRestrictedAnticoncentrationRefutation.twin_probability_density
• Dependency: D5/S3/Quantum/Entanglement/RandomizedGraphNegativityRefutation
• Dependency: D5/S3/Quantum/Measurements/IQP/HardwareCircuitFactors