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.
theorem warmRobinPaperSevenPrimitiveResource_exact :
warmRobinPaperSevenPrimitiveResource = {
oneQubit := 137
cnot := 175
oracleCalls := 0
pureAncilla := 0
depth := 266
} := by
commit-pinned source · Verso Blueprint panel
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.
theorem warmRobinXorFourSlotPrimitiveResource_exact :
warmRobinXorFourSlotPrimitiveResource = {
oneQubit := 38
cnot := 68
oracleCalls := 0
pureAncilla := 0
depth := 96
} := by
commit-pinned source · Verso Blueprint panel
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.
theorem warmRobinFigure4PrimitiveResource_exact :
warmRobinFigure4PrimitiveResource = {
oneQubit := 427
cnot := 454
oracleCalls := 0
pureAncilla := 0
depth := 674
} := by
commit-pinned source · Verso Blueprint panel
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.
theorem warmRobinFourSlotT3Cost_betterThan_paperSeven :
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.betterThan
warmRobinPaperSevenPrimitiveOperatorCandidate.cost := by
commit-pinned source · Verso Blueprint panel
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.
theorem warmRobinFourSlotT3Cost_betterThan_figure4 :
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.betterThan
warmRobinFigure4PrimitiveOperatorCandidate.cost := by
commit-pinned source · Verso Blueprint panel
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.
theorem warmRobinFourSlotT3Cost_componentwise_paperSeven :
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.gateCount <
warmRobinPaperSevenPrimitiveOperatorCandidate.cost.gateCount ∧
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.depth <
warmRobinPaperSevenPrimitiveOperatorCandidate.cost.depth ∧
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.auxiliaryQubits <
warmRobinPaperSevenPrimitiveOperatorCandidate.cost.auxiliaryQubits ∧
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.oracleCalls =
warmRobinPaperSevenPrimitiveOperatorCandidate.cost.oracleCalls := by
commit-pinned source · Verso Blueprint panel
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.
theorem warmRobinFourSlotT3Cost_componentwise_figure4 :
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.gateCount <
warmRobinFigure4PrimitiveOperatorCandidate.cost.gateCount ∧
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.depth <
warmRobinFigure4PrimitiveOperatorCandidate.cost.depth ∧
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.auxiliaryQubits <
warmRobinFigure4PrimitiveOperatorCandidate.cost.auxiliaryQubits ∧
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.oracleCalls =
warmRobinFigure4PrimitiveOperatorCandidate.cost.oracleCalls := by
commit-pinned source · Verso Blueprint panel
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.
noncomputable abbrev warmRobinBestVerified :
VerifiedOperatorBlockEncoding ℂ 3 :=
warmRobinXorFourSlotPrimitiveVerifiedBlockEncoding
/-- Machine-readable publication guard, enabled only after both source-side
same-tier comparisons have compiled. -/
commit-pinned source · Verso Blueprint panel
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.
def paperLevelWinnerCertified : Bool := true
/-- Publication guard tying the certified fixed-instance winner to empty
fixed-N8 source and primitive-obligation lists. -/
commit-pinned source · Verso Blueprint panel
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.
theorem warmRobinPublicationState_consistent :
paperLevelWinnerCertified = true ∧
warmRobinFixedN8SourceOpenContracts = [] ∧
warmRobinFigure4OpenPrimitiveContracts = [] := by
commit-pinned source · Verso Blueprint panel