10.33. QuantumBlockEncoding/Robin/T3ResourceComparison.lean
10 explicit public declarations, in source order.
Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven primitive resource exact”; the hypotheses and conclusion in the code panel fix its exact scope.
Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.
Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.
Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.
Declaration kind. theorem.
Source: QuantumBlockEncoding/Robin/T3ResourceComparison.lean:20. A commit-pinned external link is added by the publication build when the source exists at the published ref.
Lean code for Theorem10.33.1●1 theorem
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/Robin/T3ResourceComparison.leancomplete
theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveResource_exact : QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveResource = { oneQubit := 137, cnot := 175, depth := 266 }
theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveResource_exact : QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveResource = { oneQubit := 137, cnot := 175, depth := 266 }
Plain-English reading. Lean checks the proposition indexed as “warm robin xor four slot primitive resource exact”; the hypotheses and conclusion in the code panel fix its exact scope.
Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.
Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.
Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.
Declaration kind. theorem.
Source: QuantumBlockEncoding/Robin/T3ResourceComparison.lean:30. A commit-pinned external link is added by the publication build when the source exists at the published ref.
Lean code for Theorem10.33.2●1 theorem
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/Robin/T3ResourceComparison.leancomplete
theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveResource_exact : QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveResource = { oneQubit := 38, cnot := 68, depth := 96 }
theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveResource_exact : QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveResource = { oneQubit := 38, cnot := 68, depth := 96 }
Plain-English reading. Lean checks the proposition indexed as “warm robin figure 4 primitive resource exact”; the hypotheses and conclusion in the code panel fix its exact scope.
Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.
Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.
Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.
Declaration kind. theorem.
Source: QuantumBlockEncoding/Robin/T3ResourceComparison.lean:40. A commit-pinned external link is added by the publication build when the source exists at the published ref.
Lean code for Theorem10.33.3●1 theorem
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/Robin/T3ResourceComparison.leancomplete
theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveResource_exact : QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveResource = { oneQubit := 427, cnot := 454, depth := 674 }
theorem QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveResource_exact : QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveResource = { oneQubit := 427, cnot := 454, depth := 674 }
Plain-English reading. Lean checks the proposition indexed as “warm robin four slot t 3 cost better than paper seven”; the hypotheses and conclusion in the code panel fix its exact scope. The accepted XOR route uses 106 gates versus the source normal form's 312; the later score fields therefore do not decide this comparison.
Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.
Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.
Technical source note. The accepted XOR route uses 106 gates versus the source normal form's 312; the later score fields therefore do not decide this comparison.
Declaration kind. theorem.
Source: QuantumBlockEncoding/Robin/T3ResourceComparison.lean:52. A commit-pinned external link is added by the publication build when the source exists at the published ref.
Lean code for Theorem10.33.4●1 theorem
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/Robin/T3ResourceComparison.leancomplete
theorem QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_paperSeven : QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.betterThan QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate.cost
theorem QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_paperSeven : QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.betterThan QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate.cost
The accepted XOR route uses 106 gates versus the source normal form's 312; the later score fields therefore do not decide this comparison.
Plain-English reading. Lean checks the proposition indexed as “warm robin four slot t 3 cost better than figure 4”; the hypotheses and conclusion in the code panel fix its exact scope. Under the fixed exact primitive convention, the XOR four-slot route uses 106 gates while the fixed-N8 Figure-4 realization uses 881.
Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.
Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.
Technical source note. Under the fixed exact primitive convention, the XOR four-slot route uses 106 gates while the fixed-N8 Figure-4 realization uses 881. This theorem does not assert optimality outside that declared compiler and score convention.
Declaration kind. theorem.
Source: QuantumBlockEncoding/Robin/T3ResourceComparison.lean:66. A commit-pinned external link is added by the publication build when the source exists at the published ref.
Lean code for Theorem10.33.5●1 theorem
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/Robin/T3ResourceComparison.leancomplete
theorem QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_figure4 : QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.betterThan QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate.cost
theorem QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_figure4 : QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.betterThan QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate.cost
Under the fixed exact primitive convention, the XOR four-slot route uses 106 gates while the fixed-N8 Figure-4 realization uses 881. This theorem does not assert optimality outside that declared compiler and score convention.
Plain-English reading. Lean checks the proposition indexed as “warm robin four slot t 3 cost componentwise paper seven”; the hypotheses and conclusion in the code panel fix its exact scope. The evolved route improves every nonconstant score coordinate against the paper-seven normal form.
Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.
Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.
Technical source note. The evolved route improves every nonconstant score coordinate against the paper-seven normal form. Consequently its winner status does not depend on the chosen ordering of the four displayed coordinates.
Declaration kind. theorem.
Source: QuantumBlockEncoding/Robin/T3ResourceComparison.lean:80. A commit-pinned external link is added by the publication build when the source exists at the published ref.
Lean code for Theorem10.33.6●1 theorem
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/Robin/T3ResourceComparison.leancomplete
theorem QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_componentwise_paperSeven : QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.gateCount < QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate.cost.gateCount ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.depth < QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate.cost.depth ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.auxiliaryQubits < QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate.cost.auxiliaryQubits ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.oracleCalls = QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate.cost.oracleCalls
theorem QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_componentwise_paperSeven : QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.gateCount < QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate.cost.gateCount ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.depth < QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate.cost.depth ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.auxiliaryQubits < QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate.cost.auxiliaryQubits ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.oracleCalls = QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate.cost.oracleCalls
The evolved route improves every nonconstant score coordinate against the paper-seven normal form. Consequently its winner status does not depend on the chosen ordering of the four displayed coordinates.
Plain-English reading. Lean checks the proposition indexed as “warm robin four slot t 3 cost componentwise figure 4”; the hypotheses and conclusion in the code panel fix its exact scope. The same componentwise dominance holds against the fixed-N8 Figure-4 realization.
Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.
Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.
Technical source note. The same componentwise dominance holds against the fixed-N8 Figure-4 realization.
Declaration kind. theorem.
Source: QuantumBlockEncoding/Robin/T3ResourceComparison.lean:94. A commit-pinned external link is added by the publication build when the source exists at the published ref.
Lean code for Theorem10.33.7●1 theorem
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/Robin/T3ResourceComparison.leancomplete
theorem QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_componentwise_figure4 : QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.gateCount < QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate.cost.gateCount ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.depth < QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate.cost.depth ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.auxiliaryQubits < QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate.cost.auxiliaryQubits ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.oracleCalls = QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate.cost.oracleCalls
theorem QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_componentwise_figure4 : QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.gateCount < QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate.cost.gateCount ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.depth < QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate.cost.depth ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.auxiliaryQubits < QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate.cost.auxiliaryQubits ∧ QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.oracleCalls = QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveOperatorCandidate.cost.oracleCalls
The same componentwise dominance holds against the fixed-N8 Figure-4 realization.
Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “warm robin best verified”. The best fully verified Robin candidate under the frozen T3 comparison.
Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.
Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.
Technical source note. The best fully verified Robin candidate under the frozen T3 comparison.
Declaration kind. abbrev.
Source: QuantumBlockEncoding/Robin/T3ResourceComparison.lean:107. A commit-pinned external link is added by the publication build when the source exists at the published ref.
Lean code for Definition10.33.8●1 definition
Associated Lean declarations
-
abbrevdefined in QuantumBlockEncoding/Robin/T3ResourceComparison.leancomplete
abbrev QuantumBlockEncoding.Robin.warmRobinBestVerified : QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℂ 3
abbrev QuantumBlockEncoding.Robin.warmRobinBestVerified : QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℂ 3
The best fully verified Robin candidate under the frozen T3 comparison.
Plain-English reading. This definition gives the library's named construction or computation for “paper level winner certified”. Machine-readable publication guard, enabled only after both source-side same-tier comparisons have compiled.
Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.
Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.
Technical source note. Machine-readable publication guard, enabled only after both source-side same-tier comparisons have compiled.
Declaration kind. def.
Source: QuantumBlockEncoding/Robin/T3ResourceComparison.lean:113. A commit-pinned external link is added by the publication build when the source exists at the published ref.
Lean code for Definition10.33.9●1 definition
Associated Lean declarations
-
defdefined in QuantumBlockEncoding/Robin/T3ResourceComparison.leancomplete
def QuantumBlockEncoding.Robin.paperLevelWinnerCertified : Bool
def QuantumBlockEncoding.Robin.paperLevelWinnerCertified : Bool
Machine-readable publication guard, enabled only after both source-side same-tier comparisons have compiled.
Plain-English reading. Lean checks the proposition indexed as “warm robin publication state consistent”; the hypotheses and conclusion in the code panel fix its exact scope. Publication guard tying the certified fixed-instance winner to empty fixed-N8 source and primitive-obligation lists.
Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.
Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.
Technical source note. Publication guard tying the certified fixed-instance winner to empty fixed-N8 source and primitive-obligation lists.
Declaration kind. theorem.
Source: QuantumBlockEncoding/Robin/T3ResourceComparison.lean:117. A commit-pinned external link is added by the publication build when the source exists at the published ref.
Lean code for Theorem10.33.10●1 theorem
Associated Lean declarations
-
theoremdefined in QuantumBlockEncoding/Robin/T3ResourceComparison.leancomplete
theorem QuantumBlockEncoding.Robin.warmRobinPublicationState_consistent : QuantumBlockEncoding.Robin.paperLevelWinnerCertified = true ∧ QuantumBlockEncoding.Robin.warmRobinFixedN8SourceOpenContracts = [] ∧ QuantumBlockEncoding.Robin.warmRobinFigure4OpenPrimitiveContracts = []
theorem QuantumBlockEncoding.Robin.warmRobinPublicationState_consistent : QuantumBlockEncoding.Robin.paperLevelWinnerCertified = true ∧ QuantumBlockEncoding.Robin.warmRobinFixedN8SourceOpenContracts = [] ∧ QuantumBlockEncoding.Robin.warmRobinFigure4OpenPrimitiveContracts = []
Publication guard tying the certified fixed-instance winner to empty fixed-N8 source and primitive-obligation lists.