This type lists the allowed alternatives for “reconstruction protocol”; its constructors are the cases that downstream code must handle. Whether the natural-language reconstruction was produced without seeing the source prose.
inductive ReconstructionProtocol where
| blindLeanOnly
| sourceAssisted
deriving Repr, DecidableEq
/-- ASPBE-specific theorem slots whose meaning must survive formalization. -/
commit-pinned source · Verso Blueprint panel
This type lists the allowed alternatives for “semantic slot”; its constructors are the cases that downstream code must handle. ASPBE-specific theorem slots whose meaning must survive formalization.
inductive SemanticSlot where
| targetObject
| scalarAndDimensions
| quantifiers
| normalization
| ancillaLayout
| registerOrder
| cleanProjection
| exactness
| errorNorm
| oracleAssumptions
commit-pinned source · Verso Blueprint panel
This type lists the allowed alternatives for “fidelity verdict”; its constructors are the cases that downstream code must handle. Slotwise verdict for the complete source-to-Lean-to-text round trip.
inductive FidelityVerdict where
| exactMatch
| equivalentAfterElaboration
| sourceUnderspecified
| leanStrongerAssumptions
| leanWeakerConclusion
| manualReview
deriving Repr, DecidableEq
/-- Review state of a proposed clarification or theorem repair. -/
commit-pinned source · Verso Blueprint panel
This type lists the allowed alternatives for “repair status”; its constructors are the cases that downstream code must handle. Review state of a proposed clarification or theorem repair.
inductive RepairStatus where
| proposed
| needsSourceCheck
| reviewerAccepted
| rejected
deriving Repr, DecidableEq
/-- One explicit semantic discrepancy between the source reading and blind reconstruction. -/
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “semantic delta”. A proposition-valued field is a requirement until a constructor supplies it. One explicit semantic discrepancy between the source reading and blind reconstruction.
structure SemanticDelta where
slot : SemanticSlot
originalReading : String
reconstructedReading : String
consequence : String
deriving Repr, DecidableEq
/-- A non-destructive replacement candidate. It never mutates `RoundTripAudit.originalText`. -/
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “repair proposal”. A proposition-valued field is a requirement until a constructor supplies it. A non-destructive replacement candidate.
structure RepairProposal where
proposedText : String
rationale : String
status : RepairStatus
deriving Repr, DecidableEq
/--
A theorem-fidelity certificate record.
`originalText` is immutable evidence. `reconstructedText` must come from the
Lean declaration and imported definitions under `blindLeanOnly`. Any suggested
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “round trip audit”. A proposition-valued field is a requirement until a constructor supplies it. A theorem-fidelity certificate record.
structure RoundTripAudit where
auditId : String
sourceAnchor : String
originalText : String
leanDeclaration : String
decoderInput : String
reconstructedText : String
protocol : ReconstructionProtocol
reviewerSeparated : Bool
checkedSlots : List SemanticSlot
deltas : List SemanticDelta
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “admissible”. Minimal admission contract for a publishable semantic round-trip record.
def Admissible (audit : RoundTripAudit) : Prop :=
audit.auditId ≠ "" ∧
audit.sourceAnchor ≠ "" ∧
audit.originalText ≠ "" ∧
audit.leanDeclaration ≠ "" ∧
audit.decoderInput ≠ "" ∧
audit.reconstructedText ≠ "" ∧
audit.protocol = .blindLeanOnly ∧
audit.reviewerSeparated = true ∧
audit.checkedSlots ≠ []
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “published statement”. The statement exposed as source evidence remains the original, never an automatic repair.
def publishedStatement (audit : RoundTripAudit) : String :=
audit.originalText
/-- The repair candidate is available separately for human/source review. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “proposed statement”. The repair candidate is available separately for human/source review.
def proposedStatement (audit : RoundTripAudit) : Option String :=
audit.repair.map RepairProposal.proposedText
/-- Mismatches and underspecified statements must enter the independent review queue. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “requires human review”. Mismatches and underspecified statements must enter the independent review queue.
def requiresHumanReview (audit : RoundTripAudit) : Bool :=
match audit.verdict with
| .exactMatch => false
| .equivalentAfterElaboration => false
| .sourceUnderspecified => true
| .leanStrongerAssumptions => true
| .leanWeakerConclusion => true
| .manualReview => true
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “published statement eq original”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem publishedStatement_eq_original (audit : RoundTripAudit) :
audit.publishedStatement = audit.originalText := rfl
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “verified operator block encoding round trip”. **Equivalent after elaboration.** The source contract says that a verified exact operator block encoding consists of a candidate unitary plus proofs of unitarity and clean-block containment.
def verifiedOperatorBlockEncodingRoundTrip : RoundTripAudit where
auditId := "core-exact-operator-block-encoding"
sourceAnchor := "QuantumBlockEncoding/BlockEncoding.lean: VerifiedOperatorBlockEncoding"
originalText := "An exact operator block encoding contains a candidate unitary together with proofs that the candidate is unitary and that its designated clean block contains the target operator."
leanDeclaration := "QuantumBlockEncoding.VerifiedOperatorBlockEncoding"
decoderInput := "The Lean declaration and imported definitions only; the original prose is hidden."
reconstructedText := "For a scalar type and system-qubit count, the record stores an OperatorBlockEncodingCandidate, a proof of candidate.isUnitary, and a proof of candidate.blockContainsTarget. The candidate also fixes the operator target, normalizer, auxiliary-qubit count, register layout, circuit, resource record, and layout-matching equality."
protocol := .blindLeanOnly
reviewerSeparated := true
checkedSlots := [.targetObject, .scalarAndDimensions, .normalization, .ancillaLayout, .registerOrder, .cleanProjection, .exactness, .conclusion, .resourceScope]
deltas := []
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “verified operator block encoding round trip admissible”; the hypotheses and conclusion in the code panel fix its exact scope. The core exact block-encoding round trip satisfies the independent-audit contract.
theorem verifiedOperatorBlockEncodingRoundTrip_admissible :
RoundTripAudit.Admissible verifiedOperatorBlockEncodingRoundTrip := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “approximate block encoding norm round trip”. **Lean conclusion is weaker than the public analytic formula.** The public route states '‖A - α Π U Π†‖ ≤ ε' in a declared norm and register convention.
def approximateBlockEncodingNormRoundTrip : RoundTripAudit where
auditId := "approximate-block-encoding-norm-boundary"
sourceAnchor := "README Route II and QuantumBlockEncoding/BlockEncoding.lean: ApproximateOperatorBlockEncodingCandidate"
originalText := "Construct a larger unitary U satisfying ‖A - α Π U Π†‖ ≤ ε in the declared norm and clean ancilla/register convention."
leanDeclaration := "QuantumBlockEncoding.ApproximateOperatorBlockEncodingCandidate"
decoderInput := "The Lean declaration and imported definitions only; the README formula is hidden."
reconstructedText := "The interface stores an exact-candidate payload, a value epsilon, and a backend-supplied proposition approximationBound. The declaration itself does not fix a norm, define Π, connect approximationBound to A - α Π U Π†, or state the register ordering used by the projection."
protocol := .blindLeanOnly
reviewerSeparated := true
checkedSlots := [.targetObject, .normalization, .ancillaLayout, .registerOrder, .cleanProjection, .exactness, .errorNorm, .conclusion]
deltas := [
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “approximate block encoding norm round trip admissible”; the hypotheses and conclusion in the code panel fix its exact scope. The approximate-interface audit is blind, explicit, and independently review-gated.
theorem approximateBlockEncodingNormRoundTrip_admissible :
RoundTripAudit.Admissible approximateBlockEncodingNormRoundTrip := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “verified state preparation round trip”. **Equivalent after elaboration.** State preparation is reconstructed as a proof that the target is normalized, the candidate matrix is unitary, and its first computational-basis column equals the target amplitudes.
def verifiedStatePreparationRoundTrip : RoundTripAudit where
auditId := "core-exact-state-preparation"
sourceAnchor := "QuantumBlockEncoding/StatePreparation.lean: VerifiedStatePreparation"
originalText := "For a normalized target state |ψ⟩, construct a unitary U satisfying U|0…0⟩ = |ψ⟩."
leanDeclaration := "QuantumBlockEncoding.VerifiedStatePreparation"
decoderInput := "The Lean declaration, FirstColumnMatches, zeroBasisIndex, and imported definitions only; the original prose is hidden."
reconstructedText := "The certificate stores a state-preparation candidate, a proof of target normalization, a proof that the candidate matrix is unitary, and a proof that every row of column zero equals the requested amplitude function."
protocol := .blindLeanOnly
reviewerSeparated := true
checkedSlots := [.targetObject, .scalarAndDimensions, .normalization, .registerOrder, .exactness, .conclusion, .resourceScope]
deltas := []
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “verified state preparation round trip admissible”; the hypotheses and conclusion in the code panel fix its exact scope. The exact state-preparation round trip satisfies the independent-audit contract.
theorem verifiedStatePreparationRoundTrip_admissible :
RoundTripAudit.Admissible verifiedStatePreparationRoundTrip := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “one term robin claim round trip”. **Paper theorem is not yet reconstructed as a proved block encoding.** The GHL source-facing branch records the one-term Robin claim, normalizer, register and resource formulas, and the full theorem-facing transcript.
def oneTermRobinClaimRoundTrip : RoundTripAudit where
auditId := "ghl-one-term-robin-source-fidelity"
sourceAnchor := "Guseynov-Huang-Liu 2025 one-term Robin theorem; QuantumBlockEncoding/GHL2025.lean"
originalText := "The one-term Robin construction block-encodes A_k with normalizer N_D N_f κ, the stated signal-qubit layout, 2n pure ancillas, and the advertised gate complexity."
leanDeclaration := "QuantumBlockEncoding.GHL2025.oneTermRobinClaim together with oneTermRobinTheoremFacingFig4Circuit_gateList"
decoderInput := "The GHL2025 Lean declarations, their imported definitions, and declaration documentation only; the paper theorem prose is hidden."
reconstructedText := "Lean records a ConstructionClaim, symbolic normalization/layout/resource data, and a theorem-facing gate transcript. The module explicitly does not yet prove matrix-level block correctness. It also distinguishes the full source transcript from the active seven-gate backend product."
protocol := .blindLeanOnly
reviewerSeparated := true
checkedSlots := [.targetObject, .normalization, .ancillaLayout, .registerOrder, .cleanProjection, .oracleAssumptions, .conclusion, .resourceScope]
deltas := [
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “one term robin claim round trip admissible”; the hypotheses and conclusion in the code panel fix its exact scope. The GHL source-fidelity audit satisfies the independent-audit contract.
theorem oneTermRobinClaimRoundTrip_admissible :
RoundTripAudit.Admissible oneTermRobinClaimRoundTrip := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “candidate improvement round trip”. **Source wording is underspecified without a correctness fibre.** 'BlockEncodingCost.betterThan' proves only a lexicographic comparison of gate count, depth, auxiliary qubits, and unresolved oracle calls.
def candidateImprovementRoundTrip : RoundTripAudit where
auditId := "same-semantic-fibre-before-resource-improvement"
sourceAnchor := "QuantumBlockEncoding/BlockEncoding.lean: BlockEncodingCost.betterThan"
originalText := "The evolved block-encoding candidate is better than the baseline."
leanDeclaration := "QuantumBlockEncoding.BlockEncodingCost.betterThan"
decoderInput := "The Lean definition and imported resource records only; the informal improvement claim is hidden."
reconstructedText := "The relation is a strict lexicographic order on gateCount, depth, auxiliaryQubits, and oracleCalls. It contains no premise connecting the compared costs to equal targets or to certified block-encoding semantics."
protocol := .blindLeanOnly
reviewerSeparated := true
checkedSlots := [.targetObject, .normalization, .cleanProjection, .exactness, .errorNorm, .conclusion, .resourceScope, .sameSemanticFibre]
deltas := [
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “candidate improvement round trip admissible”; the hypotheses and conclusion in the code panel fix its exact scope. The same-semantic-fibre audit satisfies the independent-audit contract.
theorem candidateImprovementRoundTrip_admissible :
RoundTripAudit.Admissible candidateImprovementRoundTrip := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “semantic round trip registry”. The initial public semantic-fidelity registry shown as declaration leaves in the Underlying Lean Graph.
def semanticRoundTripRegistry : List RoundTripAudit :=
[ verifiedOperatorBlockEncodingRoundTrip
, approximateBlockEncodingNormRoundTrip
, verifiedStatePreparationRoundTrip
, oneTermRobinClaimRoundTrip
, candidateImprovementRoundTrip
]
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “semantic round trip registry length”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem semanticRoundTripRegistry_length :
semanticRoundTripRegistry.length = 5 := rfl
commit-pinned source · Verso Blueprint panel