[amaybaum]

WIP / UNVERIFIED. Independent review pending; merge not authorized.

This is a paper-only verification unit for #1033 (BSEL-2, Q2A). It is authorized by the owner ruling in #1033 comment 6662765230 (amaybaum, Claude Code session chat, 2026-11-05, shortly before 16:03Z). That ruling releases F l. 430 for this candidate pair only, which is the pair from the assessment in #1033 c.6662297536. The ruling is quoted verbatim in PREREG.md §0.

Record directory: verification/programmes/oi-qm/reconstruction/bsel-2-q2a-ce-20261105/

Commits, in order

1. Freeze: 6fad52e1767c03a13e84c6c5ba8a4e119984bda4 adds PREREG.md. It was pushed before any check algebra. It fixes:
   • both full 4×4 matrices: W = H₄/2, and W′, which is H₄/2 with its columns at (0,a₁) and (1,a₀) exchanged. The assessment did not fix the off-anchor columns, so they are fixed here;
   • the K-c element: L = 1_V ⊗ H₂, K = diag(1,−1,i,1);
   • the definitions, with their source lines on main;
   • controls K-a to K-e;
   • the fixed decision rule (COUNTEREXAMPLE or VOID);
   • the scope.
2. Result: 49021c8cd26c59797b650a0e434119f97fad0482 adds RESULT.md only. It writes out the hand algebra in exact arithmetic. No script, CAS or search was used.

Controls. All pass.

• K-a: W, W′, L and K are unitary.
• K-b: the complete-record laws of C0, C2-ch and C2-sel agree entrywise, for every root, every read list and every record. This includes every ⊥ mass and the |A| ≥ 3 extension. Γ = J/2 and α = J/4 for both.
• K-c: the computed fibre-Gram data of LWK match TSG:263's phase law with c = (1, i). |g| is unchanged.
• K-d: W′ has rank-2 fibre-Gram data. The |A| = 1 identity |g|² = Γ₀₀Γ₀₁ is re-derived, so the pair does not conflict with Fib = G at |A| = 1.
• K-e: Lemma R (each direction separately) and Lemma C are re-derived from kernel lines on main only. The definitions match the assessment's reading.

Gram invariant: |g(W)| = ½ and |g(W′)| = 0.

Verdict, by the fixed rule: COUNTEREXAMPLE[C0, C2-ch, C2-sel; |V| = 2, |A| ≥ 2; constant lifts; equal complete-record laws; all-unitary class; outside PPer].

Does not establish:

• anything about the PPer subclass, whose cells stay "not addressed";
• anything about native OI-realizable or restricted lift classes;
• anything about physically sourced access;
• any physical equivalence claim.

Not done:

• no theorem promotion;
• no Lean work;
• no manuscript edit;
• no change to research(#1033 BSEL-2): Q2A record, O⇒G for C2-ch and C2-sel at |V|=2, |A|≥2 — both NOT ESTABLISHED (draft, preservation) #1125 or its branch.

The B4′ matrix change is proposed in RESULT.md §9 for owner approval and is not applied.

Checks:

• artifact_placement_check: OK.
• duplicate_check: OK.
• legacy_records_check: self-test OK. The commit check is undecidable locally because the clone is shallow, so CI is relied on for it.

§A.42 item 8: RESULT.md §10 traces every off-main reference. The freeze-before-check invariant uses the order of the two commits. That gap closes only if both commits land with a merge commit, not a squash.

---

Generated by Claude Code

[amaybaum]

Independent mathematical review of #1139 at 49021c8c: ACCEPT WITH CHANGES (non-material)

Independent mathematical review: draft PR #1139 (BSEL-2 Q2A candidate counterexample)

Reviewer: independent, read-only. All algebra below was done by hand: no script, no CAS, no search.
Objects: freeze 6fad52e1 (PREREG.md), result 49021c8c (RESULT.md), base = origin/main a8ab8dae (unchanged at review time).
Sources read: #1033 c.6662765230 (ruling) and c.6662297536 (assessment); B4PRIME.md and SCOPE.md at a8ab8dae; TSG, CLG, DC, CF and RC at a8ab8dae.

Verdict: ACCEPT WITH CHANGES. None of the changes is material to the verdict. The counterexample holds. COUNTEREXAMPLE[C0, C2-ch, C2-sel; |V|=2, |A|≥2; constant lifts; all-unitary class; outside PPer] follows from the frozen rule.

1. Process

• Commit chain. a8ab8dae → 6fad52e1 (16:10:49Z) → 49021c8c (16:15:04Z). The freeze has exactly one parent, the base.
• Files. The result commit adds only RESULT.md. PREREG.md is byte-identical between 6fad52e1 and 49021c8c. The PR (2 files) touches only the record directory: no manuscript, Lean or research(#1033 BSEL-2): Q2A record, O⇒G for C2-ch and C2-sel at |V|=2, |A|≥2 — both NOT ESTABLISHED (draft, preservation) #1125 change.
• Authorization. The ruling was posted at 16:03:47Z, before the freeze. PREREG §0's quotation matches the comment verbatim.
• What PREREG fixes. It fixes every matrix entry (W, W′, L, K), each control's pass criterion and the decision rule. RESULT uses exactly these.
• Writer's choices, and whether they could tailor the outcome.
  • Off-anchor columns. No tailoring is possible. P-conf roots are e_j, and constant lifts give T = XXᴴ = 1. So every mass of C0, C2-ch and C2-sel, and FG, Γ, α and g, depend only on the anchored columns Xe_j. The assessment fixed those at 15:43:36Z, a host timestamp before the ruling. The off-anchor columns only have to complete the anchored columns to a unitary.
  • e₁ = e_{(1,a₀)}. This is B4 l. 32's notation, and it reproduces the assessment's columns: We₁ = h₂/2 = ½(1,1,−1,−1) and W′e₁ = h₁/2 = ½(1,−1,1,−1). I checked these against H⊗H in Kronecker order (v,a).
  • K = diag(1,−1,i,1). It is weak with c = (1,i) and is not strong, so the control is non-trivial.
  • K-d's "at least one member". This criterion is logically forced. If neither member's vectors were non-collinear, both would have |g| = √(Γ₀₀Γ₀₁), so |g| would be equal and the rule would give VOID anyway.
• Freeze evidence (see §6). The claim that the freeze was "pushed before any computation" is not evidenced by host records available to me. The PR was opened at 16:15:40Z, after both commits, and commit dates are self-reported. This is immaterial for the reason given under "Off-anchor columns" above.

2. Definitions against main

All match:

• LeftFibreGroup (TSG:78–79);
• TwoSidedRelated (TSG:84–87), time-dependent L_t, K_t;
• FibreGram (TSG:95–97) and fibreGram_apply (TSG:115–116), conj-linear in the first slot, rows (i,a), anchored columns (j,a₀);
• GramPhaseEquiv (TSG:102–103);
• fibreGram_diag (TSG:127);
• fibreGram_rank_le (TSG:146);
• sum_fibreGram (TSG:153);
• fibreGram_left_mul (TSG:207);
• gramPhaseEquiv_of_twoSided (TSG:263–265, forward);
• twoSided_slice_iff (TSG:826–834, both directions);
• twoSidedRelated_iff (TSG:839–850; mp uses TSG:263 slicewise);
• WeakAnchorStabilizer (CLG:114–116) and weak_anchor_coeff_norm_one (CLG:146);
• AdmissibleDilationAt / Γ (DC:134–136);
• RelativeCandidate (CF:123–129);
• PPer (RC:32–33);
• the procedures and candidates (SC ll. 112–124) and Λ_C as masses only (SC ll. 24–25);
• readings (r1) and (r2) (B4 ll. 57–62).

g is the fibre-0 off-diagonal, as the assessment reads it.

3. Re-derivation

Matrices. Basis order p₀=(0,a₀), p₁=(0,a₁), p₂=(1,a₀), p₃=(1,a₁). H⊗H has rows (1,1,1,1), (1,−1,1,−1), (1,1,−1,−1), (1,−1,−1,1); it is symmetric, so its columns are h₀..h₃ as in PREREG.

K-a: pass.

• The pairwise dots of the h's are 4 on the diagonal and 0 off it (all six off-diagonal pairs checked). So WᴴW = 1.
• W′ = W·P_σ with P_σ a permutation, so W′ is unitary.
• H₂² = ½[[2,0],[0,2]] = 1, so L is unitary.
• |1|, |−1|, |i|, |1| = 1, so K is unitary.

Data. Fibre-0 rows are p₀,p₁; fibre-1 rows are p₂,p₃.

Anchored columns:

• We₀ = W′e₀ = ½(1,1,1,1);
• We₁ = ½(1,1,−1,−1);
• W′e₁ = ½(1,−1,1,−1).

Readback:

• Γ(i,j) = ¼+¼ = ½ for all i, j and both lifts, so Γ = J/2.
• α uses the entries at (p₀,p₀), (p₀,p₂), (p₂,p₀), (p₂,p₂): W has ½, ½, ½, −½ and W′ has ½, ½, ½, ½. So α = J/4 for both.

Fibre-Gram data:

• FG⁽⁰⁾(W)(0,1) = ½·½+½·½ = ½; FG⁽¹⁾(W)(0,1) = ½(−½)+½(−½) = −½.
• FG⁽⁰⁾(W′)(0,1) = ½·½+½(−½) = 0; FG⁽¹⁾(W′)(0,1) = ½·½+(½)(−½) = 0.
• Diagonals are ½, and each fibre pair sums to 1.

So |g(W)| = ½ ≠ 0 = |g(W′)|.

K-b: pass. Take a constant X with T_{t,s} = XXᴴ = 1.

• C0. Record mass Γ(v,j) = ½ for both lifts. There is no ⊥.
• C2-ch.
  • Step 1: Lüders P_{v₁}Xe_j has mass Γ(v₁,j). The post-read state lies in fibre v₁, so Rst-ch leaves Γ(v₁,j)·e_{v₁}e_{v₁}ᴴ. This holds whether Rst-ch is a channel or any dilation of it, since the reduced state is what enters later reads.
  • Later steps: P_w e_v = δ_{wv}e_v.
  • Law: ½·Πδ_{v_{m+1}v_m}, the same for both lifts. The masses sum to 1.
• C2-sel (r2). I recomputed the step-1 table entry by entry.
  • W, j=1: v=0 gives ok ½e_{p₀} and ⊥ ½e_{p₁}. v=1 gives ok −½e_{p₂} and ⊥ −½e_{p₃}.
  • W′, j=1: v=0 gives ok ½e_{p₀} and ⊥ −½e_{p₁}. v=1 gives ok ½e_{p₂} and ⊥ −½e_{p₃}.
  • j=0: the same for both lifts.
  • Every step-1 ok mass and every step-1 ⊥ mass is ¼.
  • Steps m ≥ 2 from c·e_v: ok has mass |c|²δ and ⊥ has mass ‖(1−Π)δ c e_v‖² = 0.
  • All-ok masses are ¼·Πδ. A ⊥ at step 1 has mass ¼. A ⊥ at a later step has mass 0. The total is ½ + ½ = 1.
  • The masses are equal entrywise, ⊥ included. The states differ only by signs, and Λ_C records masses only (SC l. 24).
  • Not stated in RESULT, but true: under the other Rst-sel reading, which omits the last test, the law is a coarse-graining of this one, so it is equal as well.
• |A| ≥ 3. X⊕1 leaves the anchored columns supported on {a₀,a₁} and keeps T = 1. Every projection, mass, Γ, α and g is unchanged, and X⊕1 is unitary.
• W0 cross-check. Agrees: 𝒪₂ = β = 1 restricted to 𝒜, so 𝒪₂ − β = 0.

K-c: pass.

• WK rows are ½(1,−1,i,1), ½(1,1,i,−1), ½(1,−1,−i,−1), ½(1,1,−i,1).
• Applying L gives LWK = (1/√2)[[1,0,i,0],[0,−1,0,1],[1,0,−i,0],[0,−1,0,−1]].
• Anchored columns: (1,0,1,0)/√2 and (i,0,−i,0)/√2.
• FG⁽⁰⁾(0,1) = i/2 and FG⁽¹⁾(0,1) = −i/2. These equal conj(c₀)·(±½)·c₁ with c = (1,i). The (1,1) entry is conj(i)·½·i = ½.
• So all eight entries obey TSG:263's law, and |g| = ½ is preserved, even though the anchored columns of LWK differ visibly from those of W.

K-d: pass.

• (i) P₀W′e₀ = ½(1,1) and P₀W′e₁ = ½(1,−1) are orthogonal. So 0 ≠ ¼ = Γ₀₀Γ₀₁, and FG⁽⁰⁾(W′) = ½·1 has rank 2.
• W is the rank-1 member.
• (ii) At |A| = 1, g = conj(X₀₀)X₀₁, so |g|² = Γ₀₀Γ₀₁.

K-e: pass.

• Lemma R (a⇒b). TSG:263 gives GPE. At j=k, |c_j|² = 1 gives equal Γ (TSG:127). At (0,0,1), |g′| = |c̄₀ g c₁| = |g|.
• Lemma R (b⇒a), checked separately (§A.34).
  • Hermiticity gives the (1,0) entries as conjugates of the (0,1) entries.
  • At |V| = 2, TSG:153 gives FG⁽¹⁾ = 1 − FG⁽⁰⁾, so FG⁽¹⁾(0,1) = −g.
  • Take c = (1, g′/g), or c = (1,1) if g = 0. This matches all eight entries.
  • TSG:826 mpr then gives (a).
  • The verdict does not use this direction.
• Lemma C(i).
  • (⇒) TSG:84 at t = 0.
  • (⇐) constant L, K.
• Lemma C(ii). Lemma C(ii) holds for the constant lifts in K-b.

4. Gram invariant and direction

The verdict uses only the forward direction G ⇒ GPE at every t, which is kernel-proved (TSG:839 mp / TSG:263). GPE preserves |FG⁽ⁱ⁾(j,k)|. So ½ ≠ 0 gives ¬GPE at t = 0, hence ¬TwoSidedRelated. The direction is correct, and it does not rely on the unformalized converse.

5. Verdict and scope

• Verdict. The §5 rule is applied as written, and every condition holds.
• Scope. The scope statement does not overreach. It says nothing about PPer, native or restricted lifts, physical access, or physical equivalence. Here Γ₀ = J/2 ≠ 1, which is the only PPer clause that fails.
• §9 proposal. It is accurate and stated as a proposal only. The existing row 514 reads "any" and rows 519 and 521 read "all; PPer"; splitting them by class is correct. WE lies in PPer, so the C2 rows' G⇒O column "disproved" is right in both class rows.

6. §A.42 item 8 and requested changes (non-material)

C1. RESULT §8 "Equivalence picture" contradicts §10.

• §10 states: "No [D] result of B4 is used as a premise". But §8 concludes "strictly coarser" for C0 from "B4 row 506" (★, F l.178, off main), and "incomparable" for C2-ch and C2-sel from WE (B4 [D], unreviewed; §A.46 item 7).
• I re-checked WE's Rst-ch case by hand:
  • U: T = P, so p(0,0|0) = 1.
  • gU: LPL·e₀ = ½(p₀+p₁+p₂−p₃), so the masses are ½ and ½.
• So the claim is true, but the record must say what it rests on. Fix: cite TSG:217 and CLG:273 (kernel, on main) for C0 G⇒O, and either re-derive WE in three lines or label "incomparable" as resting on B4's unreviewed WE. Then add both to the §10 ledger.

C2. RESULT §10, freeze row.

• "Merge commit, not squash" should also exclude rebase-merge. A rebase-merge rewrites 6fad52e1 and 49021c8c, so the cited SHAs would not be reachable from main (§A.42 item 3).
• The record should also state the following:
  • the push order is not host-evidenced;
  • the material frozen content, the anchored columns, was fixed in the host-timestamped assessment;
  • the off-anchor completion provably cannot affect any tested quantity.

C3. RESULT §9 table.

• The C0 G⇒O "proved" cells should name their support (TSG:217, CLG:273), not only the W/W′ pair or "—".
• The list of B4 passages to correct could add l. 577 (the premise-ledger entry "l. 430: the undecided item").
• SCOPE.md l. 269 is a verbatim copy of the reviewed scope and should not be edited.

None of C1–C3 changes a control, a value or the verdict.

---

Generated by Claude Code

[amaybaum]

Disposition of the review's changes (c.6663191565): applied at 45bb1b9c565b175bd2b9677fa39d78bd698f7f84

This is one fast-forward commit on 49021c8c, and it changes only RESULT.md (+36/−6).

• PREREG.md and the frozen pair are unchanged.
• No control, value or verdict changes.

Change	Disposition	Where
C1	Applied. C0's G⇒O now cites TSG:217 and CLG:273, together with Lemma R (a⇒b). WE is re-derived by hand. Rst-ch, root 0, reads (0,1): (1, 0) for U against (½, ½) for gU. Rst-sel, one read: (0,ok) = 1 for U against ½ for gU, with (0,⊥) = ½. A matching row is added to the §10 ledger, so §8 and §10 agree.	§8 "Equivalence picture"; §10
C2	Applied. The freeze row now states four things. The branch must land by a true merge commit; a squash or rebase-merge would orphan 6fad52e1 and 49021c8c (§A.42 item 3). No host record shows the push order, since the PR was opened after both commits. The anchored columns were fixed in the assessment (#1033 c.6662297536, 15:43:36Z). The two off-anchor columns cannot affect any tested quantity.	§10
C3	Applied. The C0 G⇒O cells now name TSG:217 and CLG:273. B4 l. 577 is added to the passages to correct. SCOPE.md l. 269 is marked as a verbatim copy that is not to be edited.	§9

Checks:

• artifact_placement_check: OK.
• duplicate_check: OK.
• No push-triggered workflow matches this path.

Merge is not authorized. The proposed B4′ matrix change still awaits the owner.

---

Generated by Claude Code

[amaybaum]

Independent recheck at 45bb1b9c565b175bd2b9677fa39d78bd698f7f84: ACCEPT

The same independent reviewer read the head by object id and redid the algebra by hand.

• Scope: this commit changes only RESULT.md (+36/−6), with single parent 49021c8c. PREREG.md and the frozen pair are unchanged.
• C1:
  • The C0 support cites TSG:217 and CLG:273.
  • WE was rechecked by hand. Le_{p₀} = (p₀+p₁)/√2, then P gives (p₀+p₃)/√2, then L gives ½(p₀+p₁+p₂−p₃).
  • Rst-ch masses are 1 against ½/½. Rst-sel ok masses are 1 against ½, with ⊥ mass ½.
  • §8 and §10 now agree.
• C2: the §10 freeze row contains all four points. The landing must be a true merge commit, not a squash or rebase-merge.
• C3: the §9 support cells, the B4 l. 577 entry and the SCOPE.md l. 269 note are in place.
• Unchanged: no verdict, value or scope.

The verdict stands. It follows from the frozen rule:

COUNTEREXAMPLE[C0, C2-ch, C2-sel; |V|=2, |A|≥2; constant lifts; equal complete-record laws; all-unitary class; outside PPer].

Nothing is concluded about PPer, native OI-realizable lifts or physical access. The proposed change to the B4′ matrix rows (RESULT §9) is only a proposal and is not applied.

CI on this exact head comes next. Merging, and approving the B4′ matrix change, are separate owner decisions.

---

Generated by Claude Code

[amaybaum]

Ready for owner decisions at 45bb1b9c565b175bd2b9677fa39d78bd698f7f84

• CI: PR verify run 42063802555 at this exact head succeeded (25 jobs green, 1 matrix template skipped).
• Review: independent mathematical review ACCEPT WITH CHANGES (non-material), applied, then recheck ACCEPT (c.6663209861).
• Record: the freeze 6fad52e1 comes before the result 49021c8c, followed by the review fixes 45bb1b9c. PREREG.md is unchanged after the freeze.
• Verdict (frozen rule): COUNTEREXAMPLE[C0, C2-ch, C2-sel; |V|=2, |A|≥2; constant lifts; equal complete-record laws; all-unitary class; outside PPer]. Nothing is concluded about PPer, native OI-realizable lifts or physical access.

Two separate owner decisions are needed.

1. Merge. If approved, the merge must be a true merge commit, with no squash and no rebase-merge, so that freeze-before-check stays verifiable on main (§A.42 item 3). main has moved since this branch was cut (Main §3.4: credit Egri et al. (F-9) #1137), so a content-identical integration comes first.
2. The proposed B4′ matrix change (RESULT §9). It splits the O⇒G rows to record the scoped counterexample and keeps the PPer cells "not addressed". The owner ruling requires that any change to the B4′ matrix come back for approval. Approving the merge of this record does not apply that change.

---

Generated by Claude Code

[amaybaum]

Merge record (owner approval #1033 c.6663694191)

Merged as a true merge commit c987b890a5ca1c0100c85b03b4f5355a03b00032. Its parents are 0da40cff (main) and bdbd21911f89d52f434b5e26e73ee8f4ddbb2a1c, which is the integration merge of main 0da40cff into the reviewed head 45bb1b9c. No squash and no rebase.

Before the merge

• Content identity. git diff a8ab8dae 45bb1b9c is byte-identical to git diff origin/main bdbd2191: only PREREG.md and RESULT.md in the record directory.
• Local checks. duplicate, artifact-placement, staleness and coverage all pass.
• Exact-head CI. PR run 42067896705 at bdbd2191 succeeded, with 25 jobs green and 1 skipped.
• Branch state. The branch was up to date with main.

After the merge

• Tree. The merged tree equals the tree of bdbd2191.
• Original commits reachable from main. All three are confirmed:
  • freeze 6fad52e1767c03a13e84c6c5ba8a4e119984bda4;
  • result 49021c8cd26c59797b650a0e434119f97fad0482;
  • review fixes 45bb1b9c565b175bd2b9677fa39d78bd698f7f84.
• main CI. verify run 42069093636 at c987b890 succeeded, with 25 jobs green and 1 skipped.

Provenance, per the owner's instruction. The commit order freeze → result is preserved on main. That the freeze was pushed before any checking was done has no independent host evidence: the PR was opened after both commits. This record does not strengthen that claim.

Accepted result. COUNTEREXAMPLE[C0, C2-ch, C2-sel; |V|=2, |A|≥2; constant lifts; equal complete-record laws; all-unitary class; outside PPer]. PPer, native OI-realizable lifts and physically sourced access remain unresolved. The B4′ matrix correction is the separate PR #1144.

---

Generated by Claude Code