Repository navigation
M-INACC: does a symmetric state-dependent graph keep Lemma Q(iii)'s protection? (#1169) - #1198
Merged
Merged
Conversation
…FIED) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
Owner
Author
Review provenance: independent review of the M-INACC preregistration at
|
| Reviewed SHA | Verdict | File mtime (UTC, unattested) | sha256 |
|---|---|---|---|
75c0befc |
ACCEPT WITH CHANGES (1 blocking: F1; should-fix F2–F13; nits F14–F20) | 2026-11-08 08:09:55 | 20d776e5e7e39bbb269e77c329e5f07a6cbe19e1b564bdde63946acc549caa8b |
The findings are being applied as an amendment under minacc-1-20261108/amendments/, before any result exists. The same reviewer will confirm the amendment at its exact SHA before derivation starts. G_σ is unchanged.
REVIEW-PREREG-75c0befc.md
# Independent review: M-INACC-1 preregistration at `75c0befc`
- **Object.** `verification/programmes/oi-qm/reconstruction/minacc-1-20261108/DESIGN.md` at the exact head
`75c0befcb324466cb4bf0e90c7ef3cbe429b58ad` (draft PR #1198; parent main `f88c1842`).
- **Reviewer.** Independent Claude Code reviewer. I did not write this work. The review was read-only and on
paper; I made no edits, commits, pushes or GitHub posts. I ran no simulation or search. The only
computations were hand checks of the file's own algebra.
- **Scope.** The question is whether the preregistration is fit for derivation. Nothing has been derived
at this checkpoint, and nothing should have been.
## Verdict: ACCEPT WITH CHANGES
The construction is correctly defined. Its stated properties hold, and I checked each one by hand. Its
motivation comes from SM's own ring and form lemma, and the one place where the target enters (the
requirement of symmetry) is disclosed. The operational classes, the controls and the ledger are close to
what the owner's authorization requires.
One defect is blocking. Clause (a) of M-INACC would be decided by USE-dyn, and USE-dyn holds for every
nonzero functional (F1). Under the rule as written, outcome (A) would report clause (a) as met on a
vacuous test.
Several should-fix items concern places where the verdict could be steered after the fact or where
results could be mislabelled:
- class definitions that contradict each other (F5);
- an unattributed gate control in `Π_A` (F6);
- the combination and attribution rule (F3);
- a requirement in CC-OFF that could void a valid proof (F7);
- the rule for amending a frozen file (F8).
**Condition.** Apply F1 and the should-fix items in one amendment under `amendments/`. Commit it before any
`RESULT.md` content exists, and have the reviewer confirm it at its exact SHA before checkpoint 2 begins.
None of the fixes changes `G_σ`.
## Findings
Line numbers refer to `DESIGN.md` at `75c0befc`.
### Blocking
**F1. USE-dyn is vacuous, so clause (a) would be decided by a test that always passes (L446–456,
L462–464).**
USE-dyn asks for a configuration `λ`, a shift `w` with `f(w) = 1`, and a continuation protocol whose record
differs at `λ` and `λ + w`. By §3.3 (L355), the observer may register one slot of any active cell. So for
any nonzero `f`:
- take a slot `s` on which `f` has coefficient 1, and set `w = e_s`, so that `f(w) = 1`;
- the continuation "register `s` now" records `λ_s` in one case and `λ_s + 1` in the other.
USE-dyn therefore holds for every nonzero `f` in both classes. It excludes only `f = 0`, not "a dynamically
inert `f`" as L449–451 says.
The file itself shows (L453–456) that, under PROT-B, the statistical reading of "use" is excluded by Bayes.
So the only informative form is USE-ctx. USE-ctx has no fixed definition of "realization" and no pass
criterion.
As written, an (A) verdict would report clause (a) as met. That is the favourable label, resting on a
vacuous test (§A.29; Code Review Rules, "Exactness and controls").
**Fix.**
- Decide clause (a) by USE-ctx alone.
- Define USE-ctx before any derivation:
- the operations compared;
- the ontic maps that realize them;
- indistinguishability over all protocols of `Π`;
- the pass criterion.
- Record USE-dyn as vacuous and report it only for context.
- If USE-ctx is not decided, report the outcome as (A′), with clause (a) "not decided".
- State now, as a definitional observation, that clauses (a) and (b) of M2D's M-INACC are incompatible under
the statistical reading.
### Should-fix
**F2. The (A) label is weaker than M2D's criterion for deriving M-INACC (L442–464, L111–115).**
M2D L862–864 adds a requirement to its derivation criterion: such a graph "would also have to keep FB's
reflections out by a sourced structure". This unit declares FB out of scope (L117–118).
M2D's statement of M-INACC is also per encoded system (M2D L834). M2D's second rule-out route, "every
functional the dynamics uses becomes determinable through reuse or recombination", has no outcome slot in
§4.2.
**Fix.**
- State in §4.2 that (A) does not establish M-INACC in M2D's sense: the FB clause is outside scope and
stays open.
- Add a reported line for the second rule-out route. Once F1 is fixed, this can be the USE-ctx analysis.
**F3. The combination and attribution rule (L486–491).**
- (i) The admissible pairs are listed on {A, B, C} and leave out (A′). (A) and (A′) for `Π_B` do not carry
over to `Π_A`: clause (a) quantifies over continuation protocols of the class, so (a) can hold in `Π_B`
and fail in `Π_A`.
**Fix:** state the pairs on the protection outcome {A∪A′, B, C} and evaluate the clauses for each class
separately.
- (ii) The rule that "an exposure found in `Π_B` and not in `Π_A` is attributed to the resources `Π_B`
adds" holds only when `Π_A`'s outcome is (A).
- Under the pair (B, C) the attribution is undecided.
- Even under (B, A), CC-OFF shows that `Π_B`'s resources do not expose with linear steps (QA). The
exposure is then a property of the combination of gate and resource, not of P3 or the other devices
alone.
**Fix:** attribute to `Π_B`'s resources only under (B, A). D-ATTR names the minimal subset of resources
used, together with the gate. Under (B, C), state that the attribution is undecided.
**F4. Partial outcomes and the (C) rule (L480–484, L507–518).**
- (i) Node 1 lists QA's proof steps (s1)–(s4). These cover PROT-D only. PROT-B in the linear class rests on
a fifth step: the conditional law is uniform on an affine subspace (AP1 L560). Without that step, the
first missing premise for PROT-B cannot be named.
**Fix:** add (s5) to the audit.
- (ii) The case "PROT-D proved, PROT-B open" falls into (C) and has no separate label.
**Fix:** add sub-outcomes for (C), (C-D) and (C-B), and require that any partial result proved be reported
with its hypotheses.
- (iii) For `G_σ`, step (s1) fails by inspection: each branch is a fixed nonlinear map, not a sequence of
symplectic linear steps. If (C) names "the first step that does not transfer", it will always name (s1),
which says nothing.
**Fix:** define the "first missing premise" as a named statement `P` such that `P`, together with the
listed hypotheses, yields PROT in the record, and `P` is not implied by the class. Keep this distinct from
the first step that fails to transfer. `P` is reported, not adopted, with CC-RECON applied.
**F5. The rules on observer access and class membership contradict one another (L130–131, L307, L338–347,
L355, L400–404).**
- §1.2 makes hidden cells active. §3.3 allows registering "one slot of any active cell". §3.6 denies "access
to source cells … to the hidden sector".
- §3.1 allows source cells in `R`, and §3.6 then forbids access to them.
- Translations apply to "any slot" (L346), which includes hidden cells.
- E-iso zeroes only edges that join `R` to its complement. For an `R` that is not an interval, an internal
gated edge `{i, i+2}` with `i + 1 ∉ R` is still gated by a hidden cell. The file does not say whether E-iso
blocks that gate read, and that read is route R-G.
- QA's P1 is registration of a meter's record slot (QA L139–140; AP1 L292–295). The file widens this to any
slot of any cell without stating the identification. The identification is valid in `Π_A`, where every
ring cell is written by coupling at every tick.
Each of these changes which protocols the class contains. Settling them after the derivation would be
narrowing, or tuning, under (a3) and C-IMPORT (iii).
**Fix.**
- Restrict registration and translation to cells in `R`, and to refills of sites in `R`.
- State that a hidden cell has the same law as a source cell placed in `R` (H-PS), so that enlarging `R`
loses nothing.
- Reword §3.6 as "no access other than P1 registration".
- State the gate semantics of E-iso: gates outside `R` remain live, or `R` is required to be gate-closed.
- State that the meter is identified with a ring cell.
**F6. In `Π_A`, archiving with refill is an unattributed gate control (L319–327, L357–362, L496–498).**
Registering any slot of a cell `g` archives it, and the refill's known `u` slot (0, or 1 through H-PREP)
then sets the gate of `{g−1, g+1}` deterministically. So `Π_A` is "no arming, no isolation" (L327) only in
name: the swap is a supplied write to a gate.
AP1 also enforces terminality through P3 and E-iso ("the registered cell's edges are never armed", AP1
L338–342). `Π_A` instead supplies a cell swap. The §3.7 ledger lists registration and refill separately but
does not record that together they act as gate control. D-ATTR omits them.
**Fix.**
- Add "archive-swap or refill (gate setting)" to D-ATTR and to the §3.7 ledger.
- State that `Π_A`'s P1 is implemented by a supplied swap, where AP1 uses P3 and E-iso.
**F7. Problems with CC-OFF (L565–566, L282–287).**
- (i) "Any proof of (A) specializes to Lemma Q(iii) for `N_1`" would void a valid proof whose key step is
specific to `G_σ`.
**Fix:** require consistency instead. Where the proof's hypotheses hold in `N_1` or `N_0`, its conclusion
must agree with QA. Where they do not, state which hypothesis fails.
- (ii) The baseline "Holds (QA)" for `N_1` and `N_0` is applied to classes that QA's N does not contain:
- archive-swap refills;
- vacancies;
- direct registration of slots;
- no heralds (harmless, because each herald branch is a protocol with fixed settings).
For `N_1`, "every gate held at 1" conflicts with V-0, which makes a vacancy gate as 0. The rule for a
vacancy in that limit is not stated.
**Fix:** make C-LIN verify Lemma Q(iii) for `N_1` and `N_0` under these conventions. AP1 Lemma 3 extends
in one line, because fresh cells have disjoint support. Also state the vacancy rule in each linear limit.
**F8. The freeze cannot absorb this review as written (L34–37, L250–253, L573, L615).**
(a2), (a3) and C-IMPORT (iii) treat any restriction added "after checkpoint 1" as ad hoc and as voiding
every verdict. Fixing F5 and F6 clarifies the classes, and the fix for F5 narrows them in wording. Read
literally, the review's own changes would then void the result.
**Fix.**
- Define the preregistration as checkpoint 1 together with the amendments that precede any derivation, are
reviewed and are committed before `RESULT.md` first appears.
- Anchor (a2), (a3) and C-IMPORT (iii) to the first commit that adds `RESULT.md`.
- Add an §A.41 checkpoint: each amendment's commit is an ancestor of the first `RESULT.md` commit, or the
amendment is marked as written after a result and as not affecting the decision.
With that change, the freeze-and-amend scheme works.
**F9. The disclosure about R-G is too thin (L533–535).**
The file says that informal scoping "identified R-G as the route to examine first". The coordinator's
account is that the scoping flagged R-G as a possible exposure. The disclosure should state:
- the direction of the expectation;
- whether any example was worked by hand;
- whether any class convention was fixed with that example in view. The conventions at issue are V-0,
refill in `Π_A`, direct registration, and E-iso without gate blocking.
The decision rule itself is symmetric between outcomes, and its routes run in a fixed order. (B) requires
an explicit protocol checkable by hand, together with CC-OFF and D-ATTR. Once F5, F6 and F8 are fixed, I
see no bias that this expectation introduces.
**F10. A natural alternative is missing, and the reading of the ring is unstated (L264–272, L167).**
The `F_2` symmetrization `A + Aᵀ` of SM's directed ring is not listed. It gives:
- edge `{i, i+1}` the weight `1 + u_{i+1}`, gated by its own endpoint, so that `f_{i+1}` reads `u_{i+1}` and
SM constraint (ii) is violated;
- edge `{i, i+2}` the weight `1 + u_{i+1}`.
It is rejected for the same reason as the intersection reading.
**Fix.**
- Add `A + Aᵀ` to the table of alternatives.
- State that `E(u)` is the support, or union, reading.
- Say why `L ≥ 5` is required where SM allows `L ≥ 4`: at `L = 4`, `{i, i+2} = {i+2, i+4}` carries two
gates.
**F11. PROT-B depends on the measure (L150–155, L433–436).**
Lemma Q(iii) is a statement about support and holds for any full-support prior (QA L496–498). PROT-B, and
uniformity in the linear limits, are statements under the uniform product law.
**Fix:** state that PROT-B and any (A) verdict carry N2, H-PS and H-INF-μ, and that independence from the
measure is not claimed.
**F12. Provenance of the owner's authorization (L6–7).**
The quote is verbatim with #1169 comment 6718997520 (amaybaum, 2026-11-08T07:57:54Z, "Owner decisions
(chat, 2026-11-08)"). That comment was posted after the commit, at 07:56:43Z.
**Fix:** in the amendment or in `RESULT.md`, link that comment with its author and time (§A.42 item 7).
**F13. Self-checks under §A.41 (L555–559, L616).**
"No simulation, search or enumeration campaign" has no checkpoint, and the self-checks "are not committed".
For comparison, M2D's c3 enumerated all 1024 configurations.
**Fix.**
- Bound the self-checks: each re-evaluates only an instance stated in the record and enumerates no space of
configurations or protocols.
- Require `RESULT.md` to list each check's instance and size, so that the reviewer can confirm the bound.
### Nits
**F14.** Main's cone theorem is at **L364**, not L366. L366 is the paragraph on its scope (setting
screening). Correct L576 and L647.
**F15.** C-NS and SC-1–SC-3 have no consequence if they fail.
- C-NS follows from Main's cone theorem. A violation would therefore show an error in the analysis, and
should void the verdicts on composition.
- A positive finding under SC-1 should count as a failure of C-IMPORT.
**F16.** Two problems with the P1 and P2 controls:
- C-P1's "both slots of a cell are registered" exposes an *active* functional only through a partner cell
(AP1 C9) or if the cell stays on the ring. Name the active `Q* = 1` functional that is exposed.
- C-P1 and C-P2 are checks of the definitions. An (A) proof should also cite the line where it uses P1 and
the line where it uses P2.
**F17.** Add a countercontrol to C-LIN: the node 1 audit applied to `G_SM` must fail, at Lemma Qσ(b) and
at (s3).
**F18.** D-Q (L500–501) says R1 enters USE-ctx, but USE-ctx (L451–453) is defined on the full accessible
theory. Make the two agree.
**F19.** (m3) (L230–234) motivates reciprocity of the edges at fixed `u`. The dependence on the gate is
one-way by construction (L520–522), so state that (m3) does not cover it.
**F20.** Smaller points:
- Exclude heralds with a one-line reduction (L378), since QA's N admits them.
- "Ring `Z_L`" (L167) and "an infinite ring" (L307): fix one of them, with H-NW.
- §9 omits #1147 (L411) and the pointer to condition (iv) of #1169 (L583).
- Cite M1D SC-2 at L900.
- For B-B, §4.4 should require the conditional *law*, not only the support (L549–551).
### Confirmation of the reported defect at SM:112
The defect is confirmed. SM:112 reads "graph regularity (undirected degree bounded in [3, 2] independently
of the state) hold for any L and q". `[3, 2]` is not an interval. The degrees under each reading of SM's
directed ring are:
| Reading | `L = 4` | `L ≥ 5` |
| --- | --- | --- |
| Support (undirected) graph | 2 or 3, since `{i, i+2}` is present iff `x_{i+1} = 0` or `x_{i−1} = 0` | 2, 3 or 4, all attained |
| Out-degree | Exactly 2 | Exactly 2 |
| In-degree | 1 to 3 | 1 to 3 |
No reading gives `[3, 2]`. The likely intended statement is "bounded in [2, 4]". The bound does not depend on
the state; the degree does.
Routing the defect through the coordinator, with no manuscript edit in this unit, is correct. Under §A.45
rule 6 it needs an accountable Issue.
## What I checked
1. **The diff.** `git diff --stat f88c1842 75c0befc` shows one file, 655 lines added. The worktree is clean at
HEAD.
2. **The construction `G_σ`, by hand.**
- `f_i` from `E(u)`: the neighbours of `i` are `i ± 1` always, `i + 2` iff `u_{i+1} = 0`, and `i − 2` iff
`u_{i−1} = 0`. Over `F_2` this gives `f_i = u_{i−1} + u_{i+1} + (1 + u_{i+1}) u_{i+2} + (1 + u_{i−1})
u_{i−2}`, which matches the file.
- **Inverse.** `(a, b) = (f(u) + v, u)` gives `u = b` and `v = a + f(b)`. Correct.
- **Symmetry.** The gate of `{i, i+2}` is `i + 1` from either end. Correct.
- **Center-free.** `f_i` never reads `u_i`. Correct.
- **Degree.** The degree is `2 + [u_{i+1} = 0] + [u_{i−1} = 0]`. Correct.
- **Reflection invariance.** Correct.
- **Conservation of `Q`.** `Σ_i u_i f_i(u) = 2 Σ_{e ∈ E(u)} u_i u_j = 0`, so `Q` is conserved. This agrees
with Lemma Qσ(a), which I read at M2D L595–609.
- **Linear limits.** `N_1` and `N_0` are correct.
- **Intersection reading.** It is correct, including the claim that no gated edge survives for
`L ≥ 5`.
- **Union reading.** It equals `E(u)`.
- **Breaking controls.** The center-term control breaks `Q` through `Σ u_i^2 = Σ u_i`.
3. **The sources against the file's paraphrases.** I checked:
- SM L104–112, L224 and L226, the latter for its scope, which (m2) relies on through SM L110's "at each
step";
- Substratum L98 and L100;
- QA §1.2, C-LEAK, Lemma Q and its proof (L458–520), and the P1 and P2 ledger (L779–780);
- AP1 SA-1 (L282–299), the terminality enforcement (L338–342), §4.1 including "symplectic iff
`A = Aᵀ`" (L481–484), Lemma 3 with its affine uniformity (L533–562), §4.5 and C9;
- M2D L110–120, Lemma Qσ and P★ (L593–660), and M-INACC (L832–870);
- M1D L900 (SC-2: feedback executed by an outside agent);
- PR-QA §1, including the entire joint record at L36 and the exclusion of correlated backgrounds.
4. **Links.** All 33 blob links pin `f88c184220453badfc9279ab9a86b6785e4db5ff`. I resolved every `#L`
anchor at that commit, and each says what the file claims except Main:366 (F14).
5. **Lean.**
- `substratumGen_not_control` is at `StructuralClosure.lean:348`. It is used only as context, which is
correct: the monomial ceiling applies to the physical carrier.
- No identifier `readWriteSourced_` appears. The only mentions are the family name `ReadWriteSourced`
in an exclusion note and in the invariant row. #1188 confirms the defect.
6. **Owner records.**
- #1169 c.6718997520 matches the quote verbatim.
- c.6714136234, the addendum, is quoted correctly in substance.
- #1193 is the sign issue at odd `q`. The claim that at `q = 2` "nothing depends on #1193" is correct,
since `+v = −v` there.
7. **Register (§A.32, §A.33).** I scanned for capitals of four or more letters outside labels, for phrases
of revision history and for reader instructions. There are no hits. The capitals found are labels, and
the §A.31 category names at L543.
8. **§A.41.** I matched each invariant asserted in the file to its checkpoint row. The checkpoints that are
missing or weak are covered by F8 and F13.
9. **§A.42 item 8.**
- The manuscripts, the records on main, and the Lean statement count as support on main.
- Q-A and AP1 support Lemma Q(iii), Lemma 3 and SA-1. QA and AP1 were reviewed on #1184/#1189 and #1183
respectively, and those PR numbers are provenance.
- PR-QA and FB are used only for discipline and context, which is correct given their status "review
pending".
- The owner chat, #1169 c.6714136234, #1188, #1193 and #1147 are provenance.
- I found no support off main.
- Under §A.46 item 7, the premises used (Lemma Qσ(a), Lemma Q(iii), Lemma 3) rest on reviewed records on
main. I re-checked Lemma Qσ(a) by hand.
10. **Exhaustiveness of the outcomes.** (A), (B) and (C) are exhaustive and mutually exclusive, given a
correct proof or a correct exhibit. (B-D) is contained in (B-B). The defects are at the level of labels,
not of the logic: F1 (the favourable label regardless of result), F3 and F4.Generated by Claude Code
…eview (WIP / UNVERIFIED) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
…WIP / UNVERIFIED) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
Owner
Author
Review provenance: confirmation of amendment A1 at
|
| Reviewed SHA | Verdict | File mtime (UTC, unattested) | sha256 |
|---|---|---|---|
bcf2aba4 |
ACCEPT WITH CHANGES (G1 blocking; G2–G8), applied by amendment A2 | 2026-11-08 08:24:19 | 6b5c55ae2f4042d9ff8f686f1870a83c256ce7a3cb7ce38509412f0ee75051e5 |
The changes G1–G8 are applied by amendment A2 at 90e950e5, before any result exists. G_σ is unchanged.
CONF-A1-bcf2aba4.md
## Confirmation of A1 at bcf2aba4
- **Object.** `bcf2aba49d5f991b404c24dedbce6910470fda27`, a single-parent commit on `75c0befc`. It adds only
`minacc-1-20261108/amendments/A1-prereg-review.md` (447 lines).
- **Method.** The review was read-only. I fetched nothing, made no edits and ran no computation. Line
numbers below refer to A1.
### Verdict: ACCEPT WITH CHANGES
A1 resolves F1, F2, F3, F5, F6, F7, F10–F15 and F17–F20. F4, F8 and F16 are resolved only in part
(G4, G5, G7).
A1 also adds a new rule that has to change before derivation, and one finding is blocking. A1.1 introduces
the retrodictive property PROT-R and leaves it out of the decision (G1).
**Condition.** Apply G1–G7 in a second amendment, A2. Commit it before any `RESULT.md` content exists, and
have the reviewer confirm it at its exact SHA.
### Item 4: nothing else changed
| Check | Result |
| --- | --- |
| `DESIGN.md` byte-identical | Confirmed: `git diff --quiet 75c0befc bcf2aba4 -- …/DESIGN.md` succeeds |
| `G_σ` unchanged | Confirmed. A1.10 adds a reading and an alternative only. A1.8 moves the anchor of the sentence that fixes `G_σ` but does not change the sentence |
| No result or verdict content | Confirmed. The incompatibility statement in A1.1 is definitional and labelled as such. The example in A1.9 is described as unchecked and not a result |
| Links | All 8 blob links are pinned to `f88c1842` |
| Lean | No `readWriteSourced_` identifier appears |
| Register | The register scan is clean |
### Item 1: status of F1–F20
**F1, resolved.** USE-ctx now has an operation set, a realization (a stochastic kernel that averages over
the protocol's own fresh unknowns), indistinguishability over all `P` and `C` in `Π`, an action
`a_T(λ)`, and pass, fail and undecided criteria. Undecided maps to (A′).
- **Not vacuous.** I found no generic construction that passes. Indistinguishability quantifies over every
preparation, including preparations with known cells, so a pair that differs generically is told apart.
Averaging `a_T` over `T`'s own randomness blocks the trivial pointwise difference.
- **Can it fail?** Yes. The fail branch is well defined. In practice it is a universal statement, so the
likely outcomes are pass or undecided, which gives (A′). That is acceptable.
- **Nit.** Require `T` and `T′` to have the same tick count, or state how timing enters `K`. This closes a
possible freedom over timing (G8).
**F2, resolved** (A1.2, line RO-2).
**F3, resolved.**
- The pairs on {A∪A′, B, C} are correct.
- Attribution under (B, A∪A′) goes to the gate together with the minimal resource subset.
- (B, C) is undecided, and D-ATTR includes archive-swap.
- **Nit:** state that monotonicity also holds for the sub-labels. If `Π_B` is (C-B), then `Π_A` is
A∪A′ or (C-B) (G8).
**F4, partly resolved.** Step (s5) and the split into (C-D) and (C-B) are correct. The definition of `P`
leaves freedom (G4).
**F5, resolved**, with one gap in the rule on registrability (G2, G3).
**F6, resolved.** Nit: A1.6 cites AP1:292 for the enforcement of terminality. The sentence is at **AP1:338**
(§3.2 item 2).
**F7, resolved.** The consistency rule, the vacancy override in the linear limits, and C-LIN under this
unit's conventions are all correct.
**F8, partly resolved.**
- The anchor to the first `RESULT.md` commit is correct, and so is the ancestry checkpoint.
- Two gaps remain:
- "reviewed" has no time anchor;
- the escape for a post-result amendment covers only amendments that do not affect the decision (G5).
**F9, disclosed.** See item 2 below.
**F10–F15, resolved.**
- A1.10 states the `A + Aᵀ` row, the union reading and the reason for `L ≥ 5` correctly.
- PROT-D is measure-free; PROT-B is stated under N2 and H-PS.
- The link to c.6718997520 is verbatim.
- The self-check bound is at most 16 bits per instance and listed.
- Main:364 is correct.
- A C-NS violation voids composition verdicts, and SC-1 counts as a C-IMPORT failure.
**F16, partly resolved** (G7).
**F17–F20, resolved.**
- The `#1169` comment 6713653816 cited for condition (iv) does define (iv) ("full reversible control"), and
cites `substratumGen_not_control`.
- M1D:900 is correct.
- The reduction for heralds is correct, because each herald branch is a protocol with fixed settings.
### Findings on A1
**G1 (blocking). PROT-R is excluded from the decision (A1.1 L71–76).**
PROT-D and PROT-B quantify over *linear* `Q* = 1` functionals on active cells at the tick where `K` is
evaluated. Under nonlinear transport, the value `f(t)` is at a later tick a *nonlinear* function of the
current configuration and the archived cells. PROT-D and PROT-B at later ticks therefore do not cover it.
A protocol whose later records determine or bias `f(t)` exposes exactly the information the owner asked to
be tested ("test whether an allowed protocol can expose…"). It also violates M-INACC (b) ("no … read, reuse
or recombination determines it"). Yet under A1 such a protocol would leave (A) and Positive intact.
In the linear limits PROT-R follows from QA's content. Transport preserves `Q*`, and the determined set
`span(I_t) + R` has `Q* ≡ 0` on terminal and active cells together. So the exclusion is not inherited from
Lemma Q(iii).
A1's own Bayes argument shows that the clash is between PROT-R and the *statistical* reading of clause (a).
Since clause (a) is now decided by USE-ctx, nothing prevents including PROT-R.
**Fix.**
- Make PROT-R part of PROT, and so of (A) and of clause (b).
- Add an exposure type **(B-R)**: retrodictive determination or bias of `f(t)` from later records, with
CC-OFF.
- Add PROT-R to the partial outcomes, as (C-R).
- Have C-LIN verify PROT-R in `N_1` and `N_0`.
- Update the tier table accordingly.
**G2 (should-fix). The multiplier convention for `Π_B` (A1.9 L274–279) and the new registrability rule
(A1.5 L189–194).**
*The multiplier convention.* Its per-edge granularity is QA's P3 as written: "loaded per tick and per edge"
(QA:131) and "arming of the individual couplings" (QA:838). Retaining the gate is what keeps `G_σ` present
under arming.
The alternative of applying AP1 SA-1(a′) literally is not neutral. That reading lets the loaded `k` replace
the native coefficient, and it would:
- remove the gate on every armed gated edge;
- turn those couplings into ungated next-nearest couplings, which is QA's separate conditional extension
NNB (QA:805), not P3;
- reduce armed `Π_B` to a linear class that Lemma Q(iii) already protects. That biases toward protection,
and stops `Π_B` from being a test of `G_σ`;
- break `Π_A ⊂ Π_B`, because the native gated coefficient `1 + u_{i+1}` cannot be loaded classically.
My judgement is that the convention is not biased toward exposure in any way that can be avoided, and it
should **not** be replaced by "QA's P3 verbatim". The order disclosed (the convention was written after the
example) still requires an independent justification in the record before derivation.
**Fix (A2).**
- Justify the convention from QA:131, QA:242 and QA:838. P3 loads coefficients on individual couplings. It
cannot alter the rule's state dependence, in the same way that it cannot add a `k_ii` term.
- List the two alternatives with their reasons for rejection: replacement, and gated edges that cannot be
armed.
- Require every (B) record for `Π_B` to state whether the exposing protocol arms a gated edge while its
nearest-neighbour edges are disarmed. The role of the convention is then visible.
*The registrability rule.* A1.5's rule is also new in A1, and so also written after the example. It
decides directly whether R-G's registrations are allowed:
- a pure gate cell with no armed edge cannot be registered;
- a cell whose only armed edge is gated by an unknown gate can be registered.
A K-decidable alternative exists: require an edge whose effective coefficient is determined by `K`. That
alternative is closer to AP1's "the slot written by its coupling", read alongside AP1's discussion of
unheralded defects at L617–622.
**Fix (A2).**
- Disclose that the rule was written after the example.
- Justify the choice of multipliers over effective coefficients by K-decidability.
- State the alternative and the reason it is rejected.
**G3 (should-fix). Transported record slots (A1.5 L191–193).**
"Written at a tick in which the cell had at least one edge with multiplier 1" reads as if a record slot,
once the cell is isolated and takes free ticks, stops being registrable. AP1 SA-1(b) allows "the slot
written by its coupling, transported by the cell's free evolution".
**Fix:** state that a record slot written by coupling stays registrable after free ticks.
**G4 (should-fix). The first missing premise `P` (A1.4 L167–177).**
Two freedoms remain:
- `P = PROT-D`, or any statement about determination or bias of `Q* = 1` functionals, satisfies the
definition trivially. CC-RECON only flags such a `P`; it does not exclude it.
- "First" is not defined, and several `P` may qualify.
**Fix.**
- Require `P` to be a statement about `G_σ`, the protocol class or the supplies that does not mention
determination or bias of `Q*`-class functionals.
- Order candidates by the earliest step among (s1)–(s5) that `P` repairs.
- Report every candidate found, not a selected one.
**G5 (should-fix). The amendment anchor (A1.8 L241–251).**
- "Reviewed" should mean that the reviewer's confirmation at the amendment's exact SHA is recorded on #1198
before the first `RESULT.md` commit is pushed. Otherwise the order cannot be checked.
- An amendment written after a result that *affects* the decision is not covered.
**Fix:** state that such an amendment voids the verdicts it affects.
**G6 (should-fix). The tier mapping (A1.21, L399–431).**
- (i) **Positive.** The row requires "every control … green, CC-NC included". It does not state outright
that Positive *requires* a certified witness: a contextuality witness certified over tomographically
complete equivalences, with the blocked spanning reads shown. CC-NC can also end "not decided by
Theorem NC".
**Fix:** "Positive requires that a certified witness is exhibited. Otherwise Partial."
- (ii) **(C-B).** Mapping (C-B) to Partial gives favourable framing to an open bias question. (C-B) is not
"succeeds mathematically".
**Fix:** map (C-B) to Undecided, with PROT-D reported as proved.
- (iii) **Negative.** "Or protection otherwise shown to fail" is a category the decision rule does not
contain, and so a freedom.
**Fix:** delete it, or enumerate it (for example (B-R) once G1 is applied).
- (iv) **No headline tier.** State that no combined tier is reported. In particular, the more favourable
class is never promoted to a headline. `Π_A` is the natural class.
- (v) **Provenance.** The owner's tier instruction is quoted with an ellipsis and has no author, time or
record. I found no record of it on #1169 or #1198.
**Fix:** record it on #1169, and quote it in full with author and time (§A.42 item 7). The elided text
may bear on the mapping.
The mapping otherwise leaves the decision rule unchanged.
**G7 (should-fix). C-P1 variant (i) (A1.16 L346–349).**
"Registering its two slots at consecutive ticks" does not expose anything, because `v(t+1) = u(t)`
repeats the value already recorded. QA's two-slice receiver registers `u` and `v` at the same moment
between ticks.
**Fix:** require both slots at one moment between ticks. As written, the control would fail through its
own definition and void an (A) verdict for no reason.
**G8 (nit).**
- USE-ctx needs equal duration for `T` and `T′`.
- Monotonicity should be stated for the sub-labels.
- A1.6 should link AP1:338.
### Item 2: the F9 disclosure and the multiplier convention
The disclosure is now adequate. It states:
- the direction of the expectation, toward (B-D) in `Π_B` through R-G;
- the example, worked mentally and unchecked;
- that the multiplier convention was written after the example;
- the reason for each other convention.
On the question the coordinator raised, see G2:
- The convention is the per-edge transfer of QA's P3. It is not chosen for exposure.
- The one alternative that would erase the gate biases toward protection, and breaks `Π_A ⊂ Π_B`.
- So replacement by "P3 verbatim" is neither required nor well defined.
- An independent justification, with both alternatives and the reporting requirement, must be written before
derivation.
- The registrability rule in A1.5 is also written after the example and bears directly on R-G. It needs the
same treatment.
Because the attribution in D-ATTR and A1.3 assigns any exposure seen only in `Π_B` to the gate together
with P3, and `Π_A` does not depend on this convention, any residual bias is confined to the verdict for
`Π_B`.
### Item 3: the tier mapping
Once G6 is applied, the mapping is consistent with the decision rule and adds no freedom, and Positive
requires a certified CC-NC witness. As written, three freedoms remain:
- the requirement on the witness is not explicit;
- (C-B) is mapped to Partial;
- the "otherwise shown to fail" category in Negative.
***Generated by Claude Code
Owner
Author
Review provenance: confirmation of amendment A2 at
|
| Reviewed SHA | Verdict | File mtime (UTC, unattested) | sha256 |
|---|---|---|---|
90e950e5 |
ACCEPT FOR DERIVATION (non-blocking nits H1–H3, to be handled in RESULT.md) | 2026-11-08 08:24:19 | f7d57cf505fcecf01fb0ccbf250c425c7bba57c4a67e36a4c4a2d243f972e3a9 |
Under A2.5, this confirmation is recorded before the first RESULT.md commit is pushed; the preregistration is DESIGN.md at 75c0befc with A1 at bcf2aba4 and A2 at 90e950e5. G_σ is unchanged.
CONF-A2-90e950e5.md
## Confirmation of A2 at 90e950e5
- **Object.** `90e950e51a452f0aaacb274b4e00657184181bea`, a single-parent commit on `bcf2aba4`. It adds only
`amendments/A2-a1-confirmation.md` (274 lines). #1198's head is this SHA.
- **Method.** The review was read-only. I fetched nothing and made no edits. I read the GitHub records
through the API only.
### Verdict: ACCEPT FOR DERIVATION
The preregistration, made up of `DESIGN.md` at `75c0befc`, A1 at `bcf2aba4` and A2 at `90e950e5`, is fit for
derivation. G1–G8 are resolved. Nothing in the three documents remains blocking or should-fix.
**Procedural precondition (A2.5).** On #1198 so far, only the review of `75c0befc` is recorded
(c.6719123056, 08:12:02Z). Before the first `RESULT.md` commit is pushed, the coordinator must record two
confirmations on #1198, so that A1 and A2 count as reviewed under A2.5:
- the A1 confirmation, at `bcf2aba4`: accept with changes, with the changes applied by A2;
- this A2 confirmation.
The three nits below (H1–H3) need no amendment. They can be carried in `RESULT.md` or handled in
coordination.
### Item 2: nothing else changed
| Check | Result |
| --- | --- |
| `DESIGN.md` byte-identical to `75c0befc` | Confirmed |
| A1 byte-identical to `bcf2aba4` | Confirmed |
| Unit directory at `90e950e5` | Contains `DESIGN.md`, A1 and A2 only. There is no `RESULT.md` |
| `G_σ` unchanged | Confirmed. A2 touches only classes, rules, controls and reporting |
| Result or verdict content | None. The disclosures of A2.2 describe the order of writing, not outcomes |
| Links | All 8 blob links are pinned to `f88c1842`. QA:129–131, 242, 805 and 838, AP1:292, 338 and 617, and QA:512 say what A2 cites them for |
| Lean | No `readWriteSourced_` identifier appears |
| Register | Clean |
### Item 1: G1–G8
**G1, resolved** (A2.1).
- PROT-R is defined for every tick `t`, every `Q* = 1` functional `f` on the cells active at `t`, and every
later `t′ ≥ t`, given `K` at `t′`, which includes the archived cells.
- PROT is PROT-D ∧ PROT-B ∧ PROT-R.
- (A) requires PROT, and clause (b) is evaluated as PROT.
- (B-R) is defined with the exact conditional law, CC-OFF in both linear limits, and D-ATTR.
- The partial outcomes form the chain (C-D) → (C-B) → (C-R). The chain is exhaustive, because PROT-R at
`t′ = t` is PROT-D ∧ PROT-B.
- C-LIN verifies PROT-R in `N_1` and `N_0`, and turns red for verdicts that rely on PROT-R if PROT-R fails
there.
- The tiers include PROT-R.
**G2, resolved** (A2.2).
*The multiplier convention* is justified from QA's P3 alone, independently of the R-G example:
- P3 arms individual couplings, per tick and per edge (QA:131, QA:242, QA:838);
- P3 loads coefficients without altering the structure of the rule (QA:129–131, `k_ii = 0` for loaded
coefficients).
Both alternatives are stated, with sound reasons for rejection:
- replacement, which brings in NNB (QA:805), linearizes armed `Π_B` and breaks `Π_A ⊂ Π_B`;
- gated edges that cannot be armed, which has no source and is a restriction motivated by protection.
The reporting requirement makes the role of the convention visible in any (B) for `Π_B`.
*The registrability rule* is justified by K-decidability and by AP1's identification of the meter by
procedure. AP1:617 treats an unheralded failure of coupling as a registration that yields a different
instrument. That supports keeping registrations whose coupling acted only conditionally. Both alternatives
are stated:
- the effective-coefficient rule is not K-decidable;
- the K-determined rule conditions access on knowledge of a gate, which AP1 does not do.
Calling the second "motivated by protection" is a strong label. The primary reason, AP1's practice, is
adequate on its own.
The two consequences of the rule for R-G are stated, and (B) records must report reliance on the second
one. Since A2 discloses that both rules were written after the example, I see no residual bias that
reporting does not expose.
**G3, resolved** (A2.3). Transported record slots stay registrable, as AP1 SA-1(b) allows.
**G4, resolved** (A2.4).
- `P` may not mention determination, bias or knowledge of `Q*`-class functionals, or PROT-*. That excludes
trivial restatements of the conclusion.
- Sufficiency must be argued in the record.
- Candidates are ordered by the earliest step among (s1)–(s5) that they secure, and every candidate is
reported.
- The restrictions are adequate. See nit H1.
**G5, resolved** (A2.5).
- "Reviewed" means the reviewer's confirmation is recorded on #1198 before the first `RESULT.md` push.
- A post-result amendment that affects the decision voids the affected verdicts, and they can be
re-established only by a new unit.
- The §A.41 row works. See nit H2 on its data source.
**G6, resolved** (A2.6).
- The quote is verbatim with #1169 c.6719192859 (amaybaum, 2026-11-08T08:19:45Z). I compared it line by
line, including the closing sentence "We would still need to demonstrate physical realizability and
establish the remaining conditions". The classical-imitation quote is a faithful excerpt of the same
record.
- Positive requires (A) with PROT proved, clauses (a)–(c) met, every control green, and an exhibited
contextuality witness certified over tomographically complete equivalences, with the blocked spanning
reads shown. Without the witness the tier is Partial.
- (C-B) and the other partial outcomes map to Undecided.
- "Otherwise shown to fail" is deleted.
- No combined tier is reported, `Π_A` comes first, and the more favourable class is never promoted.
- Every outcome maps to exactly one tier, and no tier criterion falls outside the decision rule. The mapping
adds no freedom.
- In `Π_B`, a pass of USE-ctx or a witness may rely on P3 or E-iso. SC-2 already requires the record to
name the supplied element that each verdict uses, which covers the owner's "requires an additional
physical assumption".
**G7, resolved** (A2.7). Both slots are registered at one moment between ticks, so the control exposes
`u + v` as QA's two-slice receiver does.
**G8, resolved.**
- `T` and `T′` have equal duration.
- I checked the monotonicity table entry by entry against `Π_A ⊂ Π_B` and PROT-R ⇒ PROT-D ∧ PROT-B. It is
correct.
- The AP1:338 link is fixed.
### Nits (non-blocking)
- **H1.** For (C-R), state in `RESULT.md` that the ordering by (s1)–(s5) refers to the same steps applied to
active and terminal cells together, as in C-LIN's PROT-R route. Also state that "no candidate found" is
reported explicitly when no `P` is shown sufficient.
- **H2.** For the §A.41 row of A2.5, read the push time of the first `RESULT.md` commit from structured host
data: the `created_at` of the first workflow run whose `head_sha` contains `RESULT.md`, or the PR
timeline's push or synchronize events. Do not use git commit dates, which the writer sets (§A.44 spirit).
- **H3.** Calling the K-determined registrability alternative "CC-RECON" in A2.2 is stronger than needed.
Its rejection rests sufficiently on AP1's practice (AP1:617). No change is required.
### Item 3: final readiness
The preregistration is ready for derivation once the A2.5 precondition is met: the A1 and A2 confirmations
recorded on #1198 before the first `RESULT.md` push.
What is fixed and unaffected by the amendments:
- the construction `G_σ`;
- the two classes, with access, archive-swap, E-iso gate semantics, registrability and the multiplier
convention;
- the decision rule: PROT = D ∧ B ∧ R, outcomes A, A′, B-D, B-B, B-R, C-D, C-B and C-R, attribution, and
the first missing premise `P`;
- the controls, the countercontrols and the tiers.
The amendment chain and the review anchor are measurable. No outcome is labelled favourably regardless of
the result.Generated by Claude Code
… UNVERIFIED) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
… note (WIP / UNVERIFIED) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
…rding) (WIP / UNVERIFIED) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
Owner
Author
Review provenance: independent results review of M-INACC (RESULT at
|
| Reviewed SHA | Verdict | File mtime (UTC, unattested) | sha256 |
|---|---|---|---|
0e683793 |
ACCEPT WITH CHANGES (F1–F6). Both Negative verdicts stand. | 2026-11-08 08:46:29 | fb98066feb02340313396cf7e2038f5a35469bc4326ec71593308a57a09dc22e |
07bd82d0 |
ACCEPT. Results review closed. Two nits remained; they were applied in 11cc2ede (the M2D anchor, and the wording "PROT-R′, for successor units only"). |
(same file) | (same file) |
REVIEW-RESULT-0e683793.md
# Independent review: M-INACC-1 result at `0e683793`
- **Object.** `verification/programmes/oi-qm/reconstruction/minacc-1-20261108/RESULT.md` at
`0e683793466bd4ff337683c15b0e7abd03da0db3`. It is a single-parent commit on `90e950e5` and adds only
`RESULT.md` (588 lines).
- **Governing text.** `DESIGN.md` at `75c0befc`, amended by A1 at `bcf2aba4` and A2 at `90e950e5`.
- **Reviewer.** The same independent model reviewer as for the preregistration. The review was read-only. I
fetched nothing, made no edits and posted nothing.
- **Exact checks.** I ran small exact checks of the record's own stated instances: one instance each, with
no search over protocols or rules. They are listed at the end. They are not evidence and are not
committed.
## Verdict: ACCEPT WITH CHANGES
**Both Negative verdicts stand.**
- **`Π_A`: (B), type (B-D), tier Negative.** The verdict stands. I re-derived `E_A` by hand. The exact check
on the stated `L = 8` instance gives a point mass in all 64 record branches under `G_σ`, and uniformity in
all 64 branches under `N_1` and under `N_0`. `E_A′` independently gives the same type, with known-0
supplies only (branch probability 1/16).
- **`Π_B`: (B), type (B-D), tier Negative.** The verdict stands, because `E_A ∈ Π_A ⊂ Π_B`. `E_B` also
works, but `Π_B`'s outcome does not depend on it.
None of the changes below bears on either outcome. They concern one attribution to a source, the forward
correction of PROT-R, and the wording of several statements.
## What the review confirms
### 1. `E_A` and `E_A′`: re-derived by hand
**The OR form.** `u_{i+1} + (1 + u_{i+1}) u_{i+2} = u_{i+1} ∨ u_{i+2}` over `F_2`, so
`f_i = OR(u_{i−1}, u_{i−2}) ⊕ OR(u_{i+1}, u_{i+2})` is an identity of (1). The exact check agrees on all 64
configurations at `L = 6`.
**`E_A`, tick 1.**
- `u_{−1}(1) = 0 + OR(1, 0) + OR(x, 0) = 1 + x`.
- `u_0(1) = y + OR(α_1, 1) + OR(0, 0) = y + 1`, and `v_0(1) = x`.
- `f_{−1}` reads sites −3…1, and `f_0` reads sites −2…2, all of them in `R`.
**`E_A`, after the refills.** The refills are: −1 with known `v = 0`; −2 with known `u = 1`; −3, 1 and 2
with known `u = 0`.
- `u_{−1}(2) = 0 + OR(1, 0) + OR(y + 1, 0) = y`.
- `u_0(2) = x + OR(α_2, 1) + 0 = x + 1`, and `v_0(2) = y + 1`.
So cell 0 is sharp, with `(u_0, v_0) = (r_1, r_2 + 1)`. Saturation (`OR(·, 1) = 1`) removes the reader's
kick at both ticks.
**`E_A′`.**
- `r_1 = w + x`.
- `s_1 = α ∨ x`.
- In the branch `s_1 = 0`, `z = u_0(1) = y + r_1` and `v_0(1) = 0`.
- `r_2 = w_2 + z` and `s_2 = α_2 ∨ z`.
- In the branch `s_2 = 0`, `u_0(2) = w_2 = r_2` and `v_0(2) = 0`.
- The branch probability is 1/4 · 1/4 = 1/16. Here `z` is uniform given `s_1 = 0`, because `y` is.
Every step is a permitted `Π_A` action:
| Requirement | How the protocols meet it |
| --- | --- |
| Supplies | P2 ready cells, one known slot each. Known value 1 is used only at −2 in `E_A`, through H-PREP |
| Registration | P1 registration of cells of `R` between ticks, one functional per cell (A1.5). In `Π_A`, every cell meets the registrability rule, because every edge has multiplier 1 |
| Archiving | Each registered cell is archived and refilled at the same moment, with a fresh P2 cell (D§3.3, A1.6) |
| Forbidden resources | No arming, isolation, translation, vacancy, herald or feedback is used. Both protocols are non-adaptive |
**The exposed functional.** It is `u_0 + v_0` of cell 0, with `Q* = 1`. Cell 0 is a source cell that is
never registered, so it is active at `t = 2`. For `E_A` the record branch has probability 1; for `E_A′`, the
branch `s_1 = s_2 = 0` has probability 1/16. The conditional law is given exactly: a point mass. Extra
archiving records only refine the branches, and refinement cannot undo a determination.
### 2. CC-OFF is green and not vacuous on `E_A`
Under `N_1`, the same reading still happens: `r_1 = 0 + u_{−2} + u_0 = 1 + x`, so `x` is recorded. But the
reader's kick masks the conjugate slot: `u_0(1) = y + α_1`.
The control therefore exercises exactly the backaction that `G_σ` cancels. The exact check gives uniform
`u_0 + v_0` in all 64 branches under `N_1` and under `N_0` (for `E_A′`, in all 256).
On `E_B`, CC-OFF is green but weak (F6).
### 3. The outcome, the tier and the attribution follow from the rule
- `Π_A` is (B) under D§4.2 (B), with the required elements present:
- the protocol;
- the resources and their status;
- CC-OFF;
- C-L3 reported;
- blocking premises named.
- `Π_B` is (B) by inclusion. The pair (B, B) is admissible (A1.3).
- The attribution under A1.3 for (B, B) is the gate together with the `Π_A` resources, archive-swap
included. That is correctly applied: `Π_B`'s added resources are sufficient through `E_B` and are not
necessary.
- Both tiers are Negative under A2.6. No combined tier is reported, and `Π_A` comes first.
- No favourable branch was promoted. The exposure is a branch unfavourable to the framework, and it is
established at hand-checkable exactness, with the linear-limit countercontrol non-vacuous.
### 4. PROT-R: the author is right, and my G1 claim was false
The countercase is correct. Take every cell ready, with known `u = 0` and unknown `v`. Then
`u_0(1) = v_0(0) + f_0(0) = v_0(0)` under `N_1`, `N_0` and `G_σ` alike; the exact check confirms this at
`L = 5`. Registering `u_0(1)` determines `u_0(0) + v_0(0)`, a `Q* = 1` functional of a cell that was active
at `t = 0`.
My G1 statement, "span(I_t) + R has `Q* ≡ 0` on terminal and active cells together", was **false**:
- AP1 Lemma 3 gives `ω(ρ, f′) = 0` only for `f′` on *active* cells.
- On an archived cell, the transported known slot and the registered record need not commute, so an
archived cell can be sharp.
PROT-R as adopted in A2.1 therefore fails for QA's N itself. Under A2.1's own clause, C-LIN is red for
PROT-R, (A) is unreachable for every rule, and no (B-R) is issued. The record applies this correctly.
**No verdict in this record is voided.**
- D0 voids the verdicts a failed control controls. No verdict here uses PROT-R.
- Both (B) verdicts are (B-D) exposures of current active functionals.
- The controls of those verdicts are green: C-LIN for PROT-D and PROT-B, CC-OFF, C-EX-Q, C-AVG and
C-IMPORT.
- An unreachable (A) could bias a rule only toward non-(A). The (B-D) criteria are independent of PROT-R,
so the exhibited exposures are unaffected.
**The correct form** (see F2):
> PROT-R′(Π): for `t ≤ t′` and a `Q* = 1` functional `f` on the cells active at `t`, such that `f(t)` is a
> function of the configuration of the cells active at `t′` alone, `f(t)` is neither determined nor biased
> given `K` at `t′`.
This restricts retrodiction to information still held in the unregistered part. In the linear limits,
`f(t)` is then a transported linear functional `f′` supported on active cells, and `Q*(f′) = 1` because
transport, free ticks and swaps are symplectic. Lemma Q(iii) at `t′` gives non-determination, and (s5)
gives uniformity. So PROT-R′ holds in `N_1` and `N_0`, and the trivial countercase is excluded, because it
depends on the archived cell 0.
### 5. P-GK
**It is admissible.** A2.4's "`Q*`-class functionals" was written (G4) to exclude restatements of the
protected conclusion, the `Q* = 1` class and PROT-*. A statement about K-knowledge of single gate slots
(`Q* = 0`) is a restriction on the protocol class, not a restatement. I rule it admissible under the
intended reading.
**Its sufficiency argument is sound.** With every acting gate K-fixed, the step on each branch support is
the linear step of a fixed symmetric graph. The supports stay affine by induction, and QA's proof applies,
adaptive protocols included.
**The CC-RECON flag is correct.** The record's assessment ("the mechanism switched off") understates the
effect; see F3.
**The ordering follows A2.4.** P-GK secures (s1)–(s3) and (s5). P-NR and P-1 secure no step and are listed
after it.
### 6. Node 1 is correct
- (s1) fails first: `F_σ` is non-affine through the terms `u_{i±1}u_{i±2}`.
- (s2), (s3) and (s5) fail with it. `E_A` shows concretely that (s2), Lemma 3 isotropy, fails.
- (s4) transfers.
- `Q` is conserved: `Σ u_i f_i = 0`, and the exact check finds 0 of 4096 changes at `L = 6`. Yet `E_A`
produces a sharp active cell, so conservation alone does not protect.
- C-LIN reproduces the proof in `N_1` and `N_0`. I checked the argument in §6.3: the `κ + ρ` step uses
`ω(ρ, ρ) = 0` and disjoint support.
- The `G_SM` countercontrol fails as required.
### 7. Controls, self-checks, RO-2 and C-NS
| Check | Instance | Bits | My result | Agrees with the record |
| --- | --- | --- | --- | --- |
| c1 | `E_A`, `L = 8`, `R = {−3, …, 2}`, hidden sources at 3 and 4 | 16 | Identities hold in 65 536 of 65 536 assignments. `G_σ`: 64 branches, all determined. `N_1` and `N_0`: 64 branches, all uniform | Yes |
| c2 | `E_A′`, `L = 8`, `R = {−4, …, 2}`, hidden source at 3 | 16 | `G_σ`: `P(s_1 = s_2 = 0) = 1/16`. The 64 determined branches are exactly those with `s_1 = s_2 = 0`, with point mass `(r_2, 0)`. `N_1` and `N_0`: 256 branches, all uniform | Yes |
| c3 | `E_B`, `L = 8`, multipliers as in §2.1 | 16 | Identities hold. `G_σ`: 8 branches, all determined. `N_1` and `N_0`: uniform | Yes |
| c4 | The step on `L = 6`, all 12 slots unknown | 12 | `Q` changes: `G_σ` 0, `N_1` 0, `N_0` 0, `G_SM` 1664, `G_σ` plus center term 2048. OR form and inverse hold | Yes |
| c5 | `L = 5`, every cell ready with known `u = 0` | 5 | `u_0(1) = v_0(0)` under `G_σ`, `N_1` and `N_0` | Yes |
Each check stays within A1.13's bound: one stated instance, at most 16 bits, and a fixed list of rules.
**Additional fact from c2's instance.** Under `G_σ`, all 256 branches of `E_A′` are non-uniform. The 64
branches with `s_1 = s_2 = 0` are determined, and the other 192 are biased. So `E_A′` gives (B-B) with
probability 1 using known-0 supplies only (F5).
**C-NS** is correct. Disjoint backward cones of the two wings' records, together with H-PS and settings
fed back only from local records, make each complete local history independent of the remote settings.
Main:364 is the right anchor.
**RO-2** is correct as stated. Copies of `E_A` spaced 6 apart have disjoint windows: each identity reads
only sites −3…2 of its own copy. The statement about adjacent targets is honestly left undecided.
**C-P1 and C-P2** are green, as definitional controls.
**C-IMPORT** is green. Its item (iii) holds: the class definitions are those of DESIGN, A1 and A2, and no
amendment is added here.
**USE-ctx** is correctly left unevaluated under (B).
### 8. Routes not walked
D§4.3 says "the walk stops when each class has an outcome". R-G decides both classes, so leaving R-N, R-R,
R-T and R-C unwalked is permitted.
Composition, Q3, is nonetheless covered in §5: absolute exposure in one system, parallel copies, and
exposure across adjacent systems.
### 9. Mechanics
- **Diff.** The commit adds only `RESULT.md`. `DESIGN.md`, A1 and A2 are unchanged from `90e950e5`.
- **Links.** All 5 blob links are pinned to `f88c1842`. Each anchor says what is claimed: Main:364, AP1:533
and 677, M2D:483, QA:458.
- **Lean.** There is no `readWriteSourced_` identifier.
- **Odd `q`.** No statement about odd `q` is made.
- **Register.** Clean.
- **A2.5 timing.** The check passes on host data:
- c.6719242384 was posted at 08:25:17Z and c.6719247117 at 08:25:49Z;
- workflow run 42463717716 has `head_sha` `0e683793`, event `pull_request`, created 08:37:21Z.
- **§A.42 item 8.**
- The #1198 and #1169 comments are provenance.
- Sources are support on `main`.
- DESIGN, A1 and A2 land with the record.
- The self-checks are uncommitted controls. No verdict rests on them: every verdict rests on identities
written out in the record, which I re-derived by hand.
## Findings
**F1 (should-fix). An attribution to M2D is overstated (§6.2, L371–374).**
The record says "M2D's suggestion that a symmetric switched graph would keep the protection because it
keeps `Q`". M2D makes no such suggestion. It records that Lemma Qσ(a) keeps conservation, and it leaves
open whether the protection survives (M2D:858–864).
**Fix:** "M2D left open whether a symmetric switched graph, which keeps `Q` (Lemma Qσ(a)), keeps the
protection; for `G_σ` it does not."
**F2 (should-fix). Correct PROT-R forward (§6.3, L417–436; §9).**
The record correctly reports that A2.1's PROT-R is refuted. It should also state:
- that the false premise originated in the reviewer's A1 confirmation (G1, "span(I_t) + R has `Q* ≡ 0` on
terminal and active cells together"), so that provenance is accurate;
- a corrected form, for any successor: PROT-R′ above, retrodiction of information still held in the
unregistered part, which holds in the linear limits.
It should state both without adopting PROT-R′ or re-deciding anything. If the owner wants the preregistration
itself corrected, a post-result amendment A3 that states "does not affect the decision" is the route A2.5
provides.
**F3 (nit). The assessment of P-GK understates its effect (§0 item 8; §4 row 1).**
In `Π_A`, every ready cell has one unknown slot, and an unknown `v` becomes an unknown `u`, and so an
unknown gate, after one tick. The hidden sector enters every cone. So P-GK leaves essentially no protocol
of `Π_A` that touches unknowns for more than a tick.
**Fix:** call it degenerate, which empties `Π_A` of nontrivial protocols, rather than "the mechanism
switched off".
P-NR is similarly close to forbidding all registration in `Π_A`, because P1 requires a refill at the
registered site. The record's "not decided" for whether P-NR blocks every exposure is acceptable.
**F4 (nit). The "Content proviso" for P-GK (§4).**
Record my ruling: P-GK is admissible under A2.4's intended reading.
**F5 (nit, optional). A stronger statement about `E_A′`.**
`E_A′` biases `u_0 + v_0` in every branch under `G_σ`: (B-B) with probability 1, using known-0 supplies
only. The record may add this to §3.3, as an elaboration on c2's own instance.
**F6 (nit). CC-OFF on `E_B` is weak.**
Under `N_1` the only coupling is removed. Under `N_0` cell 0 has no link to the readers at all. The control
shows only that the gate is the sole channel. That is adequate for the purpose, and `Π_B`'s outcome rests
on `E_A`, whose CC-OFF is non-vacuous.
**Fix:** say so in §2.1.
## Statement on the verdicts
- **`Π_A`: the Negative verdict stands.** The outcome is (B), type (B-D), through `E_A` in every branch and
`E_A′` in a branch of probability 1/16, over green controls. It is attributed to the gate of `G_σ`
together with P2 ready cells, P1 registration and archive-swap refills.
- **`Π_B`: the Negative verdict stands.** The outcome is (B), type (B-D), by `Π_A ⊂ Π_B`. `E_B` is
additional.
- **No verdict depends on PROT-R.** The refutation of A2.1's PROT-R is correct, and it voids nothing in this
record.
***
## Confirmation at 07bd82d0
- **Object.** `07bd82d07417c7c550b029bd54907c0dd7a6b04e`, a single-parent commit on `0e683793`. It edits
`RESULT.md` (+65/−15) and adds `amendments/A3-post-result-prot-r.md` (88 lines).
- **Method.** The review was read-only, with no fetch. I re-ran one exact check on c2's stated instance.
### Verdict: ACCEPT. The results review is closed.
| Check | Result |
| --- | --- |
| DESIGN, A1 and A2 byte-identical | Confirmed: `git diff --quiet 0e683793 07bd82d0` on all three succeeds |
| Verdicts, labels and tiers | Unchanged. The diff touches no outcome row, label or tier. Both classes remain (B), type (B-D), Negative |
| (B-D) verdicts | Still rest on PROT-D and PROT-B only |
| Links | All 6 blob links are pinned to `f88c1842` |
### Findings F1–F6
**F1, resolved.** §6.2 now says that M2D left the question open, and for `G_σ` the protection does not
survive. Nit: the new anchor M2D:858 sits in the bullet about `G_SM`. The statement about symmetric graphs
is at M2D:628 ("for `G_SM` and for a symmetric `G(x)`") and at L860–864. Retarget the anchor at the next
touch.
**F2, resolved.**
- §6.3 and §9 attribute the false premise to the reviewer's G1, and §6.3 quotes PROT-R′ exactly as I gave
it.
- A3 states in its first sentence, in bold, that it does not affect any decision. It identifies itself as a
post-result amendment under A2.5 and changes no outcome, control, tier or verdict.
- A3 states PROT-R′ exactly as given, with "linear" made explicit, which is implicit for `Q*`.
- A3's argument for PROT-R′ in the linear limits is correct. A function of the cells active at `t′` alone
is, under linear symplectic transport, a linear functional `f′` supported on those cells with
`Q*(f′) = 1`. Lemma Q(iii) and (s5) then apply.
- The statement that `E_A` violates PROT-R′ at `t = t′ = 2`, where PROT-R′ reduces to PROT-D, is correct.
**F3, resolved.** P-GK is now called degenerate in `Π_A`, and P-NR "nearly degenerate".
**F4, resolved.** My ruling that P-GK is admissible is recorded.
**F5, resolved, and the numbers are right.** Re-run on c2's instance under `G_σ`:
- 64 branches are determined;
- 192 branches are biased;
- in the biased branches, the conditional probability of the value 1 is 1/3 in 64 branches, 4/9 in 32,
5/9 in 32 and 2/3 in 64. This matches the record's set {1/3, 4/9, 5/9, 2/3}.
(B-B) with probability 1 on that instance is correctly stated as an additional exposure. The (B-D) verdict
is unchanged.
**F6, resolved.** §2.1 states that CC-OFF on `E_B` is weak and that `Π_B` rests on `E_A`.
### Nothing new is wrong
The new text adds no claim beyond what the review and its checks support.
**Nit.** The unit's own register invariant (D§7) scans for the §A.33 family of revision-history phrases.
"Corrected form" appears twice: as a bold lead in `RESULT.md` §6.3 and as A3's section 4 heading. Both name
a property for successor units, not a revision of a claim, so I do not treat them as a substantive
violation. Renaming them to "PROT-R′, for successor units only" at the next touch would satisfy the scan
literally.
Neither nit affects any verdict, so the results review is closed.Generated by Claude Code
Owner
Author
Review provenance: confirmation at
|
…9 (WIP / UNVERIFIED) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
Owner
Author
Review provenance: confirmation at
|
…standing line (WIP / UNVERIFIED) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
Owner
Author
Review provenance: confirmation at
|
This was referenced Nov 8, 2026
amaybaum
marked this pull request as ready for review
November 8, 2026 12:42
Owner
Author
Merge record: #1198 M-INACC-1 (owner-approved, chat, 2026-11-08)The owner (amaybaum) approved this in chat with the coordinating session on 2026-11-08: "Approve #1199 merge and #1198 integration".
Merged as Checks:
Scope. The preregistration, the amendments and the negative results land unchanged:
This is not a general no-go: it rules out this route to M-INACC under its stated conditions, not every OI mechanism. It is a model-reviewed paper record, not human-verified. Main's push CI is running and its result will be reported here. Generated by Claude Code |
This was referenced Nov 8, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
WIP / UNVERIFIED (owner status label, pending the integration decision). This is a paper-only research unit for #1169, M-INACC-1. It has been reviewed independently by a model reviewer, not a human.
f649b3475c9d69f98cf9a6ecab9c1dd076096834, the reviewed exact head.Files
All files are under
verification/programmes/oi-qm/reconstruction/minacc-1-20261108/.DESIGN.md: the preregistration, frozen at75c0befc.amendments/A1-prereg-review.mdandamendments/A2-a1-confirmation.md: both were written before any result.RESULT.md: the derivation and outcome.amendments/A3-post-result-prot-r.md: a post-result note. It changes no decision.What M-INACC establishes (paper derivation, model-reviewed)
These hold within the registered scope: the symmetric state-dependent graph
G_σat q = 2, the classesΠ_A ⊂ Π_B, and P1 and P2.Π_A. ProtocolE_Auses the fixed rule always on, ready cells from P2, and registration with refill from P1. It determinesu + v(Q* = 1) of an active, unregistered source cell in every record branch. VariantE_A′uses known-0 supplies only. It exposes the same functional with probability 1/16 and biases it in every other branch.Π_B. ProtocolE_Barms one gated edge and determines the same kind of functional.udoes not make the full map reciprocal.G_σ; (s2), (s3) and (s5) fail with it; (s4) transfers.What it does not establish
G_σand these classes only. It is not a no-go for every observer-level extension.Π_Aprotocols. It is reported, not adopted. InΠ_Ait is degenerate: it empties the class of nontrivial protocols, so it is target-tuned.Review record on this PR
11cc2ede), 6719539235 (at4ac0a7e6) and 6719654362 (atf649b347).Not authorized by this PR: merge, computation, premise adoption and claim promotion. Integration needs a separate owner decision.
🤖 Generated with Claude Code
https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb