MATH-CON-1: preregistration on PolC + B23 (WIP / UNVERIFIED) by amaybaum · Pull Request #1206 · amaybaum/incompleteness

amaybaum · 2026-11-08T12:20:55Z

This is the guiding draft PR for MATH-CON-1, the mathematical-construction workstream under #1169.

Authority: owner decision #1169 c.6721267600. Preparation and an independent review of the preregistration only. Building on the MATH-CON-0 inventory, which was accepted (#1169 c.6721102809 and c.6721121369, with reviews c.6721133702 and c.6721137458).

Content. One file, verification/programmes/oi-qm/reconstruction/mathcon1-polc-20261108/DESIGN.md, at head e593465b, from main 45eea51d. It contains no derivation, Lean run, computation or new premise.

Design (author summary, not yet reviewed):

Object. The object is polarizedTheoryC (Fin 2), with B23's finite protocol taken as already proved. The added rule is the polarization map: its [R] part is the position-half reading; its [Q] part is the images S and H.
Frozen baseline. All monomials (substratumClass).
Target. A coherent non-monomial operation is an available branch p·Ad U with U non-monomial. The T2 criterion additionally requires U to be non-Clifford on the qubit.
Circularity test. It returns generated, installed, mixed or undetermined, with a fiat check.
Countercontrols. CC-0 is a calibration that must return generated. CC-1 is H by fiat. CC-2 compares PolGen against PolC. CC-3 checks that the monomial baseline has no coherent non-monomial operation. CC-4 covers three disguised forms of H.
Outcomes. One of (P) positive and noncircular, (C) conditional and circular, (N) negative, or (I) inconclusive. The writer discloses that on this object only (C), (N) or (I) can be reached, because the rule supplies H as a generator. Under the owner's ruling, (C) records that the existing mathematics is valid, that the noncircular milestone is not reached, and what form the missing rule needs.

Status. WIP / UNVERIFIED. An independent review is pending. Stage 1B (the derivations and Lean membership proofs) needs a separate owner authorization. This PR is not a merge request.

Generated by Claude Code

Stage 1A preregistration only, per owner decision #1169 c.6721267600. Object: polarizedTheoryC (Fin 2) = genTheory PolC with B23's finite protocol. Freezes the monomial baseline (substratumClass), D2/D3, the circularity test CT, countercontrols CC-0..CC-4 and the ordered outcome partition (P)/(C)/(N)/(I). No derivation, Lean, computation or premise. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

amaybaum · 2026-11-08T12:34:12Z

Independent review of the MATH-CON-1 preregistration at `e593465b` (model reviewer, not human): REVISE

REVIEW-MATHCON1-e593465b.md

# Independent review: MATH-CON-1 preregistration at `e593465b`

**Object.** `verification/programmes/oi-qm/reconstruction/mathcon1-polc-20261108/DESIGN.md` at
`e593465bdecd96bff92877f9ecf4fcf8befec845` (branch `research/mathcon1-prereg-20261108`; parent
`main@45eea51d`). The commit changes exactly this one file (613 lines).

**Reviewer.** An independent Claude Code reviewer, 2026-11-08. I did not write this design and had
not reviewed it before. Paper only: no Lean build, no scientific computation. Every algebraic check
below is done by hand and shown in §C.

**Authority read.** #1169 c.6721267600 (amaybaum, 2026-11-08T12:05:53Z) and c.6720678942 (amaybaum,
2026-11-08T11:03:23Z), both fetched from the API. Input: MATH-CON-0 inventory r3, sha256
`e68058bafc993a41647c4c8d50bce285a401ee2321ebaaf200b09afa1ff28df5`, which matches the design's
`e68058ba…28df5`. I also read its two reviews.

## Verdict: **REVISE**

There are 4 blocking findings, B1–B4. Each needs only a local change, and none of them touches the
object, the baseline or the owner's rulings. All four are in the circularity test (CT) or the
outcome partition, which are the design's decisive instruments. B1 changes CT's marking rule, so
the revision needs a re-review to confirm that CC-0 still returns `generated`. The re-review can be
narrow: §4.4, §5, §6 and the new §1.3 column.

***

## A. Blocking findings

### B1. CT marks leaves only and admits only scalar-unique characterizations, so fiat installation can be relocated to evade it, and CC-4 cannot fail

**Location.** §4.4, I-3 and Step 1. §5, CC-4.

**Evidence.**
- Step 1 marks a *leaf* of `d*` whose matrix is in `NM(ℛ)`. I-5 makes leaves the class-generator
  applications and interface primitives. A non-monomial matrix that a rule names *inside a closure
  constructor* is never a leaf. Example: the clause "if `K ∈ 𝓘` then `K·H ∈ 𝓘`". Apply it to the
  leaf `1 ∈ permClass` and it yields `H` at an internal node. No leaf is marked, so Q2 = yes and
  CT returns `generated`. This installs `H` by fiat, and the verdict is wrong.
- I-3 counts a characterization only "when that condition fixes the operator up to a scalar".
  Example: the generator clause "the swap layer goes to some unitary `W` with `W X Wᴴ = Z`". Its
  solution set is `{diag(e^{ia}, e^{ib})·H}`, which is not unique up to a scalar (§C.6). Every
  member is non-monomial. No bullet of I-3 clearly places such a `W` in `Mat(ℛ)`. Whether
  `diag(1,e^{iφ})·H` counts as "written by a formula" is a further choice. So CT is not decidable
  from its stated inputs for family-valued clauses. The natural reading returns `generated`.
- CC-4's three disguises map one-to-one onto three bullets of I-3: DV-a is a formula, DV-b a
  characterization unique up to scalar, DV-c a relabelling. CC-4 therefore checks the list against
  the items it was built from, and it cannot fail. A control that only reproduces its own
  specification is not decisive (Code Review Rules, "Exactness and controls").
- These holes do not change the object's verdict. `PolC`'s constructors (`mul`, `smul`, `proj`,
  `block`, `relabel`) name no matrix, and `PolC.swap` is a literal generator. They do matter for
  the (C) record. §6 item 2 defines the missing rule as "a rule for which CT would return
  `generated`", and both evasions above meet that definition.

**Change required.**
- Replace leaf marking with *clause-instance* marking. A node of `d*`, a leaf or an internal node,
  is marked when it applies a clause of `ℛ` whose text refers to specific matrices and the node's
  matrix is non-monomial. Such text includes:
  - constants;
  - a stated map at stated inputs;
  - a condition on stated matrices, *whether or not* it fixes the operator up to a scalar.

  A closure law that is uniform over all class members and names no matrix stays unmarked. CC-0's
  superposition law is the model case.
- State the same distinction in I-3. A family-valued specification places every member of the
  family in `Mat(ℛ)` when the condition refers to stated matrices.
- Add to CC-4, with the same pass condition (`installed`):
  - **DV-d:** a constructor that embeds a constant, "if `K ∈ 𝓘` then `K·siteSwapImage n ∈ 𝓘`";
  - **DV-e:** a family characterization, "the swap layer goes to some unitary `W` with
    `W X Wᴴ = Z`".
- Re-check CC-0 under the new rule. I did, in §C.5: CC-0 stays `generated`, because its clause is
  uniform over `𝓘` and names no matrix. Record that check in §5.

### B2. Step 2's shortcut ("for a rule all of whose clauses are generator clauses on the unchanged interface A-2, Q2 = no follows from O-2 and O-1") is false, and CC-0 is a counterexample

**Location.** §4.4, Step 2, last bullet. It is load-bearing for §6, "A consequence of the frozen
definitions", and for CC-1(b).

**Evidence.** `ℛ_0` is a single generator clause: it makes operators admissible. It runs on the
unchanged interface A-2. Yet the design itself requires Q2 = yes for it (CC-0, §C.5). O-2 covers
only "the least label-invariant architecture generated by `substratumClass` together with the
monomial elements of a rule's matrix set". It says nothing about a rule that adds a new closure
constructor such as superposition. Applied literally to `ℛ_0`, the shortcut gives Q2 = no while the
exhibited `d'` gives Q2 = yes. CT has no row for "Q2 both", so a runner either reads the table top
to bottom and reaches `generated` by accident of row order, or treats the case as inconsistent and
voids CT. That is the H-2 failure CC-0 exists to exclude.

**Change required.** Restrict the shortcut to rules whose clauses only admit *named* matrices, so
that the rule's class is the least label-invariant architecture containing `𝓑` (or the [N] class)
together with those matrices, and the rule adds no closure constructor. State that a rule which
adds a closure constructor is outside the shortcut, and that its Q2 is decided by exhibition or by
proof. The object, `PolC`, falls inside the restricted shortcut, so §6's consequence survives.

### B3. The outcome partition is not well ordered: row 2's condition overlaps the (I) remainder

**Location.** §6, the order-2 row and the order-4 row.

**Evidence.** Row 2 reads "T2, T3 and T4 met, but (P) not reached". With CT = `undetermined` and
T2–T4 met, row 2 matches, and it precedes row 4. Yet row 4 lists "CT `undetermined` while T2
holds" as an example of (I). The same happens with CT = `generated` and T1 undetermined (CC-2(a)
undetermined). In both cases row 2 yields a (C) with neither sub-label. "First matching row wins"
then contradicts the stated examples, and the labels are not decidable from the conditions as
written.

**Change required.** Make row 2's condition exactly the union of its sub-labels:

`T2 ∧ T3 ∧ T4 ∧ [(CT ∈ {installed, mixed}) ∨ (CT = generated ∧ CC-2 records two rules)]`.

Every other case with T2 met falls through to (I). Also restate how CC-3's blocking rule and
CC-1's rejection rule route to order 0 or order 4 (see N4).

### B4. The object's clauses carry no I-2 type, and by I-2's own definition A-3/A-4 read as interface clauses

**Location.** §1.3, the assumption table, and §4.4 I-2. Also §6, "A consequence of the frozen
definitions", first bullet.

**Evidence.** I-2 requires each clause of `ℛ` to be "tagged with its class … and its type". §1.3
gives classes but no types. Under I-2, an interface clause "changes the carrier, the
identification, …". A-4, "the observer's state space is the amplitudes over the position
alphabet", and A-3, polarization with the position half read, are on their face identification
clauses. §6 instead presupposes that A-3–A-5 are *not* interface clauses ("Unless the [R] part
A-3 to A-5 is restated as an interface clause …"). Whether the restricted B2 shortcut applies to
the object turns on this tag. As frozen, the tag is a choice left to the Stage 1B runner.

**Change required.** Add a "type" column to §1.3 for A-3–A-7, each with a reason fixed
independently of the outcome. A defensible tagging:
- A-3 and A-4 are interface clauses that leave the formal interface A-2 unchanged. The carrier is
  still `Fin 2`, the same as `substratumTheory (Fin 2)`, and the `InstAvail` rules are unchanged.
  They supply no matrix.
- A-5–A-7 are generator clauses (`PolC.shear`, `PolC.swap`).

Then state that the restricted shortcut applies to the generator part, because the interface part
changes nothing formal.

***

## B. Non-blocking findings

### N1. (C) item 2 restricts the missing rule to "a clause that is not a generator clause". CT does not entail this, and CC-0 contradicts it

**Location.** §6, "Identifying the missing rule in (C)", item 2.

CC-0's generator clause can be `generated`. The form CT entails is "a clause that supplies no
non-monomial matrix, in the B1 sense, and yields a D2 (or D3) operation". The narrowing to
interface ("access or identification") clauses is the owner's wording in c.6721267600. Keep it if
wanted, but attribute it to that ruling and do not present it as a consequence of CT.

### N2. CC-2(b) can void a legitimate outcome, and O-6 has a simpler route than the one listed

**Location.** §5, CC-2.

If (a) is refuted, meaning `K*` is unavailable in `polarizedTheory (Fin 2)`, then CT has no `d*`
for `PolGen`. Then (b), "same verdict", fails, so "CT is void" fires and takes the result to
order 0. That pre-empts the T1-two-rules record that (a)'s own rejection rule prescribes. Make (b)
apply only when `K*` is available in both theories.

*Reviewer reading (pointer for O-6, not a result):* the `block` constructor gives the system-level
`H` in `PolGen` without `relabel` (§C.7). The ancilla-bit `H` of O-3a is available as `P·(H⊗I)·Pᵀ`
with `P ∈ permClass` (`perm`, `mul`). Route (ii), by contrast, uses `relabel` essentially
(`polC_levelThree_block`, PCL:734).

### N3. CC-3(b) cannot fail as written. Make it the check that is actually informative

**Location.** §5, CC-3(b).

`IsMonomial` holds by definition for `drivePhase`, controlled-`S` and Toffoli, so D2 fails for each
and D3 rejects each. The rejection that carries information is this: `drivePhase` *passes* D3's
non-Clifford clause and is rejected only by the monomial clause (§C.4), which shows the monomial
exclusion is what does the work. Controlled-`S` and Toffoli are additionally outside D3's carrier
scope, `Fin 2`. Restate (b) to record both facts, and call it a definitional calibration rather
than a control that can fail.

### N4. CC-1's rejection text is wrong in one case

**Location.** §5, CC-1.

"(a) not shown: CC-1 is vacuous, and T2 is unmet in any case." But (a) can be unshown because O-2
is unproved while T2 is established in `polarizedTheoryC`. Say: "(a) not shown: CC-1 is vacuous
(order 0)".

### N5. Q2's witness need not be `K*`

**Location.** §4.4, Step 2.

Q2 = yes needs a derivation `d'` of *a* D2 (D3) operation, which need not be `K*`. State that when
`d'` derives an operation other than `K*`, that operation is the reported T2/T5 witness, and T3/T4
are checked for it.

### N6. The Kraus and effect bullets of I-3 need a scope

**Location.** §4.4, I-3, the bullets beginning "as a Kraus operator of a channel that a clause
makes available" and "as an effect, projector or prepared density matrix …".

Restrict them to channels and effects *the clause itself states*. Otherwise every channel available
in `𝔗_ℛ` qualifies. `NM(ℛ)` would then contain `K*`'s own unitary, FC would be trivially yes, and
`mixed` would be unreachable for every rule.

### N7. The §6 consequence is unconditional, and its reachability list is loose

**Location.** §6, "A consequence of the frozen definitions".

- It rests on O-1 and O-2, which are unproved obligations. Phrase it as conditional on them; if
  either fails, CC-3 or CC-1 routes the outcome to order 0 or 4.
- On the object, `mixed` and (C-T1) are also unreachable:
  - `mixed` needs FC = no, but `PolC ⊆ 𝓕` (O-2) gives FC = yes whenever T2 holds in `PolC`, and the
    object has no interface clause that changes A-2;
  - (C-T1) needs CT = `generated`.

  State that the reachable labels are (C-inst) with CT = `installed`, (N) and (I), and give the
  reason for each excluded label.

### N8. What CC-0 calibrates

**Location.** §5 CC-0; §6 (P).

`ℛ_0` is wholesale [Q], a superposition closure. CT calls it `generated` because CT detects
*operation-specific* naming, not quantum structure. That is defensible under owner refinement 1
(c.6720678942), but the (P) label "noncircular" must not be read as "imports no quantum
structure". Require the outcome record to state the rule's class ([R]/[Q]) next to the CT verdict.

### N9. T4 for `K*` lacks an obligation for its stopped depths

**Location.** §3.2.

O-3d gives stopped depths of the `drivePhase` loop. The depth form for `K*`, the loop conjugated by
`H` through `bind`, is not listed. Add it to O-3e or O-9.

### N10. The §A.41 table has no checkpoint for the Stage 1B gate

**Location.** §10.2.

Add one: `RESULT.md` quotes the authorizing owner comment with author and time, and the first
Stage 1B commit postdates it.

### N11. The (C) record's shape assessment omits a scope limit

**Location.** §6 (C) item 3; §7.

The CT-defined form of the missing rule is an operator-level notion. For shapes 1–2 the frame-level
CT variant is unfrozen. Item 3 should say so, and not score those shapes against the
operator-level form.

### N12. Minor exactness notes for O-3e

**Location.** §3.2, O-3e.

- `H·drivePhase·H ∈ M₂(ℚ(i))` (§C.3), but `H` itself is not in `M₂(ℚ(i))`: the kernel's
  `hc = 1/√2`, so the branch identity needs `hc² = 1/2`.
- B23's scalar is typed `(5/8 : ℂ)`, while D2's `p` is real. Stage 1B needs the cast.

Neither is a defect.

### N13. O-1 has a close kernel template

**Location.** §3.2, O-1.

`DynamicsGlue.conj_diag_entry` and the rank-one-indicator column argument of
`diagonalGlue_forces_monomial` (DynamicsGlue:101) are the same technique for a fixed target
permutation. Cite them as the proof template so the work is not duplicated. O-1 itself, a branch
of an `InstAvail substratumClass` family, is not on `main`; I searched for it.

### N14. The added (I) outcome should be explained

**Location.** §6.

The owner's c.6720678942 names three outcomes (positive, conditional/partial, negative). The added
(I) is needed for totality. Say in one line that it is the remainder that makes the partition total,
not a fourth result type.

***

## C. Checks performed (hand algebra shown)

### C.1 Kernel spot-check, all 71 §3.1 items

I checked every §3.1 name against its cited file:line at `45eea51d` with `git show`, 71 of 71,
well beyond the 15 asked for. All 71 match.

I also read these definitions in full: `PolC`, `PolGen`, `siteShearImage`, `siteSwapImage`,
`hadamard`, `InstAvail`, `Architecture`, `genTheory`, `ContextStable`, `LabelInvariant`,
`IsMonomial`, `substratumClass`, `permClass`, `classical_instAvail`, `ancBlock`,
`exists_scaled_mem_of_instAvail_unitary`, `instAvail_spectator`,
`krausSoundExt_of_implementationGenerated`, `polarizedTheoryC_derivedOI` and the B23 block
(BFP:99–275).

Other record checks:
- Every repository link in the design is pinned to `45eea51d…` (17 blob links, 1 tree link).
- The read-write-sourced family identifier (`readWrite` followed by `Sourced`) does not occur.
- `9c201475..45eea51d` adds exactly the four A5-Q3 files.
- C5A:91–106 and 247–249, CH1:104–105, and M2D around 404–410 and 485–498 contain what is cited.

### C.2 O-3a: the circuit identity

Let `W = Toff·(S⊗I⊗I)·Toff`, with Toffoli's controls on the ancilla pair `(b,c)` and the token as
target.
- On ancilla value `bc ≠ 11`, Toffoli is trivial, so `W` acts on the token as `S = diag(1,i)`.
- On `bc = 11`, `W` acts as `X S X = diag(i,1)`.

So the token-0 block is `I + (i−1)|11⟩⟨11|` and the token-1 block is `iI + (1−i)|11⟩⟨11|`.

Next, `(H⊗H)|11⟩ = ½(1,−1,−1,1)ᵀ = v/2`, with `v` as in BFP (`v a = −1` for `a = 1, 2`). So
`(H⊗H)|11⟩⟨11|(H⊗H) = vvᵀ/4 = P`. The two blocks become `I + (i−1)P` and `iI + (1−i)P`, which are
exactly `balancedCircuit`'s entries (BFP:153–157). The identity holds.

The `PolC` factors O-3a names are right:
- `siteShearImage 4` is `S` on the token;
- `siteSwapImage 4` is `H` on the token, moved to an ancilla bit by `relabel` or by a `permClass`
  conjugation;
- Toffoli is in `permClass` (`permClass_permMatrix`).

### C.3 O-3c and the route (iii) target

**O-3c.** For `j ≠ 0`, `correction j = diag(r ↦ r.1 = 0 ? 1 : −1) = Z⊗I₄`. And
`(siteShearImage 4)² = diag(1, i²) ⊗ I = Z⊗I₄`. Correct.

**O-3e target.** The family is `bind(op H, attempt, op H)`. Its branch `((),0,())` is
`Ad H ∘ (5/8)Ad D ∘ Ad H = (5/8)·Ad(HDH)`, with `D = drivePhase` and `ω = (3+4i)/5`. This is
B23's branch `(5/8)·Ad(diag(1,ω))` conjugated by `H`.

`HDH = ½[[1+ω, 1−ω],[1−ω, 1+ω]] = [[(4+2i)/5, (1−2i)/5],[(1−2i)/5, (4+2i)/5]] ∈ M₂(ℚ(i))`.
- It is non-monomial: each row has two nonzero entries.
- It is unitary: `(|4+2i|² + |1−2i|²)/25 = (20+5)/25 = 1`, and the cross term
  `(4+2i)(1+2i) + (1−2i)(4−2i) = 10i − 10i = 0`.
- It meets D3: `(HDH) Z (HDH)ᴴ = H(DXDᴴ)H`, with `DXDᴴ = [[0,ω̄],[ω,0]] = (3/5)X + (4/5)Y`. So
  `(HDH)Z(HDH)ᴴ = (3/5)Z − (4/5)Y`, which is not proportional to any Pauli.
- `(HDH)X(HDH)ᴴ = X`, which confirms it is the 3-4-5 rotation about `X`.

The target `(5/8)·Ad(H·drivePhase·H)` is therefore correct, and as frozen it would meet D2 and D3.
This is an obligation check, not a T2 result. T2 is credited only from a kernel proof or a reviewed
exact derivation (§6, "Support standard"), as required.

### C.4 D2 and D3 are precise and phase-invariant; D3 rejects the hazard operations

**D2.** `Ad U` fixes `U` up to phase, since `Ad U = Ad V` implies `V†U` is central, hence a scalar.
`IsMonomial` is phase-invariant. For a matrix, "at most one nonzero entry per row and per column" is
equivalent to `IsMonomial`, because `d` may vanish and a partial permutation extends to a full one.

**D3.** `U P Uᴴ` is Hermitian, unitary and traceless. So if it is proportional to a Pauli it is
`±` one of `X, Y, Z`, never `I`. A global phase `e^{iφ}U` leaves `U P Uᴴ` unchanged. And `U` is
Clifford iff `UXUᴴ, UZUᴴ ∈ ±{X,Y,Z}`, since `UYUᴴ = i(UXUᴴ)(UZUᴴ)`. So D3 is the exact
single-qubit non-Clifford criterion, up to phase.

**Hazard operations:**
- **`drivePhase`.** It is diagonal, hence monomial, so D2 fails. It passes the non-Clifford clause:
  `D X Dᴴ = (3/5)X + (4/5)Y`. The monomial clause alone rejects it (N3).
- **Controlled-`S` `diag(1,1,1,i)`.** It is diagonal, hence monomial, and its carrier
  `Fin 2 × Fin 2` is outside D3's scope.
- **Toffoli on `Work`.** It is a permutation matrix, hence monomial, and its carrier is outside D3's
  scope.

D3 rejects all three, and infinite order is correctly not required.

### C.5 CC-0, checked carefully

**Under CT as written.** The fixture is `ℛ_0`, the superposition closure over the class `𝓘_0`
generated by `𝓑` with the architecture operations and `relabel`. The target is
`H = (X+Z)/√2` on `Fin 2`.

- **Leaves.** `X = permMatrix(swap 0 1)` is in `permClass ⊆ 𝓑`. `Z = diag(1,−1)` is in `𝓑`, as
  `IsMonomial` with `d = (1,−1)`. Both are monomial.
- **Internal node.** The closure clause applied to `(X, Z)` with `a = b = 1/√2`. Unitarity:
  `((X+Z)/√2)ᴴ((X+Z)/√2) = (X² + Z² + XZ + ZX)/2 = (2I + 0)/2 = I`, since `XZ = −ZX`.
- **Root.** `op H` gives `InstAvail 𝓘_0 (Fin 2) Unit (fun _ => Ad H)`, a D2 operation with `p = 1`
  and `H` non-monomial (`hadamard_not_monomial`).
- **Matrix content.** `Mat(ℛ_0) = ∅`: the clause names no matrix. `H` appears literally only in
  the target slot I-4, which is not rule text. The coefficients are derivation parameters.
- **Uniqueness.** The condition "`aK + bL` unitary" with `K = X`, `L = Z` has the solution set
  `{e^{iφ}(cos θ X + sin θ Z)}`. That set does not fix an operator up to a scalar, so the
  characterization bullet does not apply.
- **Verdict.** Q1 = no and Q2 = yes, so CT returns `generated` by the first row.
- **Broad reading of the Kraus bullet.** Even if `H` were placed in `Mat(ℛ_0)` because the clause
  "makes `Ad H` available" (N6), `H` sits at an internal node, not a leaf. Q1 = no and Q2 = yes
  still hold, and the verdict is unchanged.

**Conclusion.** CC-0 does not contain a supplied non-monomial matrix, and it returns `generated`.
CT can therefore return `generated`. The one defect is B2: the Step-2 shortcut literally asserts
Q2 = no for this very rule.

**Under the B1 fix.** The fix marks clause instances whose text refers to specific matrices.
`ℛ_0`'s clause is uniform over `𝓘_0` and refers to none, so no node is marked and the verdict
stays `generated`. DV-b, DV-d and DV-e each refer to stated matrices (`X` and `Z`, or
`siteSwapImage n`), so they are marked.

### C.6 Families in DV-b and DV-e

**DV-b.** If `W X Wᴴ = Z` and `W Z Wᴴ = X`, and `W'` satisfies the same, then `W⁻¹W'` commutes with
`X` and `Z`. By irreducibility it is a scalar, so DV-b fixes `H` up to a scalar. Correct.

**DV-e, `W X Wᴴ = Z` alone.** Write `W = V H`. Then `V Z Vᴴ = Z`, so `V` is diagonal, and
`W ∈ {diag(e^{ia}, e^{ib})·H}`. That is a one-parameter family modulo scalars, and every member is
non-monomial. This is the B1 gap.

### C.7 System-level `H` in `PolGen` (pointer for O-6)

`ancBlock K f e s t = K (s,f) (t,e)` (AC:457), and
`siteSwapImage 1 ((s,0),(t,0)) = hadamard s t` (C5D:196). So
`ancBlock (siteSwapImage 1) 0 0 = hadamard`, and `PolGen.block 1 _ 0 0 (PolGen.swap 1)` places `H`
in `PolGen (Fin 2)` with no `relabel`.

### C.8 Route (ii) sanity check

With `R = (1/√5)[[2,1],[1,−2]]`:
- `RZR = (1/5)[[3,4],[4,−3]] = (3Z+4X)/5`;
- `RXR = (1/5)[[4,−3],[−3,−4]] = (4Z−3X)/5`.

`R` is non-monomial and non-Clifford. This matches the reviewer reading carried in O-4.

### C.9 Owner compliance

- **Ruling 1.** The object is `polarizedTheoryC (Fin 2)` with B23 used as proved. B1–B22 and
  B24–B26 are excluded and nothing in the K-chain is reproved. Complies.
- **Ruling 2.** The monomial baseline is frozen as D1. The fiat Clifford countercontrol is CC-1, and
  it also enters CT through FC. The decisive question is CT. Complies, subject to B1–B4.
- **Ruling 3.** The commit is one file, with no Lean, computation, premise or merge, and Stage 1B is
  gated (§10.1). Complies; see N10 for the missing checkpoint.
- **"(C) is not failure."** Stated in §6. The (C) record states the existing mathematics as valid,
  states the milestone as not reached, and identifies the missing rule. The form of the missing
  rule is named, with the N1 correction.
- **Routes and shapes** are preserved (§7). Already-proved items and new obligations are separated
  (§3.1 and §3.2).

### C.10 Baseline and new obligations

**Baseline.** All monomials (`substratumClass`) is justified independently of the outcome. Reasons
1–3 of §4.1 rest on making the baseline agree with the T2 exclusion and on strictness, not on any
result. The hazard of inventory §1 shows that `permClass` would credit `S`, `Z⊗I` and `drivePhase`
to the rule while T2 excludes them.

**O-1 to O-9 are new.**
- No other kernel file uses `balancedCircuit`, `resetPerm` or `drivePhase`.
- No `PolC Work …` or `PolC (Fin 2) hadamard` lemma exists.
- No lemma states "a branch of an `InstAvail substratumClass` family that equals `p·Ad U` has `U`
  monomial". `exists_scaled_mem_of_instAvail_unitary` covers single-outcome families only.
- O-2 is a routine induction.

**O-1's plan via `classical_instAvail` (PII:168) is sound.** Each branch preserves the diagonal PSD
cone. With branch `p·Ad U` and `p > 0`, `Ad U(e_i e_iᵀ) = u_i u_iᴴ` must be diagonal for each
`i`, where `u_i` is column `i` of `U`. So `u_i` has at most one nonzero entry.
Unitarity makes it exactly one, and orthogonality puts the entries in distinct rows. Hence `U` is
monomial.

### C.11 NC and U2 (§8)

Both are stated within their hypotheses H-F1–H-F4, matching M2D. The owner's two refinements are
quoted faithfully. The non-application claim is correct:
- the polarization map is an operator identification (`swap ↦ H`), not a nonnegative frame on
  configuration laws, so H-F4 fails;
- the operations are the `InstAvail` rules, which admit non-stochastic class members, so H-F2
  fails;
- H-F1, a single fixed bijection, is also absent.

### C.12 Records

- **§A.42 item 8.** Each off-`main` reference is classified, and none is support.
  - `70815342` and `ff9c3a35…` exist and are not ancestors of `45eea51d`. They are correctly
    marked provenance; B23's proof bodies are on `main`.
  - The inventory and its reviews (comments) are used only as obligations.
  - #1198's content is not used.
- **§A.42 item 3.** The full ids `45eea51d…` and `ff9c3a35…` resolve.
- **Statuses (§9).** Three are given: *proposed*, *mathematically sufficient* and *derived from
  native OI*. The map is never promoted beyond *proposed*. They are correct.
- **No early results.** Everything beyond citations is an obligation, apart from the §6 consequence
  paragraph (N7).
- **Register and secrets.** The register is neutral. No secrets, e-mail addresses, IP addresses or
  tokens appear.

***

## D. Does the design pre-decide its outcome in a way the owner did not rule?

Partly, and openly. The design fixes CT's verdict on the object before any derivation:
- the rule enters `H` as the generator `PolC.swap` (C5D:196, PCL:153);
- that matrix is non-monomial (`siteSwapImage_not_monomial`);
- given O-1 and O-2, every D2 derivation in `PolC` uses it, and FC is yes by `PolC ⊆ 𝓕`.

CT can therefore only return `installed`, or `undetermined` if O-1 or O-2 fail. (P), (C-T1) and
`mixed` are unreachable.

Most of this comes from the owner's choices, not the writer's. The owner chose the object, asked
whether it "merely installs Hadamard behavior by definition", and said in advance what such a
finding means: the conditional mathematics stays valid and the milestone is not reached. The test's
central criterion is also principled rather than fitted to the object: a non-monomial matrix named
by the rule, in any form, is installation. CC-0 shows the test can return `generated`, so CT does
not convict every candidate.

Three elements, however, go beyond any owner ruling and should be made explicit or corrected:
1. "Characterization counts as naming" closes, in advance, every reading of the Weil
   representation as an intertwiner-defined structure. The Weil image is characterized up to
   scalar by its action on `X` and `Z`, which is DV-b. I think that is correct, since that action
   is the definition of `H`, but it is the writer's choice. It should be stated as the reason CT
   treats any formulation of the Weil clause as `installed`.
2. The (C) record's "not a generator clause" restriction (N1) narrows the missing rule beyond what
   CT entails.
3. CT's leniency toward uniform closure laws (CC-0, N8) is a choice the owner has not ruled on. It
   shifts the quantum-import question from T5 to the class disclosure.

In the other direction, the leaf-only marking (B1) is *too lenient*. Left uncorrected, it could
certify a relocated fiat rule as `generated` when the missing rule is identified.

Net assessment: on this object, MATH-CON-1's informative content is the sufficiency of T2–T4 (route
(iii)'s membership lemmas and `HDH`) and the identification of the missing rule. It is not T5. The
revised design should say so in §6, so the owner sees it before authorizing Stage 1B.

Generated by Claude Code

Applies the independent review of e593465 (REVISE): clause-instance marking with clause kinds and DV-d/DV-e (B1); restricted Step-2 shortcut (B2); row 2 of the outcome partition as the union of (C-inst) and (C-T1) (B3); CT kinds for every clause of the object (B4); N1-N14. States that on this object MATH-CON-1 tests sufficiency for T2-T4 and identifies the missing rule, and cannot settle T5. Paper only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

amaybaum · 2026-11-08T12:42:37Z

Independent re-review of the MATH-CON-1 preregistration r2 at `e2d44d7c` (model reviewer, not human): ACCEPT WITH CHANGES (1 blocking, R1)

REVIEW-MATHCON1-e2d44d7c.md

# Narrow re-review: MATH-CON-1 preregistration r2 at `e2d44d7c`

**Object.** `verification/programmes/oi-qm/reconstruction/mathcon1-polc-20261108/DESIGN.md` at
`e2d44d7cb9e29cd27b9414e98014a24b6ed94941`.
- It is a single commit whose only parent is r1 `e593465b`, and it changes only this file
  (+233/−100).
- r1 was reviewed in `REVIEW-MATHCON1-e593465b.md`, posted on #1206 as comment 6721546806.

**Scope.** I read §1.3, §4.4, §4.5, §5 and §6 in full, together with every other region the diff
touches (`git diff -U0 e593465b e2d44d7c`):
- the standing paragraph;
- the `DG` row of the kernel-file table;
- O-1, O-3e, O-6 and the new O-10 in §3.2;
- §7, §10.2, §10.3, §11, §12 and §13.

The work was read-only and on paper; hand algebra is shown in §D.

## Verdict: **ACCEPT WITH CHANGES**

There is **1 blocking finding**, R1, which is new in r2. It is a routing defect in the
rejection rules of §5, and a local edit fixes it. It must be applied before `F`. A check of the
diff suffices; no full re-review is needed. B1–B4 and N1–N14 are resolved. The writer's
deviation on N4 is sound. There are five non-blocking findings, R2–R6.

***

## A. Blocking finding

### R1. An `undetermined` CT verdict counts as *refuted* in CC-0, CC-1(b) and CC-4. That voids at order 0 the (N) that the N4 deviation exists to protect

**Location.** §5:
- the CC-0 rejection rule ("Any other verdict … Refuted, order 0");
- the CC-1 rule "(b) any other verdict: refuted, order 0";
- the CC-4 rule "Any variant classed otherwise: refuted, order 0";
- the routing paragraph ("A control is refuted when its pass condition is shown false").

**Evidence.** CC-1(b) and every DV run in CC-4 take the target `K*` (CC-4: "with target `K*`").

Suppose `K*` is not shown. §5 itself says this is exactly the ¬T2 case. Then CT has no `d*`:
- Q1 cannot be decided;
- FC is `undetermined`;
- so the verdict is `undetermined` (§4.4, the "any other combination" row).

`undetermined ≠ installed`, so on a literal reading each rule fires "refuted, order 0". Order 0
precedes (N) at order 3, so a proved ¬T2 is reported as void.

The same thing happens when `K*` exists but an obligation is only unproved:
- if O-10 is not established, DV-d's Q2 is `undetermined`;
- if O-1 is not established, Q2 is `undetermined` for every rule inside the shortcut.

In those cases the record is voided at order 0, which is reserved for a *defective* test, when it
should have fallen to (I) at order 4.

This contradicts:
- §5's own definition: "refuted" means the pass condition is *shown false*;
- the stated rationale for the N4 deviation: "Voiding at order 0 would pre-empt a legitimate (N)".

**Change required** (either fix is sufficient):
- **(a) Preferred.** In the rejection rules of CC-0, CC-1(b) and CC-4:
  - *refuted, order 0* applies only when CT returns a **definite contrary verdict**, meaning any
    of `generated`, `installed`, `mixed` or *inconsistent* other than the one the control
    requires;
  - an `undetermined` verdict is **not established**, and it routes like a vacuous control, to
    (N) if (N)'s condition holds and otherwise to (I) at order 4.

  Add one sentence to the routing paragraph to that effect.
- **(b)** Alternatively, state that CC-0, CC-1(b), CC-2(b) and CC-4 bear only on T5. A refutation
  of any of them then excludes (P) and (C) only, through Ctrl, and does not void (N). Under
  §6's mapping, (N) does not use T5.

***

## B. Status of r1's findings

| r1 finding | Status at `e2d44d7c` | Note |
|---|---|---|
| **B1** leaf-only marking; scalar-unique characterizations; CC-4 cannot fail | **Resolved** | See below |
| **B2** shortcut contradicted by CC-0 | **Resolved** | The shortcut is restricted to rules whose clauses are all I-f or G-n of the admission form. `ℛ_0` (G-u) is explicitly outside it, and the CC-0 recheck subsection records why the shortcut and the exhibited `d'` no longer conflict. The shortcut argument via O-2 then O-1 is valid (§D.3) |
| **B3** row 2 overlaps (I) | **Resolved** | Row 2 is now `Ctrl ∧ T2 ∧ T3 ∧ T4 ∧ [(CT ∈ {installed, mixed}) ∨ (CT = generated ∧ two rules)]`, exactly the union of (C-inst) and (C-T1). Row 4 lists the cases with CT `undetermined` and with T1 undetermined. I checked that the partition is total and disjoint (§D.5) |
| **B4** no clause kinds | **Resolved** | §1.3 has a kind column with reasons fixed from the text alone. A-3 and A-4 are I-f; A-1 and A-5–A-7 are G-n of admission form; A-8 is G-u (shared); A-2 is the shared reference interface. The tagging is consistent with the §4.4 definitions, and the "Consequence of the kinds" paragraph correctly places the object inside the restricted shortcut. `PolC` is by its inductive definition the least label-invariant architecture containing `permClass` and the two images (PCL:150–162) |
| N1 form of the missing rule | Resolved, with a residue | See R2 |
| N2 CC-2(b); O-6 pointer | Resolved | (b) now applies only when `K*` is available in both theories. The pointer is carried in O-6 as a reviewer reading. PCL:731–733 is the correct citation; my r1 note "PCL:734" was off by one |
| N3 CC-3(b) | Resolved | It is now a recorded definitional calibration, and it is correctly marked as unable to fail |
| N4 CC-1 rejection text | **Resolved by a different route; the deviation is sound** | See §C |
| N5 witness for Q2 | Resolved | |
| N6 scope of the Kraus and effect bullets | Resolved | I-3 is limited to channels, instruments and effects that the clause itself states, and channels obtained only by derivation are excluded |
| N7 conditional consequence; reachability | Resolved | The consequence is conditional on O-1 and O-2. The reachable outcomes are (C-inst) with `installed`, (N) and (I), and `mixed` and (C-T1) are excluded with reasons. The routing when an obligation is refuted or not established is stated, though it depends on R1 |
| N8 what CC-0 calibrates | Resolved | The class disclosure sits beside the verdict, and §4.5 item 3 covers it |
| N9 depth form | Resolved | O-3e states `(1 − (3/8)^k)·Ad(HDH) + (3/8)^k·id`. The formula is correct (§D.4) |
| N10 gate checkpoint | Resolved | Added to §10.2 |
| N11 shapes 1–2 | Resolved | §6 item 3 |
| N12 exactness notes | Resolved | O-3e |
| N13 O-1 template | Resolved | `conj_diag_entry` is at DG:90 and `diagonalGlue_forces_monomial` at DG:101, both checked at `45eea51d`. `DG` was added to the kernel-file table with a link pinned to `45eea51d` |
| N14 the (I) remainder | Resolved | |

**B1 in detail.**

*The clause kinds G-n, G-u, I-f and I-m.*
- G-n now covers literals, formulas, maps at stated inputs, relabellings and scalar multiples.
  It also covers conditions that mention stated matrices *whether or not they are unique*, and
  closure steps that combine class members with a stated matrix (`K ↦ K·M`).
- G-u covers only laws that are uniform over all class members and name no matrix.
- I-f has no node.
- I-m marks every node that uses one of the clause's own stated non-monomial matrices.

*Marking.* Every node is now subject to marking, leaf or internal. This closes both evasions
named in r1, the constant inside a closure step and the family characterization.

*CC-4.* It gains DV-d (a constant inside a closure step) and DV-e (a family characterization).
A leaf-only marking would misclass both, so CC-4 can now fail if CT regresses. Under the frozen
rules, both DV-d and DV-e return `installed` (§D.1–§D.2), conditional on O-1, O-2, O-10 and on
`K*` existing; that last condition is R1.

*CC-0 recheck.* `ℛ_0` is G-u and `Mat(ℛ_0) = ∅`. Its leaves `X` and `Z` are monomial, and its
single superposition node is G-u, hence unmarked. So Q2 = yes and CT returns `generated`. My own
·r·echeck agrees (§D.3).

***

## C. The writer's deviation on N4

In r2, if CC-1(a) is not shown, CC-1 is *vacuous, not a pass*. It routes to (N) when (N)'s
condition holds and to (I) otherwise; it does not go to order 0. **This is sound, and better than
my r1 wording.**

1. **(N) does not depend on CC-1.** (N) needs ¬T2 at the support standard. ¬T2 depends only on
   the class `PolC` and on D2 and D3. CC-1 tests CT, and CT bears only on T5, which the (N) row
   does not use. A fiat-control comparison that cannot be run because `K*` does not exist carries
   no evidence against a proof of ¬T2. The control that guards D2 is CC-3(a), and it still voids
   at order 0 when refuted.
2. **The other route is also correct.** CC-1(a) can also fail to be shown because O-2 is unproved
   while T2 holds. Then the control is not a pass, so Ctrl fails, so (P) and (C) are excluded.
   (N)'s condition is false because T2 holds, so the outcome is (I). That is right: without the
   fiat comparison, `installed` cannot be certified.
3. **A refuted CC-1(a) still voids.** "`K*` shown in `polarizedTheoryC` but not in `𝔉`" means
   O-2 is false, which is a defect, and it still goes to order 0.

The deviation holds only if CC-1(b) and CC-4 do not themselves void the ¬T2 case. As written they
do (R1). With R1 applied, the routing is consistent.

***

## D. Hand checks

### D.1 DV-d returns `installed`

DV-d is the G-n closure step "if `K ∈ 𝓘` on `Fin 2 × Fin n`, then `K·S_n ∈ 𝓘`", with
`S_n = siteSwapImage n = H ⊗ I_n`. Its base is `permClass`, the shear image and the shared
constructors.

**Q2 = no, by O-10.** Take a derivation with no marked node. All leaves are monomial, and every
shared constructor preserves monomiality (SC:231, SC:275). At a DV-d node with monomial input
`K`, each nonzero row of `K` has a single entry at some column `c`. The corresponding row of
`K·S_n` is that entry times row `c` of `H ⊗ I_n`, which has two nonzero entries. So `K·S_n` is
non-monomial unless `K = 0`, and that node would be marked.

By induction, every class node is monomial. Each node's `InstAvail` realization is then in
`substratumClass`, and O-1 gives no D2 branch. So every D2 derivation has a marked node.

**The other two components.**
- Q1 = yes: `d*` builds `S_n` as `1·S_n`, a marked node.
- FC = yes: `NM(DV-d) ∋ S_n`, so `𝓕_DV-d ⊇ 𝓕 ⊇ PolC`.

**Verdict:** `installed`.

O-10 is valid as a proof method. One minor wording point: "the first node" should read "a node
whose child nodes all carry monomial matrices" (R5).

### D.2 DV-e returns `installed`

DV-e states the swap layer as "some unitary `W` with `W X Wᴴ = Z`", stated at every level `n` with
the ancilla a spectator.

**The family.** Write `W = V·H`. Then `V Z Vᴴ = Z`, so `V` is diagonal. The family is
`{diag(e^{ia}, e^{ib})·H}`, and every member is non-monomial (each row has two nonzero entries).

**The verdict.**
- The clause is G-n of admission form, so the restricted shortcut gives Q2 = no.
- `a = b = 0` gives `H ⊗ I_n = S_n` in the class, so `K*`'s `PolC` derivation transfers.
- Q1 = yes, at the `S_n` admission node.
- FC = yes, because `𝓕_DV-e ⊇ 𝓕`.

**Verdict:** `installed`.

### D.3 The CC-0 recheck and the restricted shortcut

**CC-0.**
- Leaves: `X = permMatrix(swap 0 1)` and `Z = diag(1,−1)`, both monomial.
- One G-u node with `a = b = 1/√2`, which is unitary:
  `((X+Z)/√2)ᴴ((X+Z)/√2) = (2I + XZ + ZX)/2 = I`.
- Root: `op H`.

No node is marked, so Q2 = yes and CT returns `generated`. G-n's clause "a condition that
mentions stated matrices" does not capture `ℛ_0`, because its condition quantifies over the class
and states no matrix. That is the G-u/G-n boundary as defined.

**The restricted shortcut.**
1. A derivation with no marked node uses only *monomial* admitted matrices and the shared
   constructors.
2. By O-2 (SC:231, SC:275), every class node therefore lies in `substratumClass`.
3. The `InstAvail` family is then in `InstAvail substratumClass`, by the same induction as
   `instAvail_mono`.
4. By O-1 it has no D2 branch.

This is valid.

### D.4 The O-3e depth form

`Ad H ∘ [(1−(3/8)^k)·Ad D + (3/8)^k·id] ∘ Ad H = (1−(3/8)^k)·Ad(HDH) + (3/8)^k·id`, because
`Ad H ∘ Ad H = Ad(H²) = id`. This is correct.

### D.5 The partition

- **Order 0:** a refuted control, an inconsistent CT, or a proof of both T2 and ¬T2.
- **(P):** needs Ctrl, T1, T2–T4 and `generated`.
- **(C):** needs Ctrl, T2–T4, and either `installed`/`mixed` or `generated` with two rules.
- **(N):** needs ¬T2, and it does not need Ctrl.
- **(I):** the remainder.

Disjointness:
- (P) and (C) differ on CT or on T1.
- (N) and (P)/(C) differ on T2, and a proof of both T2 and ¬T2 is caught at order 0.

So the partition is total and disjoint. Rows 1 and 2 require Ctrl, so a vacuous or unestablished
control falls to (N) or (I), as §5's routing states. R1 is the one place where §5's rejection
rules disagree with that routing.

### D.6 Records

- The commit changes one path.
- All 18 blob links and the one tree link are pinned to `45eea51d`, and the new link is the `DG`
  row.
- The read-write-sourced identifier is absent.
- The new kernel citations (DG:90, DG:101, PCL:731–733) match `45eea51d`.

The new §10.2 checkpoints are each measurable:
- the Stage 1B gate quotes the authorizing comment with its time and precedes the first commit;
- the kinds column is frozen through the existing diff checkpoint;
- CC-0, DV-d and DV-e are reported in the control table;
- the class column sits beside the verdict.

### D.7 §4.5, the three choices the owner has not ruled on

All three are explicit:
1. a characterization counts as naming, including family characterizations, so every formulation
   of the Weil clause is `installed`;
2. the CT-entailed form of the missing rule is kept apart from the owner-worded form;
3. uniform closure laws are treated leniently.

The section's preamble marks all three as the writer's choices, "stated here so that the owner
can rule on them". Item 3 adds that the owner has not ruled on it. §6's closing paragraph and §12
repeat that the three are not owner rulings. This meets r1 §D.

***

## E. Non-blocking findings

### R2. I-f is listed as a possible form of the missing rule, but an I-f clause cannot yield a D2 operation

**Location.** §4.5 item 2; §6, "Identifying the missing rule", item 2.

An I-f clause leaves A-2 formally unchanged and has no node (§4.4). A single I-f rule therefore
gives a theory formally identical to the one without it, which has no D2 operation. Drop I-f from
the CT-entailed form, leaving "a G-u law, or an I-m clause whose stated matrices are monomial".

### R3. §10.1 says "Lean membership proofs O-1 to O-9", but r2 adds O-10

**Location.** §10.1, line 650. Change it to "O-1 to O-10".

### R4. §11 cites my r1 review by its session-scratchpad path

**Location.** §11, the last row.

A scratchpad does not last. Cite the durable copy instead: #1206 comment 6721546806.

### R5. Two small wording points in §4.4

**Location.** §4.4, the kinds table and Step 1; §4.4 Step 2 and §3.2 O-10.
- G-n and I-m nodes can carry *channels*, but the marking condition says "carries a non-monomial
  matrix". Write "a non-monomial matrix or channel, in the sense of I-3".
- O-10's "first node" should read "a node whose child nodes all carry monomial matrices".

### R6. Cosmetic

**Location.** §10.3: H-5 is listed before H-4. Move H-5 to the end of the list and keep both
identifiers as they are.

Note

Claude's GitHub safety filter added the · characters above so that a bot command in this comment does not run automatically. A person who wants it to run can post the command without the · characters.

Generated by Claude Code

Applies the re-review of e2d44d7 (ACCEPT WITH CHANGES): R1, only a definite contrary CT verdict refutes CC-0, CC-1(b), CC-2(b) and CC-4, and `undetermined` is not established and routes to (N) or (I); R2, I-f dropped from the CT-entailed form of the missing rule; R3, O-1 to O-10; R4, review citations to the #1206 record; R5, marking and O-10 wording; R6, hazard order. Section 13 extended. Paper only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

amaybaum · 2026-11-08T12:44:11Z

Transcription note for comment 6721629501 (the r2 re-review of MATH-CON-1 at e2d44d7c).

One line of the stored comment differs from the review file. Fenced line 116, in the "CC-0 recheck" paragraph of section B, is stored as ·r·echeck agrees (§D.3). The file reads recheck agrees (§D.3).

Cause: two middle dots (U+00B7) were inserted in transit. The posted bytes were correct, the same rewrite came back after one corrective edit, and the comment was then left as stored.
Rest of the comment: byte-identical to the review file.
Source file: sha256 3f4afa873566862172554bc82b7a92779bc8ed4928b674c1b863fb554e787723, 15,322 bytes.

Generated by Claude Code

amaybaum · 2026-11-08T12:44:16Z

Confirmation of the MATH-CON-1 preregistration r3 at `41a42cb9` (model reviewer, not human): ACCEPT

CONF-MATHCON1-41a42cb9.md

# Diff check: MATH-CON-1 preregistration r3 at `41a42cb9`

**Object.** `41a42cb97e5e044f5a9e906e33fbf6f22de52dc4`.
- It is a single commit whose only parent is `e2d44d7c`, and it changes only `DESIGN.md`
  (+31/−17).
- I checked `git diff e2d44d7c 41a42cb9` against the findings of the re-review in
  `REVIEW-MATHCON1-e2d44d7c.md`.
- Read-only.

## Verdict: **ACCEPT**

R1–R6 are applied, and the diff introduces no new defect. One optional wording point follows
(§3); it does not block.

## 1. R1 (blocking at r2): resolved

§5's routing gains a bullet. For the controls whose pass condition is a CT verdict, namely CC-0,
CC-1(b), CC-2(b) and CC-4:
- only a *definite contrary* verdict refutes the control, which then goes to order 0;
- `undetermined` means the control is *not established*, and it routes to (N) or to (I);
- the bullet names the two sources of `undetermined`: `K*` not shown, so CT has no `d*`; and an
  unproved obligation such as O-1 or O-10.

Each rejection rule now matches that bullet:

| Control | Required verdict | Refuted by (order 0) | `undetermined` |
|---|---|---|---|
| CC-0 | `generated` | `installed`, `mixed` or inconsistent | not established |
| CC-1(b) | `installed` | `generated`, `mixed` or inconsistent | not established |
| CC-2(b) | the same verdict for `PolGen` and `PolC` | two definite verdicts that differ | not established |
| CC-4 | `installed` for each DV | `generated`, `mixed` or inconsistent | not established |

Consequences, checked against §6, which is unchanged:
- **Under ¬T2 proved.** CC-1(b) and CC-4 are `undetermined`, hence not established. No control is
  refuted, so order 0 does not fire, and row 3, (N), applies. The case R1 identified is fixed.
- **No positive outcome can pass through `undetermined`.** Rows 1 and 2, (P) and (C), require
  **Ctrl**, the condition that every control has *passed*. A control that is not established
  therefore never yields (P) or (C). A defective CT that hides behind `undetermined` can lower the
  outcome to (I), but it can never raise it.
- **The genuine defect cases still void.** A refuted CC-3(a), a refuted CC-1(a), and CT returning
  inconsistent all still go to order 0.

## 2. R2–R6: applied

| Finding | Check |
|---|---|
| R2 | I-f is removed from the CT-entailed form of the missing rule in §4.5 item 2 and §6 item 2, with the reason given: an I-f clause leaves A-2 formally unchanged, so it cannot yield a D2 operation. The CT-entailed form is now a G-u law, or an I-m clause whose stated matrices are monomial. Correct |
| R3 | §10.1 reads "O-1 to O-10" |
| R4 | §11 cites the r1 review as #1206 comment 6721546806. The r2 re-review is added as provenance |
| R5 | The kinds table (G-n and I-m rows) and Step 1 now say "non-monomial matrix or channel, in the sense of I-3". O-10, in §3.2 and in Step 2, now reads "a node that carries a non-monomial matrix while all its child nodes carry monomial matrices". This statement is correct: it is the contrapositive of monomiality preservation, applied at such a node |
| R6 | In §10.3, H-4 now precedes H-5, and both identifiers are unchanged |

§13 records R1–R6 with their changes, and each entry matches the diff.

## 3. Optional (does not block)

- **§6 line 566.** It reads "The image would instead have to follow from a G-u law or an interface
  clause." After R2, "interface clause" there can only mean an I-m clause. Writing "or an I-m
  clause whose stated matrices are monomial" would match §4.5 item 2.
- **§11, the r2 re-review row.** If the r2 re-review has a comment id on #1206, cite it, as the r1
  row does.

Generated by Claude Code

amaybaum · 2026-11-08T12:46:01Z

MATH-CON-1 Stage 1B (first stage), §4.5 choices and CONS-0 corrections (owner decision, chat, 2026-11-08)

The owner (amaybaum) decided this in chat with the coordinating session on 2026-11-08: "I approve all three recommendations, with explicit boundaries to preserve the scientific rigor of the OI–QM equivalence programme."

1. MATH-CON-1 Stage 1B: option (a) approved

Authorize the first stage only: O-1, O-2, and O-3a–e.

The objective is to establish whether the proposed construction works mathematically at this level, while explicitly recognizing that Hadamard is supplied rather than derived.

Conditions:

Freeze F before execution.
Require exact-head CI at F and E, with the prescribed receipt.
Do not execute O-4 through O-10 without separate authorization.
Do not claim that OI independently generates the quantum operation.
A successful first stage establishes only a candidate for outcome (C). The complete outcome still depends on the remaining obligations, including valid instruments and repeatable composition.

The design is the MATH-CON-1 preregistration, accepted at 41a42cb9 (#1206).

2. MATH-CON-1 §4.5: all three choices accepted

Approve the three design decisions as recorded. In particular, I agree that characterizing Hadamard indirectly still counts as installing it. Uniform closure laws may remain unmarked, provided they do not explicitly identify a particular non-monomial matrix.

Important distinction: passing the calibration control must not be presented as evidence that such a closure law is independently physically justified. That remains a separate question.

3. CONS-0: corrections approved

Finding	Decision
F1 — Substratum:459	Narrow the claim. Distinguish information conservation from energy conservation, and state the additional dynamical assumptions required.
F3 — GR:699	Narrow the claim. Explicitly identify the energy shell as an assumption, not a consequence of Lemma 3.
F2 — SM Theorem 22	Leave unchanged. Record the potentially unnecessary assumption as a note for future investigation.

Authorize one correction PR covering F1 and F3, including all applicable mirrors and regenerated .tex and .pdf outputs. Require an independent review, green CI, and a separate merge decision. No additional scientific claims or theorem strengthening are authorized.

Overall direction

The owner distinguishes three questions:

Mathematical construction: can the extended framework reproduce the desired quantum operation?
Independent physical justification: can the needed rule be motivated without inserting the desired quantum answer?
OI derivation: does that rule follow from OI itself?

MATH-CON-1 is currently addressing the first question. Success there must not be promoted to success on the second or third.

These authorizations do not change the existing conditional approval for #1201 or its dependency on green main CI following #1198.

Generated by Claude Code

amaybaum · 2026-11-08T13:15:32Z

Independent review of the MATH-CON-1 Stage 1B round plan and draft preregistration (scratchpad, not yet in the repo; model reviewer, not human): REVISE

REVIEW-PLAN.md

# Independent review: MATH-CON-1 Stage 1B first-stage round plan and draft control plane

**Objects reviewed:** `PLAN.md` and `preregistration.draft.md` in this directory, as they stood on 2026-11-08.
**Reviewer:** an independent Claude Code agent. I did not write either object. I made no writes outside the scratchpad.
**Read:**
- the owner decision #1169 c.6721662886 (amaybaum, 2026-11-08T12:46:00Z);
- `DESIGN.md` at `41a42cb9` (blob `27359cbd…`, 760 lines);
- from `origin/main` = `b73acf38a7c6`:
  - `architecture.md` (`K1`, `S2`, `G9`, `G7`, `S3`, `G11`, `S7`, `K2`, `G6`, `S9`, `K3`, `G13`);
  - `tools/v3_verifier.py` and `tools/v3_receipt.py`;
  - `verify.yml`, `release_gate.py`, `duplicate_check.py` and the census;
  - KTRANS-SEP-2's preregistration, receipt and `controls.py`;
  - the kernel sources the frozen statements consume: BFP, PCL, PII, IL, SC and C5D.

## Verdict: **REVISE**

The **route is right, and I accept it as drafted.** The draft preregistration has five blocking defects. All of them sit
in text that freezes at `F`, so they cannot be fixed after it. Each one is cheap to fix while drafting. One of them
(B1) would make every outcome VOID. Re-review the revised draft before a candidate `F` is held.

## Independent reproductions

1. **Verifier probe.** I rebuilt the writer's scratch repository from my own script. It ran the real `v3_verifier.py`
   and `v3_receipt.py` from `origin/main`, with the draft preregistration verbatim. The probe script is
   `/tmp/claude-0/-home-user-incompleteness/57e93868-2ccb-5ebd-afb7-d31826198729/scratchpad/mathcon1-review-probe/`.

   | case | result |
   | --- | --- |
   | clean complete path | `VERDICT  HOLDS`, governed-paths digest `81897a90…5e107`, equal to the writer's |
   | `DESIGN.md` edited in execution | `FAILS  s3:unauthorized, s9:landing-unauthorized` |
   | census conflict at reconciliation, listed in `--resolved` | `HOLDS` |
   | halted path (`W` restores the five execution paths and keeps `result.md`; `F` attestations only) | `HOLDS` |
   | `D` = the design commit, landed as a merge's second parent (the `D = 41a42cb9` alternative) | `FAILS  s9:d-not-on-first-parent-chain` |

2. **Exact truth of the frozen O-3a/O-3e statements.** This is a check of my own, in Gaussian rationals.
   - `balancedCircuit = (I⊗H⊗H)·Toff·(S⊗I⊗I)·Toff·(I⊗H⊗H)` holds exactly, with Toffoli controlled on register value 3
     (`bc = 11`, CH1:102–104).
   - The word without `S` differs.
   - `HDH = [[4/5+2/5i, 1/5−2/5i], [1/5−2/5i, 4/5+2/5i]]` is unitary and non-monomial.
   - `HDH·Z·HDHᴴ = (3/5)Z − (4/5)Y` is not proportional to any Pauli, so the non-Clifford witness is `P = Z`.
     `P = X` is fixed.
   - CAL: `drivePhase` passes the non-Clifford clause, with `P = X`.
   - `H` and `HSH` are Clifford.
   - `Z⊗I = (siteShearImage 4)²`.
   - O-1 is provable on the stated route: `classical_instAvail` (PII:168) gives per-branch preservation of the diagonal
     PSD cone, for a general carrier `S`.

3. **Drift.** `git diff 45eea51d b73acf38` under `verification/lean-mathlib`, `verification/lean`, `.github` and
   `tools` is empty.

## 1. The route

Each "cannot" claim holds against the verifier source:

| claim | verified by |
| --- | --- |
| #1206 cannot be the round PR | `control_plane()` and `check_t1()` count only `.+/(preregistration\.md\|amendments/.+)`. Each #1206 commit changes `DESIGN.md`, giving `t1:non-control-plane-change` (`S2`, `G9`). Under §A.43 item 3, a re-cut is possible in principle, but it would not help: `DESIGN.md` is not a control-plane file under any name. |
| `D ≠ 41a42cb9` | `check_first_parent_chains()` (`K3`); probe case 5 |
| the blocks cannot sit in an amendment | `t1:block-in-amendment`, plus the count rules for blocks in the preregistration (`K2`, `G10`) |
| use a sibling record directory, not the design's | `records_unchanged()` (`G13`) compares every path under the record-directory prefix. A later `RESULT.md` or `amendments/` in the design's directory would fail `g13:record-directory-changed`. |

**Is landing #1206 first required? Yes.**
- V3's mechanics force it, not only §A.42:
  - `DESIGN.md` must already be in `D`'s tree, because `delta(D, F)` may carry only control-plane files (T1);
  - an ungoverned `DESIGN.md` in the landing delta fails `s9:landing-unauthorized`;
  - control DS reads it at S1 and `E`.
- The verdict's premises (D1–D3, the obligations, CC-3(a) and CC-1(a)) are *support* under §A.42 item 8, and must be
  on `main` no later than the record.

**No simpler valid route exists.** The only alternative is the writer's fallback, which embeds the design. It is valid
under V3, but it duplicates the design, and the owner-accepted object still lies off `main` until #1206 lands. The
recommended route is the minimal valid one. Two conditions on step 0 are in N9 and N11.

## Blocking findings

**B1. S4 and V contradict each other, so every outcome reads VOID.**
- V requires the result note to carry "the owner boundaries quoted".
- S4 screens the note "outside its two frozen texts" for phrases such as "OI independently generates" and
  "physically justified".
- The quoted owner boundaries contain exactly those phrases:
  - "Do not claim that OI independently generates the quantum operation";
  - item 2's "independently physically justified".
- A correct note therefore fails S4, and `verdict` prints VOID on every outcome. The self-test's positive controls
  contain no generated note, so they would not catch this.

*Fix:*
1. Make the quoted owner boundaries a third frozen text, excluded from S4 like the other two. Check it under V,
   whitespace-normalized.
2. Add positive self-test cases that generate the complete note under CANDIDATE-C and under HALTED and pass S4 and V.

**B2. The per-cell negative tokens cannot be computed from structured data (§A.44), and KC's VOID collides with the
cells.**
- Gate A is one step over all 26 reports. Its conclusion, and M's, say only that *some* report lies outside the three
  axioms.
- The cell rule "NOT-ESTABLISHED when one of *the cell's own* reports lies outside" therefore needs the log text,
  which §A.44 forbids.
- For the same reason, `verdict` cannot tell a failing §G report (to be VOID) from a failing cell report (to be
  NOT-ESTABLISHED).
- Transitive `#print axioms` closure also makes per-cell attribution misleading:
  - O-3d and O-3e consume O-3a–c;
  - `class_hypothesis_needed` is O-3e's conjunction (see N3).
- The seven PROVED tokens are likewise one bit read seven times. That is acceptable only if the note says so.

*Fix,* either of:
- **(a), recommended:** follow KTRANS-SEP-2. Any complete-nonstandard report gives every kernel cell, and KC,
  `NOT-ESTABLISHED`, with no per-cell attribution, and the stage halts. State that the PROVED tokens share one gate.
- **(b):** `controls.py axioms` writes one step output per cell and one for KC, and the workflow carries one marker
  step per cell, each with an `if:` on its output. The verdict then reads per-cell step conclusions, and the
  attribution caveat is stated.

**B3. The frozen surface is incomplete for two load-bearing definitions.**
- `MonoExt` and `FiatC` carry their constructors only as comments. They are not listed among the `PENDING` items, and
  precondition 2 does not cover them.
- O-2's faithfulness depends on their exact constructor lists, and so does CC-1's `𝓕` = "the least label-invariant
  architecture containing `𝓑 ∪ {siteSwapImage n}`". So does the meaning of `polC_le_fiatC`: a stray `PolC`-style
  constructor would make it trivial.

*Fix:*
- Freeze both inductives in full Lean text before `F`, with the same binder forms as `PolC`.
- Freeze `ancillaHH` and `toffoliToken` in full as well. Pin the Toffoli control on register value 3: the O-3a
  identity fails for any other encoding.
- Add a self-test mutation for each of them: an extra `FiatC` constructor, a changed `toffoliToken` control value, and
  a changed `ancillaHH`.

**B4. The frozen earned reading says more than the frozen theorems.**
1. "its stopped channel at every finite depth k **is** (1 − (3/8)^k)·Ad(HDH) + (3/8)^k·id". No frozen theorem states
   an equality about a stopped loop. `conjugated_finite_available` states only that this channel is available.
   *Fix:* reword the reading to "the channel … is available at every finite depth k", or add a frozen equality
   theorem. The identity is true, but adding it is a scope decision, so the reword is preferred.
2. "In the monomial baseline every available instrument, at every carrier, has only monomial unitary branches" can be
   read as saying every branch is a unitary conjugation. O-1 proves only that a branch equal to `p·Ad(U)`, with
   `p > 0` and `U` unitary, has `U` monomial. *Fix:* state exactly that.
3. "non-Clifford" should read "non-Clifford in the sense of D3".

These texts freeze at `F` and are printed under CANDIDATE-C, which makes this a claim/evidence-boundary defect.

**B5. "Proofs only may change", together with N1, leaves no policy for auxiliary declarations or `set_option`.**
- N1 admits no declaration outside the frozen list.
- Several proofs will naturally want named helpers:
  - O-1's rank-one-indicator column argument;
  - the carrier `Equiv`s for the `relabel` routes of `ancillaHH`;
  - the `Fin 2 × Fin 1 ≃ Fin 2` transport for `polC_hadamard`.
- B23's own branch proof needed `set_option maxHeartbeats 2000000 in`, and N3 forbids "set_option that weakens
  checking" without defining it.
- So the round can halt for a reason that is not mathematical, and no amendment is possible after `F`. That would put
  an engineering artifact where §A.29 expects a measured verdict.

*Fix:* before `F`, freeze an auxiliary policy:
- `private theorem` declarations, theorem kind only, under a frozen name prefix such as `aux_`;
- no new `def`, `instance`, `inductive`, `abbrev`, notation or attribute;
- hygiene N3 applies to them;
- they are covered through the frozen theorems' `#print axioms` closure, with no print lines of their own (S5
  unchanged);
- an explicit `set_option` allowlist: `maxHeartbeats` and `maxRecDepth`, `in`-scoped only.

Add self-test cases: an allowed `aux_` lemma passes; a `private def` fails; and a `set_option` outside the allowlist
fails. N2's elision must then be specified precisely: theorem proofs elided; `def` and `inductive` bodies, the `open`
line and `#print` lines kept verbatim.

## Non-blocking findings

**N1. O-1 is frozen at a general carrier.**
- `monomial_of_coherentBranch` is stated for every finite `S`. That is strictly more general than the design's "for
  the system carrier and for every level", which `baseline_level_no_coherentNonMonomial` and `S = Fin 2` cover.
- The proof is the same, so it is not scope creep. The scope table should still say that the general carrier form is
  the means and the system and level forms are the obligation.

**N2. CC-1(a) is listed as "passed, kernel", but no frozen theorem states it.**
- It follows by composing `instAvail_polC_fiatC` with `conjugatedAttempt_available`.
- Either add `fiatC_conjugatedAttempt_available : InstAvail FiatC Token (Fin 4) conjugatedAttempt`, which is O-2's
  transfer clause, or write "follows from O-2 and O-3e by composition".

**N3. KC scope.**
- The three §G countercontrols, the exact layer and CAL are controls of the authorized cells, as §A.29 requires. They
  execute no part of O-4 to O-10 and no CT. I judge them **within scope**.
- CAL is the design's CC-3(b), a recorded definitional calibration. It is distinct from the CC-0 calibration in the
  owner's item 2. Keep that distinction explicit.
- `class_hypothesis_needed` restates O-3e (`⟨conjugatedAttempt, _, _⟩`). It witnesses that O-1's hypothesis is
  load-bearing, but it is not an independent control. Do not present it as one.
- Put the R9 confirmation into the owner's `F` request (N11).

**N4. Self-test remnants.**
- "a sixteenth print (S5)" is a KTRANS-SEP-2 remnant. The draft has 26 theorems, so this should be a twenty-seventh
  print.
- Add mutation cases for the definitions: `hdh`, `conjugatedAttempt`, `NonClifford` (for example, `pauliY` added to
  the `P` set) and `CoherentNonMonomialBranch` (for example, `p ≤ 1` dropped).

**N5. XS does not cover everything X3 reconstructs.**
- X3 recomputes the attempt from reset, circuit, readout, correction and discard.
- XS should therefore also pin `attempt`, `correctedReadout`, `resetChannel`, `readProj`, `uniformAttach` and
  `discardWith`/`ptraceAnc`. It should tie the checker's `ancillaHH`, `toffoliToken` and `hdh` to the module's frozen
  definitions.

**N6. The exact layer's evidence form.**
- An uncaught exception exits 1, the same status as a failing check.
- Follow KTRANS-SEP-2: freeze the expected output digest, and decide "complete" from that output, or from distinct
  exit statuses (for example, 0 for pass, 3 for complete with a failure, anything else VOID).
- Run the checker on the staging branch before `F`, so that the frozen statements are known to be true (reproduction 2
  agrees).

**N7. The negative route and the unproved halt.**
- State, as KTRANS-SEP-2 does, that a kernel NOT-ESTABLISHED arises only from the `sorryAx` that Lean's error recovery
  records, and that a literal `sorry` fails N3 and gives VOID.
- For "a statement cannot be proved as frozen":
  - name who decides, and when (for example, a recorded halt decision on the PR);
  - freeze the halted note's wording as "not proved in this round; open". Under the review rules, failure to recover a
    proof is not disproof. This maps to the design's "not established", routed to (I).
- The stop-rule bullet on a §A.26 anomaly says "measurements stop until resolved". That is a pause, not a halt.
  Separate it from the halt list.

**N8. §A.41 gaps.** Several asserted properties have no checkpoint:
- the checker uses the standard library only, reads no file and imports nothing from the repository;
- `controls.py` imports nothing from the repository and changes nothing.

*Fix:* add a static import-allowlist check under B or X. Separately, the checkpoint for "designation before S1" uses
the commit date, which the author sets. Use host timestamps instead: the designation comment's `created_at` against
S1's first push or run `created_at` from the API.

**N9. Step 0 merge method and identifiers (§A.42 item 3).**
- #1206 must land as a merge commit, not squash or rebase, so that `41a42cb9` (the commit the owner accepted) is
  reachable from `main`. Recent landings are merge commits; make it explicit.
- Replace `13340732fe…` and `b73acf38a…` with full ids.

**N10. Reconciliation.** "This round's four steps stay last" is not required: each round's verdict reads its own `E`
run, and the KTOKEN live constraint is retired (confirmed). Resolve by merits, keeping both rounds' blocks.

**N11. Owner-approval list.** The list is correct as far as it goes: step 0; the dispatches at `F`, S1 (optional) and
`E`; the `F` and `E` designations; and the landing. Add:
1. In the step-0 request, the owner's ruling on the sibling record directory, which departs from DESIGN §10.1's
   "`RESULT.md` in this directory" and its `amendments/`.
2. In the `F` request, the R9 confirmation that the controls are in scope.
3. Every re-dispatch after a VOID or a replaced `E` candidate needs its own approval, at about six CPU-hours each.
4. Record a designated writer in #1169's planning block (§A.45 rule 3).

**N12. Cost.** About 18–20 CPU-hours for three dispatches is acceptable under §A.40, because all of it runs in CI. The
A42 exclusion matrix (about six CPU-hours per `workflow_dispatch`) dominates, which the `verify.yml` comment confirms.
The S1 dispatch follows the KTRANS-SEP-2 precedent but is optional.

**N13. Mechanics confirmed.**
- The governed-path block matches the KTRANS-SEP-2 and OI-FINITE-PROTOCOL-1 templates: no gaps, no over-broad
  entry, and no ROADMAP entry.
- The census family is `kernel-only` with `manuscript: []`, matching 92 existing families.
- The shard and aggregate splices follow `probes_ktranssep2`. The four bridge steps follow KTRANS-SEP-2's §A.44 form.
- Only `bg2-orientation-design.yml` and `bridge-compatibility-research.yml` trigger on pushes to non-`main` branches,
  and both are path-filtered. Neither fires, and `verify.yml` pushes only on `main`.

**N14. `DESIGN.md`'s standing line is stale.** It says "Revision r2" and "WIP / UNVERIFIED". Landing the blob
unchanged is correct, because the owner accepted those bytes. The round's preregistration records the acceptance, as
the draft does. Finalize the draft's own "Status: drafting" header in the last pre-`F` commit.

## Scope check (item 2), summary

- **Authorization.** The draft authorizes only O-1, O-2 and O-3a–e. It carries the non-inference rule always, and its
  stage token stops at `MATHCON1-S1B1-CANDIDATE-C`.
- **The statements against the design.** The frozen statements match O-1, O-2, O-3a–e and D2/D3 faithfully:
  - `NonClifford` matches D3;
  - `CoherentNonMonomialBranch` matches D2;
  - `MonoExt` and `FiatC` match the design's `𝓑`-closure and `𝓕`, subject to B3;
  - O-3d/O-3e follow the design's route.
- **Nothing extra** beyond the KC controls (N3) and the general-carrier O-1 (N1).
- **The non-inference rule** lists O-6, O-8, O-9 and O-10 as needed for (C). That is a defensible reading of design §6.

Generated by Claude Code

amaybaum · 2026-11-08T13:28:19Z

Independent re-review of the MATH-CON-1 Stage 1B round plan and draft preregistration r2 (scratchpad; model reviewer, not human): ACCEPT WITH CHANGES (1 blocking, R2-B1)

REVIEW-PLAN-r2.md

# Independent re-review (r2): MATH-CON-1 Stage 1B first-stage round plan and draft control plane

**Objects:** `PLAN.md` (r2, 375 lines) and `preregistration.draft.md` (r2, 788 lines) in this directory. I compared
them with `PLAN-r1.md` and `preregistration-r1.draft.md`.

**Reviewer:** the same independent agent that wrote `REVIEW-PLAN.md`. I did not write either object, and I wrote
nothing outside the scratchpad.

## Verdict: **ACCEPT WITH CHANGES**

There is **one blocking finding, R2-B1**. It is a hole in how the auxiliary-declaration policy is enforced, and it
lives in text that freezes at `F`. The fix is one rule sentence plus five self-test cases. Once that edit is made and a
reviewer has checked it, the preregistration can be held as a candidate `F`. The rest of r2 does not need another full
re-review. The non-blocking findings R2-N1 to R2-N7 should be applied before `F` where they touch frozen text.

## Checks run

| check | result |
| --- | --- |
| V3 blocks, r1 against r2 | byte-identical; my verifier probe on the r2 text gives `VERDICT HOLDS` on both the clean complete path and the halted path, with digest `81897a90a068b0402e68393f82cffda8fd83f0bda5283316c38d8c58b28e5107` |
| full ids added under N9 | `13340732fe7e95466dd64faf3b8307fb386ad091` exists and is on `main` |
| short-name collisions | none of the new definitions or inductives is already declared at column 0 under `verification/lean-mathlib` on `main` |
| frozen `ancSign` / `ancillaHH` / `toffoliToken`, transcribed literally | they reproduce the O-3a word with the control on value `3`, and the word fails with `2`, so the B3 mutation does bite |
| count of theorems and `#print axioms` lines | 26 and 26 (3 + 6 + 4 + 2 + 8 + 1 + 2), in the same order |

The transcription check was a review check of definitional fidelity. It is review provenance only and carries no
weight in the round (see the N6 discussion).

## Dispositions of r1's findings

| finding | resolved? | notes |
| --- | --- | --- |
| **B1** S4 against V | **Yes** | Frozen text 3 (the owner's boundaries, verbatim from 6721662886; I checked it against the comment) is excluded from S4 and checked by V. The self-test generates complete notes for five outcomes. See R2-N3 for one remaining source of hits: the free-text halt reasons. |
| **B2** per-cell tokens | **Yes**, option (a) | See the B2 assessment below. |
| **B3** frozen surface | **Yes** | `MonoExt` and `FiatC` are in full Lean text in `PolC`'s binder form. `FiatC` matches CC-1's `𝓕`: `base` covers `one` and `perm`, and there is nothing beyond `swap`. `ancSign`, `ancillaHH` and `toffoliToken` are frozen with the control on value 3, and mutation cases were added. |
| **B4** earned reading | **Yes** | I checked every clause of frozen text 1 against a frozen theorem. Each holds; I found no overstatement. |
| **B5** auxiliary and option policy | **Yes in substance; enforcement hole** | See R2-B1. |
| **N1** O-1 at a general carrier | Yes | The scope table names the system and level forms as the obligation. |
| **N2** CC-1(a) has no frozen theorem | Yes | `fiatC_conjugatedAttempt_available` is O-2's transfer clause applied to O-3e, so it is not scope creep. |
| **N3** KC scope; `class_hypothesis_needed` | Yes | That theorem is removed. The CAL/CC-0 distinction is in the scope table and in frozen text 2, and the scope confirmation is in the `F` request (precondition 6). |
| **N4** template remnant; definition mutations | Yes | |
| **N5** XS coverage | Yes | `stopped` and the discard and partial-trace definitions are included, with a correspondence table. |
| **N6** exact layer's evidence form | **Adopted in part; I accept the part not adopted** | See the N6 assessment below. |
| **N7** negative route; unproved halt; §A.26 | Yes | KTRANS-SEP-2's wording; "not proved in this round; open"; a three-step recorded halt decision; a separate *Pauses* paragraph. |
| **N8** §A.41 gaps; designation order | Yes, with a gap | AST allowlists, and host timestamps in `evidence/order.json`. See R2-N1 and R2-N2. |
| **N9** merge method; full ids | Yes | Step 0 includes an ancestry check. |
| **N10** "four steps stay last" | Yes | Dropped. |
| **N11** approval list | Yes | Now complete: step 0 (merge commit, directory ruling, writer); dispatch at `F`; designation of `F` with the scope confirmation; dispatch at S1 (optional); dispatch at `E`; designation of `E`; each re-dispatch; the conditional halt decision; the landing. The step-0 text in PLAN §6 is accurate and complete. |
| **N12**, **N13**, **N14** | Yes | |

## The B2 choice (option (a), KTRANS-SEP-2's form)

Option (a) is the right choice.
- **The evidence carries one fact.** The structured evidence says one thing about the kernel: whether all 26 reports
  are standard.
- **Attribution would mislead.** `#print axioms` reports transitively, so naming a cell would mislead: O-3d and O-3e
  consume O-3a–c, and §F2 consumes O-2 and O-3e.
- **Option (b) changes nothing.** Every negative reading halts the stage, so per-cell markers would decide nothing
  differently.
- **The rule is disclosed.** The rule is stated in the decision table, and frozen text 2 discloses it ("one reading of
  one kernel gate").
- **The negative route is pinned down.** It arises only from complete reports with a non-standard axiom, in practice
  error-recovery `sorryAx`; a literal `sorry` fails N3 and gives VOID. That matches the precedent.

## The B5 policy

The substance is sound:
- only `private theorem aux_…` may be added;
- no `def`, instance, attribute or notation may be added, so no auxiliary declaration can change what a frozen
  statement means;
- the axiom coverage is transitive;
- the bounded options (`maxHeartbeats ≤ 4000000` and `maxRecDepth ≤ 8192`, `in`-scoped) are proportionate, given that
  BFP needed 2000000.

The policy removes the engineering-only halts that B5 was about. The enforcement has one gap, R2-B1.

## The N6 partial adoption

**I accept the writer's position: the checker does not run on the round's objects before `F`.**
- **The writer's ground is correct.** DESIGN §3.2 lists "the checks that `H·drivePhase·H` meets D2 and D3, by exact
  algebra" as part of O-3e itself. The owner's "Freeze `F` before execution" therefore puts those computations after
  `F`.
- **§A.29 points the same way.** Preregister the rule, not the numbers.
- **My own checks have no standing in the round.** My r1 reproduction 2, and today's transcription check, were review
  checks outside the round. They are review provenance only. The preregistration rightly does not cite them, and they
  must never appear as support in the result note.
- **The rest of N6 is adopted.** That part covered the distinct exit statuses, completeness read from exit status plus
  the summary line plus the check count, and a crash reading VOID.

**What the refusal costs.** The checker's blob freezes at `F` but meets real objects only at S1. A reconstruction bug
found there cannot be repaired, and the round halts for a non-mathematical reason. This is the KTRANS-SEP-1 failure
mode. R2-N4 gives a mitigation that stays inside the owner's boundary.

## Blocking finding

**R2-B1. The elision rule and N1 can hide a forbidden declaration inside an elided proof span.**
- Step 3 of the elision rule ends a declaration only at a column-0 line that starts with one of the listed keywords:
  `theorem`, `private`, `def`, `noncomputable`, `inductive`, `/--`, `--`, `set_option`, `#print`, `end`,
  `namespace`, `open`, `section`, `import`.
- These column-0 commands are missing from that list: `instance`, `attribute`, `@[…]`, `lemma`, `abbrev`, `example`,
  `structure`, `class`, `notation` and its `infix` family, `macro`, `syntax`, `local` and `scoped`, `variable`,
  `universe`, `mutual`.
- Any of them placed directly after a frozen theorem's proof becomes part of that elided proof, so N2 passes.
- N1's frozen definition ("the frozen declarations, in order and by kind, plus only `aux_` theorems") does not say that
  it inspects elided spans.
- N3's text grep covers only `axiom`, `opaque`, `sorry` and the like.

**Why this matters.** A column-0 `instance`, `notation` or `attribute [local simp]` can change how a *later* frozen
statement elaborates while its text stays byte-identical. That defeats the round's central invariant, "statements and
definitions are not changed in execution".

**Fix, frozen before `F`:**
- Any non-blank line at column 0 ends a declaration. Lean proofs are indented, so this costs nothing and becomes a
  stated formatting constraint.
- N1 classifies every column-0 line against an explicit allowlist and fails on anything else. The allowlist is the
  frozen commands, `private theorem aux_`, `/--`, `--`, `set_option … in`, `#print axioms` and `end`.
- Add self-test cases, each placed directly after a frozen theorem's proof:
  - a column-0 `instance`;
  - a column-0 `attribute [simp]`;
  - `@[simp] private theorem aux_x`;
  - a column-0 `notation`;
  - a column-0 `lemma`.

  Each must fail N1. A proof containing a column-0 comment must fail N2, as the documented formatting constraint
  requires.

## Non-blocking findings

**R2-N1. The designation-order checkpoint misses where proof work starts (§A.41).**
- `evidence/order.json` checks that the `F` designation precedes the first host run at S1.
- PLAN §1.2 and step 9 have the proofs developed on a disposable dev branch with its own draft PR. That is where
  execution actually begins, and nothing measures it.
- *Fix:* extend `order.json` to the dev branch's first host run, created from `F` after designation, or require the
  dev branch's first commit to be a child of `F` and record its first run's `created_at`.
- Also state where the order evidence goes on a halt before S2. `order.json` is added only at S2, so it should also be
  carried at `W`.

**R2-N2. P's clause on evidence files is ambiguous.**
- P says pinned evidence files carry "no timestamp or duration field", while `order.json` exists to carry `created_at`
  values.
- If that clause reaches `evidence/**`, every complete `check E` is VOID.
- *Fix:* restrict the clause explicitly to the files pinned at `F`, or give `order.json` its own frozen schema: the
  two `created_at` values, the answer digests and the computed ordering.
- Add one positive self-test of a full synthetic `check E` that includes `order.json`. Also name the comments-API
  answer as a captured input beside `RUN` and `JOBS`.

**R2-N3. Free-text halt reasons can trip S4 or V.**
- "Control <code> failed: <reason>" puts unscreened text into the note. An S4 failure's own reason may quote the phrase
  it found.
- *Fix:* make each control's reason a frozen string per code, screened in the self-test.
- Likewise, write the note and `derive-run`'s output to stdout, or list those write sites. Otherwise B's "two frozen
  write sites" rule contradicts the note generation.

**R2-N4. Mitigate the N6 residual risk without crossing the owner's boundary.**
- Before `F`, run every checker code path on objects already proved on `main`. They are not O-3a–e content:
  - X3 and X4's reset, readout, correction, discard and `stopped` machinery on B23's **unconjugated** attempt, against
    `attempt_balanced_branch` (BFP:194) and `balanced_stopped_formula` (BFP:245);
  - X1's 8×8 word code path on an identity that is not O-3a's, for example `ancillaHH·ancillaHH = 1` or
    `toffoliToken² = 1`.
- Record these as fixtures. The checker then first meets *new* content at S1, but no untested code path.

**R2-N5. A countercontrol that does not fail as stated reads as an exact NOT-ESTABLISHED.**
- Exit status 3 lumps checks and countercontrols together, as KTRANS-SEP-2 did. Under §A.29, a countercontrol that
  does not fail as stated is a failed control, so the reading should be VOID or control-failure, not a negative
  scientific reading.
- Both outcomes halt, and the halt sentence names the check ids, so only the label is affected.
- *Fix (optional):* use a distinct exit status, such as 4, for a countercontrol that does not fail as stated, mapped to
  the control-failure route.

**R2-N6. The elaboration-corrections clause.** The clause ("an implicit argument, a coercion, a `noncomputable`
marker or a qualified name may change") is sound. Record each correction with a before/after diff on the PR, so that
a reviewer can confirm no hypothesis or conclusion changed. The draft says the corrections are recorded; say how.

**R2-N7. Cost and approvals.** The cost statement is unchanged and acceptable under §A.40. The re-dispatch approval
(step R) and the conditional halt approval (step H) are correctly separate. No further change is needed.

## Summary for the coordinator

- **Verdict:** ACCEPT WITH CHANGES.
- **Blocking:** one finding, R2-B1, the enforcement of the column-0 declaration allowlist.
- **N6:** the writer's partial adoption is correct and accepted. Exact algebra on the round's objects is part of O-3e
  and belongs after `F`. Apply R2-N4 to exercise the checker's code paths on objects already proved on `main` before
  the checker's blob freezes.
- **V3 blocks:** unchanged; the digest and the `HOLDS` result were reproduced.

Generated by Claude Code

amaybaum · 2026-11-08T13:30:27Z

MATH-CON-1-S1B-1, step 0: decisions recorded (owner decision, chat, 2026-11-08)

The owner (amaybaum) decided this in chat with the coordinating session on 2026-11-08: "I approve the recommended path for all four decisions, with the existing scientific and execution safeguards preserved."

Decision	Authorization
Merge #1206	Approved. Preserve `41a42cb` through a normal merge commit, unchanged.
Sibling directory	Approved. Use `round-mathcon1-s1b-1/` and record the explicit deviation from §10.1.
Designated writer	Approved. The proposing Claude Code session is designated writer, limited to O-1, O-2 and O-3a–e.

The existing r2 / WIP header may remain unchanged. Record the accepted status and exact commit in the round's preregistration.

The Stage 1B round may proceed to PR preparation only after the revised round draft receives an independent ACCEPT and the design is integrated into main.

N6.

I do not approve running the actual exact-arithmetic checker on the real objects before F. … If the checker fails at E, halt, preserve the evidence, and request a separate decision. Do not silently repair or rerun the frozen round.

Execution boundaries.

The estimated 18–20 CPU-hours are acceptable as a planning budget, not as blanket execution authorization.

Each of the following still needs its own approval:

the exact F designation and its controls;
each CI dispatch at F, E, and optionally S1;
the E designation and any re-dispatch;
the final landing merge.

Most importantly, Stage 1B must not be described as deriving quantum mechanics from OI. The Hadamard operation is supplied by the proposed rule. A successful first stage establishes, at most, mathematical support for a candidate circular construction (C). It does not establish a final outcome or resolve the remaining instrument, composition, and noncircularity obligations.

No research execution, freeze, CI dispatch, or additional merge is approved beyond the explicit decisions above.

Planning-status entry (§A.45 rule 3)

Field	Value
Item	MATH-CON-1-S1B-1 (MATH-CON-1 Stage 1B, first stage)
Scope	O-1, O-2 and O-3a–e only, under #1169 c.6721662886
Writer	The coordinating Claude Code session (session_013T6pfKuv5mi3MXtKjH2tZb)
Authorization	`execution`, limited to O-1, O-2 and O-3a–e; each `F`/`E` designation, dispatch, re-dispatch and the landing need separate approval
Record directory	`verification/programmes/oi-qm/reconstruction/round-mathcon1-s1b-1/` (a sibling directory; deviates from DESIGN §10.1, as approved)
Readiness	`blocked`, until (1) #1206 lands on `main` and (2) the revised round draft (r3) receives an independent ACCEPT
Conflicting writers	None. No other active item writes the round branch, its record directory or its execution paths

Generated by Claude Code

amaybaum · 2026-11-08T13:36:36Z

Independent review of the MATH-CON-1 Stage 1B round draft r3 (scratchpad; model reviewer, not human): REVISE (R3-B1, R3-B2)

REVIEW-PLAN-r3.md

# Independent re-review (r3): MATH-CON-1 Stage 1B first-stage round, focused check

**Objects:** `preregistration.draft.md` and `PLAN.md`, both r3, read against their r2 copies saved beside them.
**Reviewer:** the same independent agent as for r1 and r2; I am not the writer. I made no writes outside the
scratchpad.

## Verdict: **REVISE. Not accepted.**

Two items must be fixed. Both sit in the frozen policy text, and each needs a few lines plus self-test cases:
- **R3-B1**, the command scan, is a gap that matters.
- **R3-B2** is a contradiction inside the policy.

The other parts of r3 are correct. If only these two items change, a narrow check of them is enough before an ACCEPT;
r3 does not need another full review.

## 1. R2-B1 and the writer's extension

**The writer's objection is right, and my R2-B1 fix was incomplete on its own.** Lean 4 commands are not tied to
column 0. After a term-mode proof, the term ends and the next keyword begins a new top-level command, at any
indentation. After a tactic block, a token that cannot start a tactic ends the block in the same way. Scanning the
elided proof spans for commands is the right mechanism.

### R3-B1 (blocking): the frozen keyword list is incomplete, and the gaps include commands that change meaning

The list is hand-written. These command keywords, among others, are not on it, so a command led by one of them passes
the scan from inside an elided proof:

- **bare `open Foo`, without `in`.** `open` appears only in the `open … in` exemption. A bare indented `open` after a
  term-mode proof is a file-level command. It changes how names resolve, and which scoped instances and notation
  apply, in every later frozen statement, while their text stays byte-identical. This is exactly the hazard R2-B1 was
  about.
- **`alias`** (Batteries). It declares a new constant. Inside `OIBridge.PolarizedProtocol`, an alias named like a
  consumed kernel name, `conjChannel` for example, would take precedence in later statements over the outer
  declaration.
- **`notation3`** (Mathlib). The whole-word rule does not match `notation` inside `notation3`. The same holds for
  `elab_rules` against `elab`.
- **`run_cmd`, `run_elab`, `run_meta`.** These can change the environment arbitrarily: add instances, attributes or
  declarations.
- **`unif_hint`, `irreducible_def`, `binder_predicate`, `declare_syntax_cat`, `simproc`, `dsimproc`, `add_decl_doc`,
  `include`, `omit`, `assert_not_exists`, `suppress_compilation`,** and the rest of the command table.

A denylist written by hand cannot be shown complete. The command category is extensible, and Mathlib adds commands.

**Fix, frozen before `F`:**
1. **Derive the list from the environment.** Take the scan list from the leading-token table of the `command` syntax
   category in the pinned toolchain-plus-Mathlib environment of the module's imports. Dump it with a small Lean
   `#eval` in the statement-elaboration design run, as design evidence, not in the frozen workflow. Pin it at `F` as
   a structured file with its sha256, and have N1 read it. That list is complete with respect to the environment the
   module actually elaborates in. Every top-level command begins with a token from that table, including declaration
   modifiers such as `@[` and `private`, and docstring-led declarations. The module itself cannot add command syntax,
   because `syntax`, `macro` and `notation` are in the table and therefore banned.
2. **Make the exemptions exact grammar, not keyword omission.**
   - `open` is a hit unless the tokens after it are identifiers (optionally after `scoped`) and are followed by `in`.
   - `set_option` is a hit unless it reads `set_option (maxHeartbeats|maxRecDepth) <n> in`, with `<n>` within the
     bounds.
   - Exempt `open scoped … in` explicitly. Otherwise a proof that needs a scoped instance, such as `ComplexOrder` near
     PII's cone, must fall back on `open ComplexOrder in`. That works, but it should be a stated choice, not a trap.
3. **Self-test cases:**
   - an indented bare `open Foo` after a term-mode proof;
   - `alias`;
   - `notation3`;
   - `run_cmd`;
   - `elab_rules`;
   - a nested block comment `/- /- instance -/ -/`, which must pass;
   - a `«instance»`-escaped identifier, which must pass.
4. **State the lexing.** A hit is a Lean token equal to a listed keyword. Identifiers, dotted names included, are
   single tokens, and the match is case-sensitive. Under that rule `infer_instance`, `classical`,
   `ImplementationClass` and `readout_is_localLuders` never match. Under a plain `\b` regex they still would not, but
   the frozen text should not leave the rule implicit.

If the owner prefers not to add a Lean dump, the minimum acceptable fix is the hand list extended by every item above,
with bare `open` treated as a hit. The preregistration must then say that the list's completeness is unverified for
commands added later.

**Can a legitimate proof be rejected in a way that halts the round? No, in practice.**
- Proof bodies and term-mode proofs do not need command keywords. With token-level matching, tactic names such as
  `infer_instance` and `classical` do not collide with them.
- N1 runs locally in `check S1` before any dispatch, and a repair may rewrite proofs and `aux_` theorems. A false hit
  therefore costs a proof rewrite, not a halt.
- The only residual risk is a proof that needs a flagged construct with no workaround. With the `open [scoped] … in`
  and `set_option … in` exemptions, I know of none for these statements.

### R3-B2 (blocking): the option and `open` policy contradicts its own self-test

- The option allowlist says each allowed `set_option` is "`in`-scoped, directly before a frozen theorem or an `aux_`
  theorem. Any other `set_option`, a global one, or one before a `def` or `inductive` fails N3."
- The new self-test case says "`set_option maxHeartbeats 400000 in` inside a proof pass[es]".
- Likewise, the auxiliary policy refuses "any … `open` … command beyond the frozen ones", while the scan exempts
  `open … in` inside proofs.

The self-test would expose the conflict before `F`, so nothing silent is at stake, but the frozen rule has to say one
thing.

**Fix:** state that the in-proof forms `open [scoped] <ids> in` and `set_option (maxHeartbeats|maxRecDepth) <n> in`,
with the same bounds, are permitted in proof spans. State that N3's placement rule governs the command-level forms
only. Make N3's implementation and the self-test agree with that text.

## 2. R2-N1 to R2-N6

| finding | applied? | note |
| --- | --- | --- |
| R2-N1 order evidence | **Yes** | `order.json` covers the dev branch's first host run and the round branch's first execution run. It is carried at `W` on an early halt, and the measurement limit is stated. **Non-blocking (R3-N1):** the holds-rule makes "`dev_branch.first_commit_parent` is `F`" a conjunct, yet the dev branch is disposable and off `main`, and the text calls it provenance. Under §A.42 item 8, a conjunct of the rule is support, not provenance. Either drop it from the rule and keep it as a recorded provenance field (the host timestamps already carry the ordering), or record that it rests on an off-`main` object. Also page the runs answers past `per_page=100`, or capture the oldest run by `created_at` ascending. |
| R2-N2 timestamp clause | **Yes** | The clause is scoped to the files pinned at `F` and to `f-run/results.json`. `order.json` has its own schema, and there is a positive full synthetic `check E` with `order.json`. |
| R2-N3 free text in the note; write sites | **Yes** | One frozen reason per code, and none of the reasons contains a screened phrase. The note interpolates only ids, codes and frozen names. Outputs go to stdout, and P and V regenerate and compare. |
| R2-N4 checker code paths before `F` | **Yes** | Four fixtures: BFP:194, BFP:245, `ancillaHH·ancillaHH = 1` and synthetic X2 matrices. None computes O-3a–e content. They are a precondition of `F`. |
| R2-N5 countercontrol outcome | **Yes** | Exit 4 is a failed control X, deterministic, with no re-dispatch. The summary separates checks from countercontrols, and the twelve printed lines (8 + 4) agree with it. |
| R2-N6 elaboration corrections | **Yes** | Each correction is its own control-plane commit with a before/after diff and reviewer confirmation before `F`. This is permitted before `F` (`G9`). |

## 3. V3 blocks

They are byte-identical to r1 and r2. My verifier probe on the r3 text again gives `VERDICT  HOLDS`, with
governed-paths digest `81897a90a068b0402e68393f82cffda8fd83f0bda5283316c38d8c58b28e5107`.

## 4. New defects

- R3-B2 above. It is new in r3.
- **R3-N2 (non-blocking): comment and string stripping.** The stripping must handle Lean's nested block comments
  (`/- … /- … -/ … -/`), docstrings `/-- … -/`, char literals such as `'"'`, and raw strings. Add a self-test case for
  nesting; R3-B1 item 3 includes one.

Nothing else changed outside the R2 dispositions. I checked the following and found each consistent:
- the frozen statements and frozen texts 1–3 (unchanged from r2);
- the decision table;
- the stop rule's new exit-4 bullet;
- the precondition renumbering, 6 to 7;
- PLAN steps 4, 5, 9 and 11;
- the owner-approval list.

## What would turn this into ACCEPT

1. **R3-B1.** A complete command list: preferably the dumped command-category token table, pinned at `F`; at minimum,
   the extended hand list with bare `open` as a hit. Add exact exemption grammar, a stated lexing rule, and the new
   self-test cases.
2. **R3-B2.** One consistent rule for in-proof `open … in` and `set_option … in` across the policy, N3 and the
   self-test.

R3-N1 and R3-N2 are recommended but are not conditions.

Generated by Claude Code

amaybaum · 2026-11-08T13:44:23Z

Independent review of the MATH-CON-1-S1B-1 round draft r4 (scratchpad; prereg sha256 dd7bab93fd2438413c46cd1cc3cfe04b457fddcb78497d2c94b8cffd336a4acc, PLAN sha256 0d0259dee41a0d9a62992d4686b59c23815ac5f0760d7c5ca956564265c5de30). Verdict: ACCEPT WITH CHANGES (one blocking finding, R4-B1). Model review, not human verification.

REVIEW-PLAN-r4.md

# Independent re-review (r4): MATH-CON-1-S1B-1 round draft, focused check

## Objects reviewed

| file | sha256 |
| --- | --- |
| `preregistration.draft.md` (r4) | `dd7bab93fd2438413c46cd1cc3cfe04b457fddcb78497d2c94b8cffd336a4acc` |
| `PLAN.md` (r4) | `0d0259dee41a0d9a62992d4686b59c23815ac5f0760d7c5ca956564265c5de30` |

Each was compared line by line with its r3 copy (`preregistration-r3.draft.md`, `PLAN-r3.md`).

I am the same independent reviewer as for r1–r3, not the writer. I made no Lean build, no push and no GitHub write.

## Verdict: **ACCEPT WITH CHANGES**

There is one blocking finding, **R4-B1**. It must be in the text before a candidate `F` is held.
- It is a cheap, decidable non-vacuity precondition on the command-table dump.
- A check of that one edit is enough; no further full review is needed.

Everything else in r4 closes its finding without opening a new hole. The non-blocking findings R4-N1 to R4-N4 should
be applied in the same edit if convenient.

## Checks run

| check | result |
| --- | --- |
| V3 blocks against r3 | byte-identical (the diff touches no line of either block) |
| verifier probe on the r4 text (real `v3_verifier.py` and `v3_receipt.py`) | clean path `VERDICT  HOLDS`, governed-paths digest `81897a90a068b0402e68393f82cffda8fd83f0bda5283316c38d8c58b28e5107`; a `DESIGN.md` edit `FAILS s3:unauthorized, s9:landing-unauthorized` |
| push triggers for the design branch's modified workflow | `verify.yml` triggers on `push` only for `main`, so the design-only step runs only through the design PR's ordinary `pull_request` run |

## The planner's claims, verified

### Claim 2: R3-B2 is closed

*Permitted scoped forms* is now one rule, and it is consistent across the policy, N1, N3 and the self-test:
- **Command level.** Only a bounded `set_option … in` is allowed, on its own line directly before a theorem line. N3
  governs command-level forms only.
- **In proofs.** Exactly two forms are allowed, by the scan's exemption grammar: `open [scoped] <ident>+ in`, and the
  same bounded `set_option … in`. Bare `open`, `open … hiding`, `open Foo (x)` and any other option are hits.
- **Self-test.** It has both the command-level and the in-proof cases, including `open scoped ComplexOrder in`, which
  passes.

The line "refused at command level" in the auxiliary policy removes the earlier conflict.

### Claim 3: R3-N1 is closed

- The parent of the dev branch's first commit is now a `provenance` field that no rule reads, and it is classified
  under §A.42 item 8.
- The ordering rests on host timestamps alone.
- Runs answers are captured `--paginate` and checked against `total_count`; an incomplete capture fails P.
- The first run is the earliest `created_at` across all pages.

### Claim 4: R3-N2 is closed

The lexing rule covers:
- nested block comments;
- `/--` and `/-!` openers as hits;
- escaped, interpolated and raw strings;
- char literals;
- `'` inside identifiers;
- `«…»` escaped identifiers and dotted names as single tokens;
- `#`-tokens.

Self-test cases cover each of these. See R4-N2 for one detail of the lexer that needs to be stated precisely.

### Claim 5: the V3 blocks are unchanged

Confirmed above.

### Claim 1: R3-B1, the route through the command-table dump

**The mechanism is right.** The leading-token table of the `command` category, in the module's own import environment
under the pinned toolchain, is the correct source of completeness. The floor (ii) now contains every item R3-B1 named,
with bare `open` and `set_option` as hits outside the exact exemption grammar. The caveat for parsers not indexed by a
first token is honest, and its frozen sentence passes S4 (the writer's probe, plus my reading).

**§A.39 and §A.43: no violation.**
- **No authorization needed.** The dump step runs only on the disposable design branch under ordinary `pull_request`
  CI, which §A.43 item 4 allows by default. It is not a `workflow_dispatch` and not a governed launch, and the push
  does not trigger `verify.yml`.
- **Not part of the round's workflow.** It is not part of the frozen workflow edit, and W refuses it at S1 and `E`.
- **Structured retrieval.** The file is retrieved as an artifact through the artifacts API, as a structured file
  (§A.44), not from a log.
- **Durable copy and recipe on `main`.** The artifact and the run id are provenance only. The file's content lands on
  `main` at S1 as `evidence/command-tokens.json`, with its sha256 pinned at `F`. The dump script is embedded verbatim
  in `controls.py` and in the preregistration, so the recipe is on `main` (§A.42 items 1–2 and 8).
- **Deterministic and matched to execution.** The output is deterministic for the pinned environment. The environment
  at `E` is `D`'s toolchain and imports, so the dump describes the environment the module actually elaborates in.

**Is the route decidable before `F`? Yes, provided R4-N1 is applied.** The contingency is decided before `F`, and the
text says "one of the two routes is in force at `F`, never both as alternatives". Several sites still assume the dump
route unconditionally, however:
- precondition 3's pin list;
- P's list of files pinned at `F`;
- the dump-consistency self-test cases;
- the §A.41 row.

If the frozen text at `F` kept both routes, the executor would choose after `F`. R4-N1 removes that possibility.

**Could an unconfirmed API name make a control vacuous rather than failing? A wrong name could not; wrong semantics
could.** That is R4-B1.
- **A wrong API name fails loudly.** If `parserExtension`, `leadingTable` or `leadingParsers` is misnamed or
  mistyped, elaboration fails. No dump is produced, and the contingency applies.
- **A wrong encoding passes silently.** This is the dangerous case: names that elaborate but return token strings the
  lexer never produces.
  - `leadingTable` is a `TokenMap`, keyed by `Name`. With its default escaping, `Name.toString` renders a non-identifier
    token such as `@[` or `#eval` as `«@[»` or `«#eval»`.
  - A dump in that form is non-empty and well-formed. Its symbolic entries match no lexed token, so the scan silently
    falls back to the floor, while the note implies completeness.
  - The same silent failure follows from a table that is empty or partial at `#eval` time, or from keys that encode
    something other than the literal token text.
- **The current guard is circular.** It reads "`leading_tokens` must contain every floor entry that the environment
  defines". But whether the environment defines an entry is judged from the dump itself. And the self-test case "a
  token drawn from the embedded dump list fails N1" shows only that the lexer matches the dump's strings, not that
  those strings are real Lean tokens.

## Blocking finding

**R4-B1. Add a decidable non-vacuity precondition for route (i).**

Freeze a reference set of command tokens that the dumped environment certainly defines:
- Lean core: `theorem`, `def`, `instance`, `@[`, `#eval`, `open`, `set_option`, `namespace`, `end`, `variable`,
  `section`, `private`, `/--`;
- Batteries: `alias`;
- Mathlib: `lemma`, `notation3`, `irreducible_def`.

Route (i) is admissible only when every reference token appears **verbatim** in `leading_tokens`: unescaped, as the
literal token text. If any is absent, the dump is defective, and the floor-only route applies under the stated
contingency. A floor entry missing from the dump is not to be explained away "with a reason".

Make three supporting changes:
- **Script.** Emit raw token text from the dump script, either by pattern-matching `.str .anonymous s` or with
  `Name.toString (escape := false)`. Write the JSON with `IO.FS.writeFile`, not mixed into stdout with Lean's own
  messages.
- **Control P.** Have P check the reference-set condition against the pinned file.
- **Self-test.** Add three cases: a dump with escaped tokens (`«#eval»`) fails; a dump with an empty `leading_tokens`
  fails; and a dump missing one reference token fails.

## Non-blocking findings

**R4-N1. Freeze exactly one route.** In the last pre-`F` commit, replace the contingency paragraph with a single route
line, for example `command-scan route: dump` or `command-scan route: floor-only (completeness unverified)`, and let
`controls.py` read it. Make every route-dependent site agree with that line:
- precondition 3;
- P's list of files pinned at `F`;
- the dump-consistency self-test cases;
- the caveat sentence;
- the §A.41 row.

No conditional wording may remain at `F`.

**R4-N2. Define the lexer's identifier characters and the char-literal fallback.**
- Identifier characters must follow Lean's own classes: letter-like, including Greek and script letters such as `𝓘`,
  plus subscripts, `_`, `!`, `?` and `'` as Lean permits. Otherwise the `'` in `h𝓘'` would open a char literal.
- A `'` that does not begin a complete char literal, by the exact grammar, is an ordinary token and skips nothing.
- Add the self-test case `h𝓘' instance` placed after a proof; it must fail N1.

**R4-N3. Include the module's frozen `open` line in the dump.** Activating a namespace can bring in scoped syntax, so
the dump script's environment should also carry the module's frozen `open` line once the design run fixes it. Scoped
command parsers are rare, so this is low risk.

**R4-N4. Keep the dump step out of the derived design-run evidence.** Place the design-only step so that the four
round steps L0, L, A and M remain the bridge job's last four steps on the design branch; the writer's "after `Build`"
does that. `derive-run` should be run on the design run's answers unchanged.

## Summary

- **Verdict:** ACCEPT WITH CHANGES.
- **Blocking:** one, R4-B1, a frozen reference-token non-vacuity condition on the dump.
- **Claims verified:** R3-B2, R3-N1, R3-N2 and the unchanged V3 blocks are confirmed.
- **The dump route:**
  - It is sound and complies with §A.39, §A.42, §A.43 and §A.44.
  - It is decidable before `F` once R4-N1 is applied.
  - An unconfirmed API name fails loudly. An unchecked token encoding would fail silently, and R4-B1 closes that path.

Generated by Claude Code

amaybaum · 2026-11-08T14:07:49Z

Independent review of the MATH-CON-1-S1B-1 round draft r5 (scratchpad; prereg sha256 36cc740af35a654bb96e11a9ef73b3e71ca59042fb00f020b35bd512fd23c3eb, PLAN sha256 bcd2d160549b5473d3fe14bffa4c830fa961519b4ec3edd5f73d71415f0be29d). Verdict: ACCEPT WITH CHANGES (no blocking findings; R5-N1–N3 to be applied by candidate F). Model review, not human verification.

REVIEW-PLAN-r5.md

# Independent re-review (r5): MATH-CON-1-S1B-1 round draft, focused confirmation

## Objects reviewed

| file | sha256 |
| --- | --- |
| `preregistration.draft.md` (r5) | `36cc740af35a654bb96e11a9ef73b3e71ca59042fb00f020b35bd512fd23c3eb` |
| `PLAN.md` (r5) | `bcd2d160549b5473d3fe14bffa4c830fa961519b4ec3edd5f73d71415f0be29d` |

Both hashes match the coordinator's. I compared each file line by line with its r4 copy (`preregistration-r4.draft.md`
and `PLAN-r4.md`).

I am the same independent reviewer as for r1–r4, not the writer. I made no Lean build, no push and no GitHub write.
For the reachability and identifier-class checks I read public source at the pinned tags: Lean `v4.33.0` and Mathlib
`v4.33.0`.

## Verdict: **ACCEPT WITH CHANGES. No blocking finding.**

- R4-B1 is closed, and so are R4-N1 to R4-N4.
- Preparation of the round PR may proceed.
- Three corrections, R5-N1 to R5-N3, must be in the text by candidate `F`. All three are pre-`F` drafting edits, and
  PLAN step 6's scheduled pre-`F` re-review checks them.
- R5-N1 is a factual correction to frozen text. It errs only on the safe side, so it cannot admit a hidden command.

## Checks run

| check | result |
| --- | --- |
| V3 blocks against r4 | byte-identical (the diff touches neither block) |
| verifier probe on the r5 text (real `v3_verifier.py` and `v3_receipt.py`) | `VERDICT  HOLDS`, governed-paths digest `81897a90a068b0402e68393f82cffda8fd83f0bda5283316c38d8c58b28e5107` |
| route line | exactly one standalone column-0 line, `command-scan route: PENDING` (line 332). The other mentions of the two route values sit inside prose or list items, never as a standalone column-0 line. |
| drafting note | exactly one line begins `*Drafting note` |
| import closure of the module's three imports | 93 `OIBridge` modules, read from `main`. Its Mathlib imports include `Data.Complex.BigOperators`, `Analysis.SpecialFunctions.Trigonometric.Basic`, `Analysis.SpecialFunctions.Complex.Log`, `Topology.Algebra.UniformRing`, `Analysis.CStarAlgebra.*` and `Analysis.Matrix.*`. |

## R4-B1 and the reference set (planner's claim 1)

R4-B1 is closed.
- **The reference set is frozen.** It holds 17 tokens: 13 from Lean core, `alias` from Batteries, and `lemma`,
  `notation3` and `irreducible_def` from Mathlib.
- **The admission rule is decidable.** The `dump` route is admissible only when every reference token appears
  verbatim and unescaped. Otherwise the route is `floor-only`.
- **No escape hatch.** Absence is not explained away, and the reference set may not be edited after the dump is seen.
- **The script fixes the encoding.**
  - It now uses `Name.toString (escape := false)`, so a symbolic token is no longer wrapped as `«@[»`.
  - It writes the file with `IO.FS.writeFile`, so Lean's own messages never reach the JSON.
- **P checks the condition at S1 and `E`.**
- **Self-test cases** cover an escaped dump, an empty dump and a dump missing `notation3`.

**Vacuity.**
- A wrong API name fails to elaborate, so no dump is produced and the route is `floor-only`.
- A wrong encoding, or an empty or partial table, fails the reference set, with the same result.
- The control can no longer go silently vacuous: every failure mode leads to the stated `floor-only` route, whose
  completeness is declared unverified.

**The planner's flagged risk, reachability of `notation3` and `irreducible_def`: both are reachable, with high
confidence.** I checked use sites at Mathlib `v4.33.0` by reading the source, not by a build:
- `Mathlib/Data/Real/Basic.lean` declares `private irreducible_def zero`, `one`, `add`, `neg`, `mul` and others.
  `Data.Complex.BigOperators` and `Analysis.SpecialFunctions.*`, which are in the closure, sit downstream of
  `Data.Real.Basic` through ℂ and ℝ.
- `Mathlib/Order/SetNotation.lean` declares the `⨆`, `⨅`, `⋃` and `⋂` notations with `notation3`. Every
  order-theoretic and topological import in the closure sits downstream of it.

Each command's syntax is defined upstream of its first use. If my reading were wrong, the reference-set condition
would decide mechanically before `F`, and the round would fall to `floor-only`, never to a vacuous control. This risk
therefore cannot harm validity; at worst it costs completeness, and that cost is declared.

## R4-N1, the single route (planner's claim 2)

R4-N1 is closed, and I found no discretion left after `F`.
- `controls.py` reads the route line from `F`'s blob.
- P fails if the line is missing or duplicated, if it reads `PENDING` or anything else, or if a route-dependent site
  disagrees with it.
- The last pre-`F` commit sets the route and deletes the drafting note, and P fails if any `*Drafting note` line
  remains at `F`.
- So `F` carries exactly one route, and the pinned `controls.py` enforces it.

**Deleting the drafting note is not a control-plane change after `F`.**
- It happens in the last pre-`F` commit, which is `F` or a commit before it, and `G9` permits it.
- `G7` forbids control-plane changes only after `F`.
- PLAN step 6 lists the deletion among the candidate-`F` conditions.

## R4-N2, the lexer (planner's claim 3)

The char-literal rule is correct. A `'` after an identifier character belongs to the identifier. Otherwise a char
literal is skipped only when it is complete under the exact grammar, and an incomplete one skips nothing. The escape
list now matches Lean 4, and the earlier `\u{…}` form is gone. The self-test cases `h𝓘' instance` and `'a instance`
are present. The identifier-class transcription is **inaccurate**; see R5-N1.

## R4-N3 and R4-N4

Both are closed.
- **R4-N3.** The dump script now carries `namespace OIBridge`, `namespace PolarizedProtocol` and the frozen `open`
  line, which stays PENDING until the design run fixes it.
- **R4-N4.** The dump step now sits directly after `Build` and before `Release gate`. L0, L, A and M therefore stay the
  bridge job's last four steps, and `derive-run` runs on the design run's answers unchanged.

## Non-blocking findings (required by candidate `F`)

### R5-N1: the transcription of the identifier classes is incomplete against Lean `v4.33.0`

`src/Init/Meta/Defs.lean` at tag `v4.33.0` defines the following. The items marked **missing** are absent from the r5
text.

`isLetterLike`:
- `0x3B1–0x3C9` except `0x3BB` (lower Greek except λ);
- `0x391–0x3A9` except `0x3A0` and `0x3A3` (upper Greek except Π and Σ);
- `0x3CA–0x3FB` (Coptic);
- `0x1F00–0x1FFE` (Greek Extended);
- `0x2100–0x214F` (Letterlike Symbols);
- `0x1D49C–0x1D59F` (Mathematical Alphanumeric Symbols);
- **missing:** `0x00C0–0x00FF` except `0x00D7` (×) and `0x00F7` (÷), the Latin-1 Supplement letters;
- **missing:** `0x0100–0x017F`, Latin Extended-A.

`isSubScriptAlnum`:
- `0x2080–0x2089`, `0x2090–0x209C` and `0x1D62–0x1D6A` (the r5 text gives no ranges for these);
- **missing:** `0x2C7C`.

`isIdFirst` is `c.isAlpha`, `_`, or a letter-like character. `isIdRest` adds `c.isAlphanum`, `'`, `!`, `?` and the
subscript alphanumerics.

**Effect.** The r5 class is narrower than Lean's, so it errs on the safe side. The lexer splits more than Lean does:
- `éinstance` would yield the token `instance`, a false hit, which fails N1 and costs only a proof rewrite;
- a `'` after `é` could open a complete one-character literal, which hides no keyword.

It can never merge or skip text that Lean reads as a command. The frozen text nonetheless claims "Lean's own classes,
transcribed", which is false as written.

*Fix:* write the exact ranges above into the preregistration and into `controls.py`, citing the file and tag. Add one
self-test case in which `é` and `ŝ` are identifier characters.

### R5-N2: the drafting note's floor-only edit list is incomplete

Under `floor-only`, two further route-dependent sites need an edit:
- the result-note rule "It also interpolates the dump's `non_indexed_leading_parsers` count";
- precondition 2's dump-step and script paragraph, which must be kept as a record of the attempt or reworded to say
  the dump was not admitted.

*Fix:* add both to the drafting note's list, and to P's route-dependent sites, so that a `floor-only` `F` carries no
dump-route wording.

### R5-N3: make "the reference set is not edited after the dump is seen" checkable

Commit the reference set as it stands in r5 in the round PR's first control-plane commit, before the design run's
dump step runs. The PR's commit order then shows the rule was kept. The design PR records the dump run's id and the
round-branch commit current at that time.

## Summary

- **Verdict:** ACCEPT WITH CHANGES, with no blocking finding.
- **Closed:** R4-B1 and R4-N1 to R4-N4.
- **V3 blocks:** byte-identical, digest `81897a90…5107`, and `HOLDS` reproduced.
- **After `F`:** no route discretion remains, and deleting the drafting note is a pre-`F` change.
- **Reachability:** `notation3` and `irreducible_def` are reachable from the closure with high confidence. If they
  were not, the result would be a `floor-only` route, never a vacuous control.
- **Required by candidate `F`:** R5-N1 (the identifier ranges, incomplete but safe), R5-N2 (two more floor-only edit
  sites) and R5-N3 (commit order for the reference set).

Generated by Claude Code

amaybaum · 2026-11-08T14:12:31Z

Independent review of the MATH-CON-1-S1B-1 round draft r6 (scratchpad; prereg sha256 34f424e32e34c98be6d231cbe124346bb9de355234e9120f023156fc8eb1429d, PLAN sha256 2034a03238ae1a36164ed12f1067670cc2c9583094b96c72de9496786f125553). Verdict: ACCEPT WITH CHANGES (one blocking finding, R6-B1, floor-only route; R6-N1–N2 by candidate F). Model review, not human verification.

REVIEW-PLAN-r6.md

# Independent re-review (r6): MATH-CON-1-S1B-1 round draft, focused check

## Objects reviewed

| file | sha256 |
| --- | --- |
| `preregistration.draft.md` (r6) | `34f424e32e34c98be6d231cbe124346bb9de355234e9120f023156fc8eb1429d` |
| `PLAN.md` (r6) | `2034a03238ae1a36164ed12f1067670cc2c9583094b96c72de9496786f125553` |
| `preregistration-r5.draft.md` (diff base) | `36cc740af35a654bb96e11a9ef73b3e71ca59042fb00f020b35bd512fd23c3eb` |
| `PLAN-r5.md` (diff base) | `bcd2d160549b5473d3fe14bffa4c830fa961519b4ec3edd5f73d71415f0be29d` |

All four hashes match the coordinator's. I am the same independent reviewer as for r1–r5, not the writer. I made no
Lean build, no push and no GitHub write.

## Verdict: **ACCEPT WITH CHANGES**

- **Blocking: one finding, R6-B1.** It concerns the floor-only route only.
  - The marker rule's own prose contains the markers it forbids under `floor-only`. A floor-only `F` would therefore
    fail P.
  - It is not caught silently: `mock-s1` (precondition 5) would fail at candidate `F`. Even so, as written one of the
    two preregistered routes cannot be realized.
  - The fix is one sentence. It must be in place by candidate `F`, not before round-PR preparation.
- **The coordinator's three dump-run checks pass.** No dispatch is needed. The design-only step never reaches the
  round branch. The round-branch commit is well defined and checkable.
- **Wording and one sufficiency gap.** The wording ("dispatched") should change, and one gap in what the timestamps
  prove should be closed: R6-N1 and R6-N2, required by candidate `F`.

## Checks run

| check | result |
| --- | --- |
| V3 blocks | byte-identical to r1–r5 |
| verifier probe on the r6 text | `VERDICT  HOLDS`, governed-paths digest `81897a90a068b0402e68393f82cffda8fd83f0bda5283316c38d8c58b28e5107` |
| marker strings | grepped every occurrence of the four route markers in r6 (results under R6-B1) |

## The coordinator's three checks on the dump run

### 1. No `workflow_dispatch` or other special launch: **passes**

- PLAN step 5 says "ordinary `pull_request` CI: no dispatch, no A42 matrix".
- Precondition 2 says "The ordinary pull-request CI runs it".
- The added `order.json` input, `GET …/actions/runs/{id}`, is a read.

The only problem is wording. Scan list (i), item 2 says the round-branch commit is the one "current when that run was
**dispatched**". The run is a `pull_request` run, so nothing is dispatched. This is R6-N1.

### 2. The design-only step never reaches the round branch before `F`: **passes, and this is enforced mechanically**

- Precondition 2 places the step only on the disposable design branch. W refuses it at S1 and `E`.
- Two independent mechanisms also prevent any non-control-plane commit on the round branch in `D..F`:
  - `tools/v3_verifier.py` `check_t1()`, which reports `t1:non-control-plane-change`, so `--verify-round` fails;
  - control T, under which `delta(D, F)` is the control plane only.

So the step cannot reach the round branch before `F` without the round failing.

*Optional:* one explicit sentence in precondition 2, "the design branch is never merged into or committed to the round
branch".

### 3. The round-branch commit is well defined and checkable: **passes, in a form that is sufficient**

**Well defined.** The commit is named explicitly, as 40 hex characters, on the frozen
`command-scan dump run: <id> at round-branch commit <sha>` line.

**Checkable.** Three checks apply:
- P checks that the commit lies in `D..F` and carries the reference-set line.
- P checks that the reference-set line is byte-identical from the first control-plane commit through `F`.
- `order.json`'s `dump` entry shows, from host timestamps, that this commit's first host run was created before the
  dump run.

**The design branch need not be built from that commit.** The property R5-N3 needs is only this: the reference set
was published on the round branch before the dump run started. The three checks establish exactly that.

**"Current at dispatch" is neither true nor checked.** The design branch is built from `D`, not from the round commit,
and nothing measures "current". The prose should describe what is checked. That is R6-N1.

**The gap is earlier dump runs.** The checks bind only the dump run named on the line. A design-branch run that
produced a dump *before* the reference set was published would go unmeasured. That is the situation the rule "fixed
before the dump is seen" is meant to exclude. This is R6-N2.

## R5-N1: the identifier ranges against Lean `v4.33.0`

**Correct.** They match my reading of `src/Init/Meta/Defs.lean` at tag `v4.33.0`:
- **`isLetterLike`:** all eight ranges and all four exceptions (λ, Π, Σ, ×, ÷).
- **`isSubScriptAlnum`:** `0x2080–0x2089`, `0x2090–0x209C`, `0x1D62–0x1D6A` and `0x2C7C`.
- **`isIdFirst`:** `Char.isAlpha` (ASCII), `_`, or `isLetterLike`.
- **`isIdRest`:** equivalent to Lean's own definition, `c.isAlphanum || '_' || '\'' || '!' || '?' || isLetterLike ||
  isSubScriptAlnum`.

Two further pieces close the finding:
- **Toolchain pin.** S2's check that `lean-toolchain` pins `leanprover/lean4:v4.33.0` keeps the tables bound to the
  toolchain they were read from.
- **Self-test cases.** `éinstance`, `ŝinstance` and `instanceé` each pass as one identifier, `hŝ' instance` fails, and
  `×` and `÷` are not identifier characters.

## R5-N2 and R5-N3

- **R5-N2.** The drafting note's edit list now names:
  - the `non_indexed_leading_parsers` interpolation rule;
  - precondition 2's paragraph, replaced by a fixed "not admitted" sentence;
  - the reference-set and dump-run lines.

  It is closed except for R6-B1.
- **R5-N3.**
  - The reference-set line is required in the round PR's first control-plane commit and is held byte-identical
    through `D..F`.
  - The dump-run line and `order.json`'s ordering conjunct are added, with self-test cases.

  It is closed, with the R6-N2 refinement.

## Blocking finding

**R6-B1. The floor-only marker check fails on its own rule text.**

The rule says P checks route agreement by four markers: `evidence/command-tokens.json`,
`non_indexed_leading_parsers`, `IO.FS.writeFile` and the reference-set line. Under `floor-only`, "none occurs".

Two passages contain those markers literally and are **not** route-dependent sites, so they survive the floor-only
edits:
- **line 334:** the enumeration of route-dependent sites, "the result-note rule that interpolates
  `non_indexed_leading_parsers`";
- **lines 341–342:** the marker rule itself, which names all three string markers.

A preregistration edited exactly as the drafting note prescribes would therefore still contain the markers, and P
would fail at `F` under `floor-only`. `mock-s1` would catch this at candidate `F`, so the round would not silently
fail. But one preregistered route cannot be realized as written, and which route applies is decided only after the
dump is seen.

**Minimal fix, either of:**
- **(a)** P counts marker occurrences only *within* the enumerated route-dependent sites, located by their section
  anchors, and never in the *route line* paragraph or the enumeration.
- **(b)** Replace the prose markers with dedicated column-0 machine lines that appear nowhere in rule prose. For
  example, put one line `command-scan site: dump` at each route-dependent site under `dump`, and have P require
  exactly *k* such lines under `dump` and zero under `floor-only`.

Either way, add a positive self-test: a preregistration edited exactly as the drafting note prescribes for
`floor-only` passes P.

Also keep the route-line self-test cases under both routes. These are `PENDING`, the line appearing twice, a
disagreeing site, and a remaining drafting note. They currently sit in the "Dump consistency (P; route `dump`)" list,
which the floor-only edit replaces wholesale.

## Non-blocking findings (required by candidate `F`)

**R6-N1. Reword "dispatched", and claim only what is checked.** Replace "the round-branch commit current when that run
was dispatched" with this: "a round-branch commit in `D..F` that carries the reference-set line and whose first host
run (a `pull_request` run) was created before the dump run". Make the same change in PLAN §5 R5-N3, which says
"current at dispatch".

**R6-N2. Bind every dump-producing design run, not only the named one.**
- Add the design branch's runs capture to `order.json`, with every page, checked against `total_count`, as for the
  other captures.
- Extend the ordering rule: the design branch's earliest run must be created after the first host run of the round
  PR's first control-plane commit.
- That shows no design-branch run, and so no dump, existed before the reference set was published.
- Add a self-test case in which an earlier design-branch run fails.

## Summary

- **Verdict:** ACCEPT WITH CHANGES.
- **Blocking:** one, R6-B1. The floor-only markers occur in the marker rule's own prose; the fix is to scope the check
  to the route-dependent sites, or to use dedicated column-0 site lines.
- **Required by candidate `F`:**
  - R6-N1, reword "dispatched";
  - R6-N2, require the design branch's earliest run to postdate the reference set's publication.
- **Coordinator's checks:**
  1. no dispatch is needed;
  2. the design-only step never reaches the round branch before `F`, which `t1:non-control-plane-change` and control T
     enforce;
  3. the round commit is well defined and checkable, and sufficient without building the design branch from it.
- **R5-N1:** the ranges match Lean `v4.33.0` exactly.
- **V3 blocks:** unchanged, `HOLDS`, digest `81897a90…5107`.

Generated by Claude Code

…t scan) PR CI run 42481551235 failed "SC-42 integration source scope and must-fail controls" on the local-path pattern matching the row label "R4: scratchpad citation" (DESIGN.md:758). The label now reads "R4: review citation". Editorial only: no other text changes; the row's content and every other line of the design are unchanged. 41a42cb stays the parent. Owner-authorized on 2026-11-08 (chat). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

amaybaum · 2026-11-08T14:20:28Z

Independent review of the MATH-CON-1-S1B-1 round draft r7 (scratchpad; prereg sha256 b2076efab4898f75a4c056bd1c668f1668bbbdd6cbb67a856a9d732e19f38356, PLAN sha256 08b034eb861e1b3ec420f5911d64a08897567cadab406fd9f429a1523fe0e54f). Verdict: ACCEPT WITH CHANGES (no blocking findings; R7-N1–N5 by candidate F, of which N1 and N2 complete enforcement of owner conditions 3 and 5). Model review, not human verification.

REVIEW-PLAN-r7.md

# Independent re-review (r7): MATH-CON-1-S1B-1 round draft

## Objects reviewed

| file | sha256 |
| --- | --- |
| `preregistration.draft.md` (r7) | `b2076efab4898f75a4c056bd1c668f1668bbbdd6cbb67a856a9d732e19f38356` |
| `PLAN.md` (r7) | `08b034eb861e1b3ec420f5911d64a08897567cadab406fd9f429a1523fe0e54f` |
| `preregistration-r6.draft.md` (diff base) | `34f424e32e34c98be6d231cbe124346bb9de355234e9120f023156fc8eb1429d` |
| `PLAN-r6.md` (diff base) | `2034a03238ae1a36164ed12f1067670cc2c9583094b96c72de9496786f125553` |
| `scratchpad/mockP/mock_p.py` | run as given |

All hashes match the coordinator's. I am the same independent reviewer as for r1–r6, not the writer.

I fetched `origin/research/mathcon1-prereg-20261108` without `--depth` and read it only. I made no Lean build, no push
and no GitHub write.

## Verdict: **ACCEPT WITH CHANGES. No blocking finding.**

- R6-B1, R6-N1 and R6-N2 are closed, and the floor-only route can now be carried out.
- The new design pin is correct.
- Each of the owner's six conditions has a control or precondition at the point of decision.
- Two of the conditions, 3 (no special dispatch) and 5 (V3 blocks unchanged), are enforced only by a check run once,
  or by review, and leave no durable, machine-checked record. R7-N1 and R7-N2 close that.
- The owner's authorization of the design edit must be quoted from a recorded comment (R7-N3).
- These items, with two small text fixes (R7-N4 and R7-N5), are required by candidate `F`. None needs another review
  cycle; the pre-`F` re-review in PLAN step 6 checks them.

## Checks run

| check | result |
| --- | --- |
| V3 blocks | byte-identical to r1 through r6 |
| verifier probe on the r7 text | `VERDICT  HOLDS`, governed-paths digest `81897a90a068b0402e68393f82cffda8fd83f0bda5283316c38d8c58b28e5107` |
| site lines | exactly seven standalone column-0 `command-scan site: dump` lines (lines 375, 752, 886, 1033, 1146, 1189, 1236); everywhere else site lines appear only in backticks |
| other column-0 machine lines | one route line, one reference-set line, one dump-run line; none of these lines falls inside the drafting note |
| mock | `python3 -I -B mockP/mock_p.py preregistration.draft.md` prints `MOCK OK`, 8 of 8 cases as expected |
| design pin | correct (see the design-pin section below) |

## R6 findings

- **R6-B1: closed.**
  - The prose markers are gone. P counts only dedicated column-0 site lines: exactly seven, each naming the route
    word.
  - Under `dump`, the reference-set line and the dump-run line each occur exactly once. Under `floor-only`, neither
    occurs.
  - The drafting note gives a floor-only replacement for every site.
  - The route-line self-test cases moved to a list that applies to both routes and sits before site 6, so a
    floor-only edit no longer deletes them.
  - Positive cases now exist for both routes.
- **R6-N1: closed.** The text claims only what is checked: a commit in `D..F` that carries the reference-set line and
  whose first `pull_request` run precedes the dump run. "Nothing is dispatched" is stated.
- **R6-N2: closed.**
  - Every page of the design branch's runs is captured and checked against `total_count`.
  - The ordering rule requires the design branch's earliest run to come after the first host run of the round PR's
    first control-plane commit.
  - The self-test covers both failure cases.

## The mock against the frozen rule

The eight cases match the frozen rule text (*Site lines*, *The route line*):

| frozen rule | mock |
| --- | --- |
| one route line, exactly `dump` or `floor-only (completeness unverified)`; not `PENDING` | `route-line-count` and `route-line-value` |
| no `*Drafting note` line | `drafting-note-remains` |
| exactly seven site lines, each naming the route | `site-count` and `site-route-mismatch` |
| under `dump`, one reference-set line and one filled dump-run line | `ref-line-count` and `dump-run-line` |
| under `floor-only`, neither of those lines | `dump-lines-remain-under-floor-only` |

The floor-only text, edited as the drafting note prescribes, passes, and so does the filled `dump` text. Each
defective variant fails for its stated reason.

**Limit.** The mock edits only site 1's text and the site lines. Since P counts lines and nothing else, that is
enough for P. It does not show that the other sites' text is rewritten correctly. A leftover site-5 entry, for
example, would make P demand `command-tokens.json` under `floor-only`. `mock-s1` at candidate `F` would catch that.
P's code must read the route line and require route-specific evidence only under `dump`.

**Realizability.** The floor-only route can now be carried out as written.

## The new design pin

All of the following were read from `origin/research/mathcon1-prereg-20261108`:

| item | finding |
| --- | --- |
| branch head | `06b5d4f23895baebf1372b6a4cbb2c85f5044458`, a commit |
| parent | exactly one, `41a42cb97e5e044f5a9e906e33fbf6f22de52dc4` |
| `DESIGN.md` blob at `06b5d4f2` | `4d47fbc876427a26dff12a486fa43a67a95aac5b` |
| file sha256 | `6f502c51e2e362621773f84454131671ae0c6baab46f2678b4fa09d174d61e3d` |
| `git diff 41a42cb9 06b5d4f2` | one file, one line: `DESIGN.md:758`, `\| R4: scratchpad citation \|` becomes `\| R4: review citation \|`; the row's content is unchanged |

- The commit message gives the reason: SC-42 matched the local-path pattern in the label in PR run 42481551235. It
  says "Owner-authorized on 2026-11-08 (chat)".
- The preregistration's design paragraph, DS, precondition 1, and PLAN steps 0, 1 and §6 all pin `06b5d4f2` and
  `4d47fbc8…` consistently.
- The owner's acceptance quote "accepted at `41a42cb9`" is kept verbatim.
- The V3 digest does not depend on the pin, because neither block names `DESIGN.md`.

See R7-N3 for the authorization record.

## The owner's conditions: is each enforced?

| condition | enforcement found | assessment |
| --- | --- | --- |
| **1. The command-table check stays on a separate throwaway branch, under ordinary PR CI** | Precondition 2 (a disposable design branch with its own draft PR). W refuses the design-only step at S1 and `E`. Precondition 7 requires that no design commit is an ancestor of `F`. P checks again at S1 and `E` that the dump's design commit is not an ancestor of `F`. `check_t1` makes any such commit fail `--verify-round`. | **Enforced.** |
| **2. No execution-related commit on the round branch before `F`** | Control T, and `check_t1` (`t1:non-control-plane-change`), run on the candidate (precondition 7), at S1 and `E` (T), and in `--verify-round Q`. | **Enforced**, at three points. |
| **3. No special CI dispatch** | Precondition 7 checks the event of every design-branch run from the captured answers. `order.json`'s `dump.event` must be `pull_request`, and P checks it at S1 and `E`. | **Only partly durable.** Three gaps: (a) the design branch's other runs are checked only once, before `F`, from answers that are not retained; under `floor-only` the design branch is not captured at all; (b) round-branch runs before `F` other than the approved `F` attestation run are not checked; (c) dev-branch runs are not checked. See R7-N1. |
| **4. Provenance: toolchain, command-table output, source commit, validated round revision** | The five-field dump-run line, with P checking each field against its other source. The file lands at S1 and is pinned at `F`. | **Enforced.** Two refinements in R7-N5: the toolchain comparison needs a stated normalization, and the Mathlib revision should be recorded. |
| **5. Both V3 blocks unchanged** | Review across r1–r7, and `--verify-round Q`, which *re-derives* the digest at `F`. | **Asserted, not enforced.** Re-deriving the digest compares it to nothing. See R7-N2. |
| **6. If branch compliance cannot be established, halt before `F`** | Precondition 7: if any bullet fails, no `F` is requested, preparation stops, and the finding is reported on the PR. | **Enforced** as a gate before `F`, which is the only place a halt before `F` can be. It inherits condition 3's gap through its third bullet. |

## Non-blocking findings, required by candidate `F`

**R7-N1. Make condition 3 durable and complete.**
- **Record every relevant run.** `order.json` already captures every page of the runs for the round branch and the
  dev branch. Under **both** routes, add the design branch's capture, and record the set of `event` values seen on
  each branch.
- **Ordering rule, extended:**
  - every design-branch run is `pull_request`;
  - every dev-branch run is `pull_request`;
  - every round-branch run whose `head_sha` is in `D..F` is `pull_request`, except the one `workflow_dispatch` run at
    `F` that the `F` check-run attestation names;
  - after `F`, the only round-branch `workflow_dispatch` runs are those at S1 and `E` named by their approvals.
- **Re-check at S1 and `E`.** P checks all of this, so precondition 7's third bullet becomes a check that leaves a
  record on `main`, not a one-time reading.
- **Self-test.** A `workflow_dispatch` design-branch run fails, and so does an extra round-branch dispatch.

**R7-N2. Make condition 5 a check.**
- Freeze the expected governed-paths digest
  `81897a90a068b0402e68393f82cffda8fd83f0bda5283316c38d8c58b28e5107` and the three `v3-round` lines in the
  preregistration's prose, outside the blocks.
- Have precondition 7, and control T at S1 and `E`, recompute the digest from `F`'s blocks with `tools/v3_verifier.py`'s
  `parse_governed_text` and `governed_digest`, and compare it.
- A mutation self-test, an altered block, fails.
- The probe I ran is the template: it parses the draft and prints the digest.

**R7-N3. Quote the owner's authorization of the design edit from a record (§A.42 item 7; §A.45 rule 3).**
- The preregistration, PLAN §5 and `06b5d4f2`'s commit message say only "owner-authorized … 2026-11-08 (chat)". No
  comment records it. The comments on file from 2026-11-08 are the owner decision 6721662886 and review postings.
- The step-0 request asks the owner to approve landing #1206 at head `06b5d4f2`. Have that recorded comment also state
  the label correction.
- Quote it under *Authority* with comment id, author and time. It stays PENDING until recorded, so control P refuses
  it at `F`.

**R7-N4. Two text fixes.**
- The ordering rule says "all three of these hold" (line 932) and lists four bullets.
- The `author is amaybaum` check (line 928) shows only that the comment was posted under the owner's account. The
  coordinating session also posts as `amaybaum`; the review comments 6721957164–6722542847 are examples. The record
  therefore establishes "the owner's designation" through the quoted owner words, as KTRANS-SEP-2's receipt did, not
  through the login. Say so, and do not present the author check as proof of human authorship.

**R7-N5. Specify the toolchain comparison.**
- State the normalization between `leanprover/lean4:v4.33.0` (`lean-toolchain`) and the dump's `toolchain` field
  (`Lean.versionString`, for example `4.33.0`).
- Record the resolved Mathlib revision in the dump file and on the dump-run line. The lakefile pins it only by the tag
  `v4.33.0`, and no `lake-manifest.json` is committed. The command table depends on Mathlib as well as on Lean, so
  "exact toolchain" should cover both.
- Name the command that runs precondition 7's `check_t1`. It is a library function, not a CLI mode of
  `tools/v3_verifier.py`.

## Summary

- **Verdict:** ACCEPT WITH CHANGES, with no blocking finding.
- **Closed:** R6-B1, R6-N1 and R6-N2. The floor-only route can be carried out; the mock gives 8 of 8 and matches the
  frozen rule.
- **Design pin:** confirmed. `06b5d4f2` has the single parent `41a42cb9`, its blob is `4d47fbc8…` (sha256
  `6f502c51…1e3d`), and it changes one label line.
- **V3 blocks:** unchanged; digest `81897a90…5107` and `HOLDS` reproduced.
- **Owner conditions:** 1, 2, 4 and 6 are enforced. Condition 3 is enforced only for the dump run and only once before
  `F` for the rest (R7-N1). Condition 5 is asserted by review (R7-N2).
- **Required by candidate `F`:** R7-N1 to R7-N5.

Generated by Claude Code

amaybaum · 2026-11-08T14:28:45Z

Merge record: #1206 (MATH-CON-1 design)

Merged as a normal merge commit 2cd49dc082ee7b2a026fd6d1fb4a6168f92fac51.

First parent: 5ce4f98ec3a76aee6fdd17ed1bad7b278f1d9732 (main).
Second parent: 06b5d4f23895baebf1372b6a4cbb2c85f5044458 (PR head).
The merge tree e67ec2d78251ccaf63892046ae0c810e0a978b16 equals the pre-merge git merge-tree --write-tree result.
41a42cb97e5e044f5a9e906e33fbf6f22de52dc4, the commit at which the owner accepted the design, and 06b5d4f2 are both reachable from main.

What landed. verification/programmes/oi-qm/reconstruction/mathcon1-polc-20261108/DESIGN.md as accepted at 41a42cb9, plus one editorial commit:

06b5d4f2, whose single parent is 41a42cb9, changes only the §13 row label at line 758, from "R4: scratchpad citation" to "R4: review citation".
The 41a42cb9 head had failed PR CI run 42481551235 at "SC-42 integration source scope and must-fail controls", because the checker's local-path pattern matched that label.
New DESIGN.md blob: 4d47fbc876427a26dff12a486fa43a67a95aac5b, file sha256 6f502c51e2e362621773f84454131671ae0c6baab46f2678b4fa09d174d61e3d. Old blob: 27359cbd452a55ba26769b3b9d6fb518630f8898.

Owner authorization (amaybaum, in the coordinating Claude Code session's chat, 2026-11-08; quoted verbatim):

Yes, you have my authorization to make the one-word scratchpad → review correction.

This was explicitly approved in my previous decision.

The authorization includes creating a new commit, obtaining independent confirmation of the editorial-only change, requiring green exact-head CI, and performing a normal merge after checking compatibility with current main.

Preserve the accepted 41a42cb9 commit in the ancestry. Verify green post-merge main CI.

No additional design edits are authorized.

The owner's earlier decision on #1206 is c.6722109292 (step 0: merge as a normal merge commit).

Checks performed

Independent confirmation (model reviewer; read-only; 7/7 PASS):
- single parent;
- a one-line diff, reproduced byte for byte;
- the new label is accurate for the row;
- no local-path strings remain in the added text;
- the SC-42 checker exits 0 at 06b5d4f2, and exits 1 with the single hit at 41a42cb9 as a control;
- the merge with main is clean;
- the commit message matches the change.
Exact-head CI on 06b5d4f2: run 42488701308 (pull_request), all check runs green (25 success, 1 skipped matrix placeholder).
Post-merge main CI on 2cd49dc0: run 42489463543 (push), all check runs green (25 success, 1 skipped).

No other design edits were made. This record is the GitHub record of the owner's authorization of the 06b5d4f2 edit. The MATH-CON-1-S1B-1 round draft cites it in its Authority section.

Generated by Claude Code

amaybaum · 2026-11-08T14:35:54Z

Independent review of the MATH-CON-1-S1B-1 round draft r8 (scratchpad; prereg sha256 a8358bc532a70c72d8a782a5fea48d319347f1239fccb9c18df1f51ceb60b2ac, PLAN sha256 c4c0b7d7996630aa7e1741f16d6919ca3891f176d90951ee50ffb8f6b8988362). Verdict: REVISE (narrow; R8-B1 branch identities, R8-B2 single-dispatch trap). Model review, not human verification.

REVIEW-PLAN-r8.md

# Independent re-review (r8): MATH-CON-1-S1B-1 round draft

## Objects reviewed

| file | sha256 |
| --- | --- |
| `preregistration.draft.md` (r8) | `a8358bc532a70c72d8a782a5fea48d319347f1239fccb9c18df1f51ceb60b2ac` |
| `PLAN.md` (r8) | `c4c0b7d7996630aa7e1741f16d6919ca3891f176d90951ee50ffb8f6b8988362` |
| `preregistration-r7.draft.md` (diff base) | `b2076efab4898f75a4c056bd1c668f1668bbbdd6cbb67a856a9d732e19f38356` |
| `PLAN-r7.md` (diff base) | `08b034eb861e1b3ec420f5911d64a08897567cadab406fd9f429a1523fe0e54f` |

All hashes match the coordinator's.
- I am the same independent reviewer as for r1–r7, not the writer.
- I fetched `origin/main` without `--depth`; its head is `2cd49dc082ee7b2a026fd6d1fb4a6168f92fac51`.
- I made no Lean build, no push and no GitHub write.

## Verdict: **REVISE (narrow). Not yet an ACCEPT.**

Two blocking findings remain. Both concern how the owner's conditions 1 and 3 are enforced, which the owner requires
to be done by controls. Each fix is a few lines of frozen text plus self-test cases:

- **R8-B1.** The design-branch and dev-branch names are not fixed before `F`. The run evidence can therefore be taken
  from a branch the writer chooses.
- **R8-B2.** "Exactly one `workflow_dispatch` in `D..F`" is a trap. A candidate `F` that is re-cut, or an `F` dispatch
  that is retaken (both of which §A.39 permits once the owner approves), makes the rule impossible to satisfy for that
  `D`.

**Apart from these two, and apart from the PENDING merge-record id, I would ACCEPT r8.** The PENDING id is expected,
and control P refuses it at `F`. Every other part of r8 is closed and checked: R7-N1 to R7-N5, the V3 blocks, the
precondition 7 command and the handling of `D`.

## Checks run

| check | result |
| --- | --- |
| V3 blocks | byte-identical to r1–r7 |
| verifier probe on r8 | complete path `VERDICT  HOLDS`, halted path `HOLDS`, digest `81897a90a068b0402e68393f82cffda8fd83f0bda5283316c38d8c58b28e5107` |
| precondition 7 command (extracted verbatim, run on a scratch round built from the r8 text) | clean candidate: exit 0, printing the frozen round lines and digest. Three mutations each exit 1: (i) `execution AM` on the module gives digest `11d5a061…`; (ii) a non-control-plane commit before `F` gives `t1:non-control-plane-change`; (iii) `kind sealing` gives a kind mismatch plus `t1:seal-record-entry`. |
| mock `mock_p.py` | `MOCK OK`, 8/8 |
| `main` after #1206 | `2cd49dc0` has parents `5ce4f98e` and `06b5d4f2`, is on `main`'s first-parent chain, and carries `DESIGN.md` at blob `4d47fbc876427a26dff12a486fa43a67a95aac5b`; `41a42cb9` is reachable from it; no path under `verification/lean-mathlib`, `verification/lean`, `.github` or `tools` changed from `b73acf38` to `2cd49dc0` |

## R7 findings

- **R7-N1 (condition 3), closed except for R8-B1 and R8-B2.**
  - `runs-to-f.json` covers the design branch and the round branch from `D` to `F`.
  - `order.json` covers events on the design branch, the dev branch and the round branch after `F`, plus
    `approved_dispatches`.
  - P re-checks at S1 and `E`, and there are self-tests.
- **R7-N2 (condition 5), closed.** The digest and the three round lines are frozen in prose. Precondition 7 and
  control T re-derive them, and I confirmed the exact command myself.
- **R7-N3, closed as drafted.** The Authority line cites the #1206 merge record. It stays PENDING, and P refuses
  PENDING at `F`. The authorization rests on the quoted owner words, and the transmitted words are included.
- **R7-N4, closed.** "four"; `quoted_words` must contain `F`'s full id; the `author` login is not treated as evidence
  of human authorship.
- **R7-N5, closed.**
  - The toolchain normalization is exact: the content minus `leanprover/lean4:v` must equal `Lean.versionString`,
    with self-tests.
  - `mathlib_rev` is in the dump and on the six-field line.
  - The `check_t1` command is exact and works.

## Question 4: does r8 assume `D = 5ce4f98e`?

**No.**
- `D` is PENDING and defined as the head of `main` after #1206's merge, so it is `2cd49dc0` or later.
- Precondition 1 requires `06b5d4f2` and `41a42cb9` to be reachable, and `D`'s `DESIGN.md` to be at blob `4d47fbc8…`.
  All of this holds at `2cd49dc0`.
- The drift paragraph measures only up to `b73acf38`. I confirmed there is no drift from there to `2cd49dc0` in Lean,
  CI or tools, and S2 re-measures at `D`.

*Text note.* When `D` is filled in, extend the drift sentence to "`b73acf38` → `D`".

## The six owner conditions (PLAN §5, r8 table)

| condition | enforced durably? |
| --- | --- |
| 1. separate throwaway branch, ordinary PR CI | **Not yet.** The branch whose runs are recorded is not fixed before `F` (R8-B1). |
| 2. no execution commits on the round branch before `F` | **Yes.** The precondition 7 command, control T at S1 and `E`, and `--verify-round` (`t1:non-control-plane-change`). |
| 3. no special CI dispatch | **Not yet.** It depends on R8-B1 (which branches are inspected) and R8-B2 (the rule for dispatches up to `F`). |
| 4. provenance of toolchain, output, source commit and round revision | **Yes.** The six-field line, cross-checked by P, with `command-tokens.json` pinned. |
| 5. both V3 blocks unchanged | **Yes.** The frozen expectation, the precondition 7 command, and T with a mutation self-test. Verified. |
| 6. halt before `F` if compliance cannot be established | **Yes**, as a pre-`F` gate. A halt before `F` leaves no V3 object to record, so the PR record is the right home. Its third bullet inherits R8-B1 and R8-B2. |

## Blocking findings

### R8-B1. Fix the design-branch and dev-branch identities before `F`

`runs-to-f.json` and `order.json` take `design_branch.name` and `dev_branch.name` from whatever branch the writer
captures. Neither name is frozen. Under `dump`, P ties the dump run to a design commit, but nothing ties that run's
`head_branch` to the captured branch. Under `floor-only`, nothing ties anything at all.

A clean branch could therefore be recorded while the work, or a dispatch, ran on another branch. The owner's
conditions 1 and 3 are then asserted, not enforced.

**Minimal fix:**
1. **Freeze the names.** Add one column-0 line to the round PR's first control-plane commit, held byte-identical
   through `D..F` exactly like the reference-set line:
   `command-scan branches: design draft/mathcon1-s1b-1-skeleton; dev <name>`
2. **Record the design PR.** Add the design PR's number to the dump-run line, or to precondition 2's record under
   `floor-only`.
3. **P checks, at S1 and `E`:**
   - `runs-to-f.design_branch.name` and `order.json`'s `design_branch.name` and `dev_branch.name` equal the frozen
     names;
   - the dump run's `head_branch` equals the design name, and its `pull_requests[].number` contains the design PR;
   - for every commit of the design branch, read through git while it exists and recorded as provenance,
     `GET …/actions/runs?head_sha=<sha>` shows only `pull_request` runs. This closes a dispatch on another branch
     that points at the same commit.
4. **Self-tests:** a renamed design branch fails; a dump run on another branch fails; a `workflow_dispatch` that
   carries a design commit's `head_sha` fails.

### R8-B2. Replace "exactly one `workflow_dispatch` in `D..F`" with "every dispatch approved; the `F` attestation among them"

§A.39 lets an `F` attestation be retaken. A candidate `F` can also be held, dispatched, found red and re-cut, and the
re-cut candidate's `D..F` still contains the earlier candidate as an ancestor. A retaken `F` dispatch is a new run id
with `head_sha F`. Either case puts two `workflow_dispatch` runs in `D..F`.

Each case is legitimate when owner-approved. Yet the frozen rule makes P fail at S1 and `E` for that `D` forever,
since `F` cannot change.

**Minimal fix:** give `runs-to-f.json` an `approved_dispatches_to_f` list, built the same way as `order.json`'s, and
set the rule to:
- every `workflow_dispatch` in `D..F` appears in `approved_dispatches_to_f`;
- exactly one of those entries is the `F` attestation, with `head_sha` = `F` and `run_id` = the run in
  `f-run/results.json`;
- every other run is `pull_request`.

Self-tests: a re-cut candidate's approved dispatch passes, and an unapproved one fails.

## Non-blocking finding: requirements on every approval entry (`approved_dispatches`, and its pre-`F` twin)

"Quoted owner words" alone is not enough. Each entry's approval comment must:
- quote owner words that name the dispatched commit by its **full id** (as the designation rule already requires for
  `F`), and the stage: F, S1, re-dispatch after VOID, or the replacement `E` candidate;
- have a `created_at` earlier than the run's `created_at`.

In addition:
- each approval authorizes **one** run, so no comment id appears twice;
- the run's `head_sha` equals the quoted id.

Self-tests: a reused approval, an approval posted after its run, and an approval quoting another commit each fail.

*Note:* dispatches at or after `E` lie outside `order.json`, which is written at S2. They are recorded by the
receipt's `check-run` attestations, so say so, and require the approval to be quoted in each attestation record under
the same rules.

## Summary

- **Verdict:** REVISE, narrowly.
- **Blocking:**
  - R8-B1: freeze the design and dev branch names and the design PR before `F`, and bind the runs to them by
    `head_branch`, PR number and `head_sha`;
  - R8-B2: replace "exactly one `workflow_dispatch` in `D..F`" with an approved-dispatch list that contains the `F`
    attestation.
- **Non-blocking, required:** approval entries quote the full commit id, predate their run, and are used once.
- **Everything else is closed and checked:** R7-N1 to R7-N5; V3 digest `81897a90…5107` with `HOLDS`; the precondition
  7 command (exit 0 clean, exit 1 under three mutations); the mock 8/8; `D` correctly left PENDING at `2cd49dc0` or
  later.
- **With R8-B1 and R8-B2 applied, I would ACCEPT, apart from the expected PENDING merge-record id.**

Generated by Claude Code

amaybaum · 2026-11-08T14:36:22Z

Independent review of the MATH-CON-1-S1B-1 round draft r9 (scratchpad; prereg sha256 2c68a096f5bbc44c5f98fe4eb39cac466724ca030b0874431f7af428c69b5741, PLAN sha256 c3fdb4f48f18eb966378342a5c1a2448ef9ea9bbaafd4ea88750b760b6fea506). Verdict: REVISE (narrow; R9-B1 commit sets, R9-B2 pull_requests field). Model review, not human verification.

REVIEW-PLAN-r9.md

# Independent re-review (r9): MATH-CON-1-S1B-1 round draft

## Objects reviewed

| file | sha256 |
| --- | --- |
| `preregistration.draft.md` (r9) | `2c68a096f5bbc44c5f98fe4eb39cac466724ca030b0874431f7af428c69b5741` |
| `PLAN.md` (r9) | `c3fdb4f48f18eb966378342a5c1a2448ef9ea9bbaafd4ea88750b760b6fea506` |
| `preregistration-r8.draft.md` (diff base) | `a8358bc532a70c72d8a782a5fea48d319347f1239fccb9c18df1f51ceb60b2ac` |
| `PLAN-r8.md` (diff base) | `c4c0b7d7996630aa7e1741f16d6919ca3891f176d90951ee50ffb8f6b8988362` |

All hashes match the coordinator's. I am the same independent reviewer as for r1–r8, not the writer. I made no Lean
build, no push and no GitHub write.

## Verdict: **REVISE (narrow). Not ACCEPT yet.**

R8-B1, R8-B2, the approval-entry finding and the note on `D` are applied as I asked. In applying them, r9 introduces
two frozen-rule traps:
- **R9-B1.** The commit sets are undefined.
- **R9-B2.** The `pull_requests` field reports open pull requests at the time of the query, not the pull request that
  triggered the run.

Read as written, either would make P (or precondition 7) fail on a correct round, with no repair possible after `F`.
Each needs a sentence or two of frozen text and two or three self-test cases. With both applied, I would ACCEPT r9
apart from the three expected PENDING fields: the #1206 merge-record id, the `command-scan design pr` line, and `D`.

## Checks run

| check | result |
| --- | --- |
| V3 blocks | byte-identical to r1–r8 |
| verifier probe on r9 | `VERDICT  HOLDS`, digest `81897a90a068b0402e68393f82cffda8fd83f0bda5283316c38d8c58b28e5107` |
| column-0 machine lines | one `branches`, one `design pr` (PENDING), one route (PENDING), one reference set, one dump run (PENDING), and seven `site` lines |
| mock | `MOCK OK`, 8/8; the new lines do not disturb it |

## The findings applied

- **R8-B1: applied.**
  - The `command-scan branches:` line freezes `draft/mathcon1-s1b-1-skeleton` and `draft/mathcon1-s1b-1-dev`. It sits
    in the first control-plane commit and stays byte-identical through `D..F`.
  - The `design pr` line is PENDING, and P refuses it at `F`.
  - P checks the captured branch names, each design-branch run's `head_branch`, the dump run's `head_branch` and PR,
    and the `?head_sha=` queries.
  - The self-tests are present.
  - R9-B1 and R9-B2 below arise from this fix.
- **R8-B2: closed.**
  - Every `workflow_dispatch` in `D..F` must appear in `approved_dispatches_to_f`.
  - Exactly one entry is the `F` attestation, matching `f-run/results.json`.
  - A dispatch of a re-cut candidate, or a retaken `F` dispatch, passes when approved.
  - Self-tests cover zero and two matching entries.
- **The approval-entry finding: closed. The rules match it and apply to both lists.**
  - Each entry quotes the full 40-hex id and the stage, from a closed set of stage names.
  - The run's `head_sha` equals the quoted id, and the approval predates the run.
  - No approval comment is used twice, across both lists.
  - Dispatches at or after `E` are recorded in the receipt's `check-run` attestations under the same rules and are
    reviewed at `Q`. The text correctly says no predicate reads them (`S5`).
- **The note on `D`: applied.** The drift sentence now covers `b73acf38` → `2cd49dc0`, and is extended to `D` when
  `D` is filled in.

## Blocking findings

**R9-B1. The design and dev commit sets are undefined, and literal readings fail.**

r9 says "for every commit of the design branch and of the dev branch, `GET …/actions/runs?head_sha=<sha>` … shows
only `pull_request` runs". Precondition 7 says "no design-branch commit is an ancestor of the candidate `F`". Three
problems follow.

- **Main's history is included.** Read literally, the commits of a branch include everything reachable from its head.
  - For the design branch that includes `D` and `main`'s history. `?head_sha=D` returns `D`'s `push` run on `main`,
    which fails the rule.
  - `D` is also an ancestor of `F`, which fails precondition 7.
  - The dev branch, created from `F`, includes `F` and `D..F`. `?head_sha=F` returns the approved `F` attestation, a
    `workflow_dispatch`, which fails.
- **Approved dispatches are not exempted.** If the final dev commit is pushed to the round branch as S1 itself,
  `?head_sha=S1` returns the approved S1 dispatch, which fails.
- **Possible repair.** A correct implementation would have to choose a definition that the frozen text does not state.

*Fix, frozen before `F`:*
- **Design commits** are `rev-list <design head> ^D`, minus any commit in `D..F`. **Dev commits** are
  `rev-list <dev head> ^F`.
- Record each head and its commit list in the evidence, as provenance (§A.42 item 8).
- The `?head_sha=` rule reads: every run is `pull_request`, or is an entry of `approved_dispatches_to_f` or
  `approved_dispatches`, matched by `run_id`.
- Precondition 7's ancestry bullet uses the same design-commit set.
- Self-tests:
  - `D`'s push run does not trip the rule;
  - `F`'s attestation does not trip the rule;
  - an approved S1 dispatch at a dev commit passes;
  - an unapproved dispatch at a design commit fails.

**R9-B2. `pull_requests` is not evidence of which pull request triggered a run, and it can empty.**

GitHub's API documents the field `pull_requests` on a workflow run as "Pull requests that are open with a `head_sha`
or `head_branch` that matches the workflow run. The returned pull requests do not necessarily indicate pull requests
that triggered the run."

r9 makes "lists the design pull request" a P conjunct for every design-branch run (runs-to-f, read at designation
time) and for the dump run (`order.json`, read at S2). The disposable design PR will normally be closed at some point
before S2. Once it is closed, `pull_requests` comes back empty, and P fails at `E`. Nothing can repair that.

*Fix,* either of:
- **(a), preferred.** Drop the `pull_requests` conjunct. Bind runs to the branch by `event == pull_request` and
  `head_branch == <frozen design name>`. Bind the design PR separately with `GET /repos/{o}/{r}/pulls/<n>`: its
  `head.ref` equals the frozen design name, its `head.repo` is this repository, and its `base.ref` is `main`. Capture
  that answer with its digest. `head_branch` and `head.ref` hold whether the PR is open or closed.
- **(b)** Keep the conjunct, and add a frozen operational rule: the design PR stays open until `order.json` is
  captured at S2 (or at `W`). Also allow several PR numbers to be recorded, in case the PR is reopened as a new one.
  This is weaker, because it relies on a field the API documents as non-causal.

*Self-tests:* the dump run with an empty `pull_requests` passes under (a); a pull request whose `head.ref` is another
branch fails.

## The six owner conditions (PLAN §5)

| condition | status in r9 |
| --- | --- |
| 1. separate throwaway branch, ordinary PR CI | **enforced, durably**, once R9-B1 and R9-B2 are fixed. It rests on the frozen branch names, `head_branch`, the design PR binding and the ancestry check. |
| 2. no execution commits on the round branch before `F` | **enforced**, durably: precondition 7's command, T at S1 and `E`, and `--verify-round` |
| 3. no special dispatch | **enforced, durably**, once R9-B1 and R9-B2 are fixed. It rests on `runs-to-f.json`, `order.json`, the approval entries and the `?head_sha=` queries, with E-onward dispatches in the receipt's attestations, reviewed at `Q`. |
| 4. provenance | **enforced**, durably: the six-field dump-run line, cross-checked by P |
| 5. V3 blocks unchanged | **enforced**, durably: the frozen expectation, re-derived by precondition 7 and T; digest verified unchanged |
| 6. halt before `F` | **enforced** as a pre-`F` gate (precondition 7). Its ancestry bullet needs R9-B1's definition. |

## Summary

- **Verdict:** REVISE, narrowly.
- **Blocking:**
  - R9-B1: define the design commits as `rev-list <design head> ^D` minus `D..F`, and the dev commits as
    `rev-list <dev head> ^F`; exempt approved dispatch runs from the `?head_sha=` rule; apply the same set to
    precondition 7.
  - R9-B2: replace the `pull_requests` conjunct with `head_branch`, plus a pulls-API binding of the design PR.
- **Closed:** R8-B1 (apart from these two traps), R8-B2, the approval entries for both lists, and `D`.
- **V3 digest:** unchanged.
- **Once both are applied, I would ACCEPT r9 apart from the three expected PENDING fields.** Those are the #1206
  merge-record id, the `command-scan design pr` line and `D`, and P refuses each at `F`.

Generated by Claude Code

amaybaum · 2026-11-08T14:36:54Z

Independent review of the MATH-CON-1-S1B-1 round draft r10 (scratchpad; prereg sha256 7f750298e3094f19abdf863170c2175d5de6ac9aa5c4cd51a6dbef027884fd32, PLAN sha256 795035c6ae4d0c19a23efde2467d2d1562b3dce8e5ed2d9eb4f1eb0d3ad8dced). Verdict: ACCEPT (no blocking findings; R10-N1–N3 non-blocking; VOID-at-E question to the owner). Model review, not human verification.

REVIEW-PLAN-r10.md

# Independent re-review (r10): MATH-CON-1-S1B-1 round draft

## Objects reviewed

| file | sha256 |
| --- | --- |
| `preregistration.draft.md` (r10) | `7f750298e3094f19abdf863170c2175d5de6ac9aa5c4cd51a6dbef027884fd32` |
| `PLAN.md` (r10) | `795035c6ae4d0c19a23efde2467d2d1562b3dce8e5ed2d9eb4f1eb0d3ad8dced` |
| `preregistration-r9.draft.md` (diff base) | `2c68a096f5bbc44c5f98fe4eb39cac466724ca030b0874431f7af428c69b5741` |
| `PLAN-r9.md` (diff base) | `c3fdb4f48f18eb966378342a5c1a2448ef9ea9bbaafd4ea88750b760b6fea506` |

All four hashes match the coordinator's. I am the same independent reviewer as for r1–r9, not the writer. I read
#1206 comments 6722716262 and 6722109292 through `gh api`. I made no Lean build, no push and no GitHub write.

## Verdict: **ACCEPT**

There is no blocking finding. The remaining PENDING items are expected fills before `F`. Each is refused by control P
at `F`, or is named as a step before `F`; see the PENDING inventory below, which adds one item to the coordinator's
list. The non-blocking notes R10-N1 to R10-N3 are clarifications to apply before candidate `F`.

## Checks run

| check | result |
| --- | --- |
| V3 blocks | byte-identical to r1–r9 |
| verifier probe on r10 | complete path `VERDICT  HOLDS`, halted path `HOLDS`, digest `81897a90a068b0402e68393f82cffda8fd83f0bda5283316c38d8c58b28e5107` |
| site-line mock | `MOCK OK`, 8/8 |
| citations | checked against the live comments (see 2 below) |

## 1. R9-B1 and R9-B2

**R9-B1: closed.**
- Design commits are defined as `rev-list <design head> ^D` minus `D..F`. Dev commits are `rev-list <dev head> ^F`.
  Each set is recorded with its head as provenance.
- The `?head_sha=` rule admits `pull_request` runs, and approved entries matched by `run_id`.
- `D`'s push run and the `F` attestation now fall outside the sets, or are exempt.
- Self-tests cover `D`'s push run, the `F` attestation, an approved S1 dispatch, and an unapproved dispatch.

**R9-B2: closed.**
- `pull_requests` is no longer used. Runs bind by `event` and `head_branch`.
- The design PR binds through `GET /pulls/<n>` (`head.ref`, `head.repo.full_name`, `base.ref`), which works whether
  the PR is open or closed.
- Self-tests cover a closed PR that binds, an empty `pull_requests`, a fork head, a wrong base and a wrong `head.ref`.

**New holes:** none. Two remarks follow, under R10-N1.

## 2. The two filled citations

**#1206 comment 6722716262**
- Posted by amaybaum at 2026-11-08T14:28:45Z and never edited.
- All five owner sentences quoted under *Authority* appear verbatim in the comment's quote block. I checked each one as
  a substring:
  1. "Yes, you have my authorization …"
  2. "This was explicitly approved …"
  3. "The authorization includes …"
  4. "Preserve the accepted `41a42cb9` … Verify green post-merge `main` CI."
  5. "No additional design edits are authorized."
- The merge facts the preregistration states also match the comment: `2cd49dc0`, its parents `5ce4f98e` and
  `06b5d4f2`, and green post-merge run 42489463543.

**#1206 comment 6722109292**
- Posted by amaybaum at 2026-11-08T13:30:27Z and never edited.
- With whitespace normalized, both quotes match exactly:
  - "I approve the recommended path for all four decisions, with the existing scientific and execution safeguards
    preserved."
  - The table row "Sibling directory | Approved. Use `round-mathcon1-s1b-1/` and record the explicit deviation from
    §10.1."
- The *record directory* paragraph is the recorded deviation that the ruling requires.

As before, both records rest on the quoted owner words, not on the posting account.

## 3. The six owner conditions

| condition | durable enforcement |
| --- | --- |
| 1. separate throwaway branch, ordinary PR CI | the frozen `branches` line; the design PR bound through the pulls API; runs bound by `head_branch` and `event`; the design-commit set with its `?head_sha=` runs; P at S1 and `E`, from `runs-to-f.json` and `order.json`; precondition 7 |
| 2. no execution commits before `F` | precondition 7's exact command (verified in r8: exit 0 clean, exit 1 under mutation); T at S1 and `E`; `--verify-round` (`t1:non-control-plane-change`) |
| 3. no special dispatch | `runs-to-f.json` with `approved_dispatches_to_f`, exactly one entry being the `F` attestation; `order.json` with `approved_dispatches`; the approval-entry rules (full id, stage, prior approval, single use); the `?head_sha=` sets; `E`-onward dispatches in the receipt's attestations, reviewed at `Q` |
| 4. provenance | the six-field dump-run line, cross-checked by P against `lean-toolchain`, `mathlib_rev`, the pin, the file and `order.json` |
| 5. V3 blocks unchanged | the frozen expectation, re-derived by precondition 7 and by T, with mutation self-tests; the digest above is unchanged |
| 6. halt before `F` | precondition 7: no `F` is requested and the finding goes to the owner on the PR |

**All six are enforced, with durable records.**

## 4. The PENDING inventory

Each item is either refused by P at `F`, through "with `--freeze`, nothing is PENDING", or named as a step before `F`:

| item | where | how it is closed |
| --- | --- | --- |
| `D` | *Objects* | P (PENDING) |
| **anchors of the shared-file splices** | *Objects*, "measured at `D` (PENDING)" | P (PENDING). **This item is missing from the coordinator's list.** |
| design PR line | *Branches* | P (PENDING), with its own self-test |
| `open` line | frozen surface; dump script comment | P (PENDING); fixed by the design run |
| route line | *Route line* | P (PENDING) |
| dump-run line | scan list (i) | P (PENDING), or removed under `floor-only` |
| checker blob | exact-layer heading | P (PENDING) |
| XS files and lines | *Source-text control XS* | P (PENDING) |
| precondition-3 pins (`controls.py` blob, skeleton digest, `d-push-run.json`, `command-tokens.json`) | precondition 3 | P (PENDING and pins) |
| drafting note | *Route line* | P (`*Drafting note` rule) |
| status paragraph | header | a step before `F` (PLAN step 6); not checked by P (see R10-N2) |

## Non-blocking notes (apply before candidate `F`)

**R10-N1. Two clarifications.**
- **Precondition 7's ancestry bullet is now vacuous.** It says no design commit is an ancestor of `F`, but the
  design-commit set excludes `D..F` by definition. The real guarantee comes from `check_t1`: a design commit
  introduced into `D..F` changes non-control-plane files, so the check fails. Restate the bullet as "neither the
  design head nor the dump's design commit is an ancestor of `F`", which is a check that can actually fail.
- **The branches must survive until capture.** The design branch and the dev branch must exist until their last
  capture: `runs-to-f.json` at designation, and `order.json` at S2 or `W`. The commit sets are read through git.
  State this as an operational rule.

**R10-N2. Define what a "PENDING field" is.**
- The rule prose contains the word `PENDING` six times, at lines 5, 121, 399, 966, 1176 and 1186. All six are inside
  backticks, and every true field is unbackticked.
- Freeze that convention: a PENDING field is an unbackticked occurrence of the word. Add a self-test confirming that
  the rule prose does not trip P.
- Optionally, let P also refuse the status line "drafting, not a candidate `F`" at `F`.

**R10-N3. Preserve the evidence at a halt.** Owner comment 6722109292 says to "preserve the evidence". At `W`, commit
the derived run result for the failing exact-head run, together with the checker's exit status and summary line.
These are structured and contain no personal data. The raw `RUN` and `JOBS` answers stay uncommitted, as they are now.

## The owner-facing question: a checker VOID at `E`

The owner wrote, in comment 6722109292: "If the checker fails at `E`, halt, preserve the evidence, and request a
separate decision. Do not silently repair or rerun the frozen round."

The draft currently treats checker outcomes in three ways:
- exit 3 (a failed check) halts;
- exit 4 (a countercontrol that did not fail as stated) halts;
- a checker crash or an incomplete run (VOID) is retaken through an owner-approved re-dispatch.

**My view:** this is consistent with the owner's words only in part, and I recommend making every checker VOID
halt-only.

- **A checker crash is deterministic.** The blob is pinned and the inputs are fixed, so a re-dispatch cannot cure it.
  The only cure is a repair, which the owner forbids. A pre-registered retake path for it is either useless or an
  invitation to a "rerun until clean".
- **The owner's wording covers it.** "If the checker fails" plainly includes the checker not completing. The
  instruction is to halt, preserve, and ask, not to rerun.

**Recommended frozen rule:**
- At `E`, any exact-layer outcome other than exit 0 halts the round under `S12`:
  - exit 3;
  - exit 4;
  - a crash;
  - an incomplete summary.
- The evidence is preserved at `W` (R10-N3), and the halt record asks the owner for a separate decision. No rerun
  path for the checker is pre-registered.
- VOIDs that come from the host and not the checker may be retaken only by a separate owner decision, recorded after
  the evidence is preserved. Examples are a cancelled run, missing jobs and runner failure. The draft already
  requires approval (step R); its wording should make clear that this is a decision requested after the fact, not a
  pre-authorized path.

This is a matter for the owner to decide, and it does not block ACCEPT. Applying it changes only the stop rule, the
VOID paragraph and the self-test list, all before `F`.

## Summary

- **Verdict:** ACCEPT.
- **Closed:** R9-B1 and R9-B2. Both citations are verbatim against the live comments.
- **Owner conditions:** all six are enforced with durable records.
- **V3 digest:** unchanged, `81897a90…5107`, with `HOLDS` on the complete and halted paths.
- **PENDING:** every item is refused at `F` or named as a step before `F`. Add the splice anchors to the list.
- **Before candidate `F`:** R10-N1 to R10-N3, plus the owner's ruling on VOID handling, for which I recommend
  halt-only for any checker non-success.

Generated by Claude Code

amaybaum mentioned this pull request Nov 8, 2026

OI-QM-EXT-1: establish conditional equivalence with explicit added conditions, then minimize and source them #1169

Open

amaybaum marked this pull request as ready for review November 8, 2026 14:21

amaybaum merged commit 2cd49dc into main Nov 8, 2026
26 checks passed

amaybaum deleted the research/mathcon1-prereg-20261108 branch November 8, 2026 14:22

amaybaum mentioned this pull request Nov 9, 2026

MATH-CON-1-S1B-1: native V3 round control plane (MATH-CON-1 Stage 1B, first stage) #1215

Draft

Conversation

amaybaum commented Nov 8, 2026

Uh oh!

amaybaum commented Nov 8, 2026

Independent review of the MATH-CON-1 preregistration at e593465b (model reviewer, not human): REVISE

Uh oh!

amaybaum commented Nov 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Independent re-review of the MATH-CON-1 preregistration r2 at e2d44d7c (model reviewer, not human): ACCEPT WITH CHANGES (1 blocking, R1)

Uh oh!

amaybaum commented Nov 8, 2026

Uh oh!

amaybaum commented Nov 8, 2026

Confirmation of the MATH-CON-1 preregistration r3 at 41a42cb9 (model reviewer, not human): ACCEPT

Uh oh!

amaybaum commented Nov 8, 2026

MATH-CON-1 Stage 1B (first stage), §4.5 choices and CONS-0 corrections (owner decision, chat, 2026-11-08)

1. MATH-CON-1 Stage 1B: option (a) approved

2. MATH-CON-1 §4.5: all three choices accepted

3. CONS-0: corrections approved

Overall direction

Uh oh!

amaybaum commented Nov 8, 2026

Independent review of the MATH-CON-1 Stage 1B round plan and draft preregistration (scratchpad, not yet in the repo; model reviewer, not human): REVISE

Uh oh!

amaybaum commented Nov 8, 2026

Independent re-review of the MATH-CON-1 Stage 1B round plan and draft preregistration r2 (scratchpad; model reviewer, not human): ACCEPT WITH CHANGES (1 blocking, R2-B1)

Uh oh!

amaybaum commented Nov 8, 2026

MATH-CON-1-S1B-1, step 0: decisions recorded (owner decision, chat, 2026-11-08)

Planning-status entry (§A.45 rule 3)

Uh oh!

amaybaum commented Nov 8, 2026

Independent review of the MATH-CON-1 Stage 1B round draft r3 (scratchpad; model reviewer, not human): REVISE (R3-B1, R3-B2)

Uh oh!

amaybaum commented Nov 8, 2026

Uh oh!

amaybaum commented Nov 8, 2026

Uh oh!

amaybaum commented Nov 8, 2026

Uh oh!

amaybaum commented Nov 8, 2026

Uh oh!

Uh oh!

amaybaum commented Nov 8, 2026

Merge record: #1206 (MATH-CON-1 design)

Uh oh!

amaybaum commented Nov 8, 2026

Uh oh!

amaybaum commented Nov 8, 2026

Uh oh!

amaybaum commented Nov 8, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Independent review of the MATH-CON-1 preregistration at `e593465b` (model reviewer, not human): REVISE

amaybaum commented Nov 8, 2026 •

edited

Loading

Independent re-review of the MATH-CON-1 preregistration r2 at `e2d44d7c` (model reviewer, not human): ACCEPT WITH CHANGES (1 blocking, R1)

Confirmation of the MATH-CON-1 preregistration r3 at `41a42cb9` (model reviewer, not human): ACCEPT