Plain-English reading. Lean checks the proposition indexed as “warm robin four slot bits prepare unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The two-bit selector PREPARE is unitary.

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 two-bit selector PREPARE is unitary.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:33. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot selector prepare unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Reindexing preserves selector unitarity.

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. Reindexing preserves selector unitarity.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:47. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot bits prepare clean column”; the hypotheses and conclusion in the code panel fix its exact scope. Uniform clean-column amplitude before selector flattening.

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. Uniform clean-column amplitude before selector flattening.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:54. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot selector prepare clean column”; the hypotheses and conclusion in the code panel fix its exact scope. Uniform clean-column amplitude after selector flattening.

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. Uniform clean-column amplitude after selector flattening.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:63. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot selector prepare probability”; the hypotheses and conclusion in the code panel fix its exact scope. Every selector slot has probability exactly '1/4' in the clean column.

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. Every selector slot has probability exactly '1/4' in the clean column.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:76. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot system perm bijective”; the hypotheses and conclusion in the code panel fix its exact scope. Each sector-preserving four-shift SELECT is a basis bijection.

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. Each sector-preserving four-shift SELECT is a basis bijection.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:103. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot coefficient abs le one”; the hypotheses and conclusion in the code panel fix its exact scope. Every four-slot real amplitude lies in '[-1,1]'.

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. Every four-slot real amplitude lies in '[-1,1]'.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:119. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot rotation unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Every controlled coefficient rotation is unitary.

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. Every controlled coefficient rotation is unitary.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:137. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot rotation clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. The clean coefficient entry is the desired signed amplitude.

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 clean coefficient entry is the desired signed amplitude.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:144. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot coefficient complex”; the hypotheses and conclusion in the code panel fix its exact scope. Rational and real-complex views of the four-slot coefficient agree.

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. Rational and real-complex views of the four-slot coefficient agree.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:153. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot middle logical unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The complete four-slot middle construction is exactly unitary.

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 complete four-slot middle construction is exactly unitary.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:171. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot sector clean formula same”; the hypotheses and conclusion in the code panel fix its exact scope. On one sector, the full-system formula is the existing four-shift formula.

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. On one sector, the full-system formula is the existing four-shift formula.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:190. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot sector clean formula cross”; the hypotheses and conclusion in the code panel fix its exact scope. Cross-sector clean entries vanish because SELECT preserves the sector.

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. Cross-sector clean entries vanish because SELECT preserves the sector.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:200. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot sector clean formula eq target”; the hypotheses and conclusion in the code panel fix its exact scope. The structural clean formula is exactly the normalized direct sum.

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 structural clean formula is exactly the normalized direct sum.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:221. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot middle logical unitary clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. The reusable clean-entry expansion specializes to the four-slot sector formula.

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 reusable clean-entry expansion specializes to the four-slot sector formula.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:239. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot middle logical unitary clean entry eq target”; the hypotheses and conclusion in the code panel fix its exact scope. The middle logical clean block is exactly the normalized sector target.

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 middle logical clean block is exactly the normalized sector target.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:278. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. Lean checks the proposition indexed as “warm robin four slot middle logical unitary clean system block”; the hypotheses and conclusion in the code panel fix its exact scope. Matrix form of the middle clean-block certificate.

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. Matrix form of the middle clean-block certificate.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean:287. A commit-pinned external link is added by the publication build when the source exists at the published ref.