Repository navigation
A5-Q3: does any A6 extension to affine offsets (E1–E3) have independent justification? (#1049) - #1202
Merged
Merged
Conversation
Fixes the question, the statements of E1-E3 (core file N9), the evaluation criteria, the decision rule (S/M/N; N valid), the controls (linear limit, target-import check, target-tuned countercontrol E*) and the invariant-to-checkpoint table, before any assessment is written. Paper-only; pinned to main 9c20147. No assessment, computation, manuscript change or premise adoption. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
…iew (WIP / UNVERIFIED) Applies F1-F10 and N1-N7 of the independent review of f71bdc8 before any assessment exists. A1 governs where it differs from DESIGN.md and restates the criteria, decision rule, controls, invariants and reference trace as the operative rule. DESIGN.md is unchanged. Paper-only; pinned to main 9c20147. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
…VERIFIED) Applies G1-G4 and H1-H7 of the re-review of d7b6d32 before any assessment exists: outcome on J1-J5, C-CAL replaced by E4 on the whole rule, transformation-law exemption narrowed with an E-star-law countercontrol, and literature-only J3 support searched, specified and labelled. DESIGN.md and A1 unchanged. Paper-only; pinned to 9c20147. 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 Q3 preregistration (f71bdc8 → A1 d7b6d32 → A2 ab0e1da: ACCEPT FOR ASSESSMENT)An independent model reviewer (a subagent) wrote this review; it is not a human review. The reviewer is not named, and the time below is unattested. The text is posted verbatim. This record is posted before any assessment text exists; the preregistration is DESIGN.md at
REVIEW-PREREG-f71bdc87.md# Independent review: A5-Q3 preregistration (#1049), checkpoint 1
- **Object:** `verification/programmes/substratum/a5-linear-affine-20261104/q3-a6-offsets-20261108/DESIGN.md`
- **Head:** `f71bdc8706300a743c03346a7b2d1d0bee4f9a49`. Its parent is `9c201475ba6fd8f341591d14dd8e88db2e2aaa90`. The commit adds this one file, 424 lines.
- **Reviewer:** an independent session. I did not write the object. I worked read-only and posted, committed and pushed nothing.
## Verdict: **REVISE**
Most of the rule is well built:
- The candidate set is quoted correctly.
- The Lean restatement is faithful.
- The target is named so that it can be excluded.
- The owner's boundaries are carried.
- (N) is admitted.
- The O5 boundary sits where the owner put it.
- The pins resolve.
Three defects remain, each fixable in the text. Each one bears directly on the verdict that the assessment will produce.
1. Two clauses can count *yielding T1* as a demerit. This breaks the rule's own C-TI standard, and the effect falls on E1 alone.
2. The rule has no positive control. Its reach is not calibrated, and nothing shows that it could ever return (S) or (M).
3. B2's "new role" clause is undefined. Its one example is the N9 finding about E1. It probably decides E1's J3 result.
The rule should be revised before any assessment is written. The revision should be re-reviewed.
***
## Findings
### Blocking
**F1. Two clauses can count yielding T1 as a demerit, and only E1 is exposed.** §5.2 states that no clause "takes as a merit or a demerit whether an extension yields T1, T2 or ¬T". Two clauses can do exactly that.
- **(a) C2, "target-adjacent".** The clause reads: "… is logically equivalent to one of them on the rule class at issue". It does not say whether equivalence is judged for the imported assumption alone or together with 𝔅.
- E1's import ("b is not transported", with the quantifier over all g) is not equivalent to T1 on its own.
- Together with 𝔅 (`a6cov_all`) it is equivalent to T1 for K ≥ 2 and odd K = 1. That is N9's own computation, and I re-derived it by hand: Cov_E1 ⇔ siteAct g b = b for all g.
- Read the second way, C2 grades E1's import target-adjacent *because E1 derives b = 0*. That penalizes a derivation for its conclusion. Under that reading, the core file's criterion-1 success (a principle that implies b = 0) could never pass.
- E2 and E3 cannot trip the clause. They force nothing, and ¬T ("a nonzero offset retained") is not *forced* by either of them.
- **(b) D1/D4-P5, the "imposes no condition" sources.** Several A6 sources characterize A6 as imposing no condition:
- Substratum:102: "once it is in place the local transformation law imposes no further condition on the rule";
- SM:118, in the same words;
- Main:726: "(xii) restricts no rule", which in its ledger sentence carries no scope qualifier;
- the `a6cov_all` docstring: "restricts no link-coupled rule".
E1 restricts b, and E2 and E3 restrict nothing. Whether E1 is then graded *tension* or *inconsistent*, which fails J4, is not decided in advance. The two D-grade definitions both apply arguably. The sources say "in the form formalized" in one place and nothing in another. Consistency with these sentences correlates exactly with T1 versus not-T1.
**Required.**
- In C2, state that equivalence to T1, T2 or ¬T is judged for the imported assumption on its own. What the assumption yields together with 𝔅 is recorded under A1 and never under C.
- State in advance how the "imposes no condition / restricts no rule" sources are graded for an extension beyond the linear class. Either they are statements about `A6Cov` on additive link data, so an extension that restricts b is at most *tension*, or the opposite, with the reason given. Apply the grading identically to all three extensions.
- Add both clauses to the C-TI table.
**F2. No positive control; J6 is uncalibrated, and the rule may be unable to return (S) or (M).** C-CC is a negative control. C-LIN is a well-formedness check that all three candidates pass by construction (see F7). Nothing shows that the rule can accept anything. Several features push toward (N) regardless of the merits:
- **J6.** J6 requires a consequence that goes beyond "A6 for offset-carrying rules", beyond A1 and A2, and beyond T1, T2 and ¬T. It must be checkable against a result at the pin.
- The baseline itself probably fails this test. On the linear class, `A6Cov` is an identity whose "content is the interface, not a constraint" (BackgroundIndependence:52–55, ROADMAP P1). Its downstream consequences in the corpus (SM:114–118: link connection, plaquettes, local gauge reading) are T2 or O5.
- The natural candidate consequences of E2, such as an affine (translational) part of plaquette holonomies, are link-action statements. A3 forbids deriving those.
- So the O5 boundary and J6 may together exclude the only consequences an extension could have.
- **§5.4, third bullet.** A clause that cannot be evaluated "counts as not held". That is defensible, since the burden of proof is on the extension, but it adds to the tilt.
- **J6 and §A.29.** J6 is warranted *if* (S) is a recommendation to adopt an extension as a premise: §A.29 together with §A.45 rule 5 then applies. But the owner's question was whether an extension is "independently justified" (c.6719886996), and J3 tests that. J6 tests §A.29 adoptability. Folding J6 into "independently justified" makes the outcome label claim more than J3 decides. A reader would take (N) to mean that no justification exists, when the failure may be only the absence of an independent consequence.
**Required.**
- (i) Add a positive control decided before the assessment: apply J1–J6 (J2 trivially) to the baseline `A6Cov` on the linear class, or explain why J6 binds the extension and not the baseline. If the baseline would fail J6, say so now.
- (ii) Report two sets: J₁₋₄ (J1–J4: independently justified and consistent) and J (J1–J6: also hard to vary and with an independent consequence). The outcome (S/M/N) stays on J. The per-extension verdict then shows which clauses produce an (N).
- (iii) State whether A3 and A4 entries can count toward J6. J6 now excludes only A1 and A2, and A3 is the O5 boundary.
**F3. B2's "new role" clause is undefined, its example is N9's E1 finding, and it probably decides E1's J3.**
- Without B2, E1 arguably imports nothing beyond 𝔅. "Untransported" is the default for a datum `A6Cov` does not mention, so E1 would pass J3 trivially. B2 is therefore the operative clause for E1.
- Its only example ("the additive typing `V →+ V` … used to constrain an offset") is N9's pressure-test conclusion ("additivity relocated to the links"), written in as the pattern before the assessment. §8 discloses that the author read N9.
- The example also misplaces the mechanism. In Cov_E1, M drops out through `a6cov_all`. What constrains b is that g ranges over AddAut V (no translations) and that b is untransported, not the additive typing of M.
- "Role on `main`" has no definition. The stated role ("to carry linear rules") is [D]; no cited source assigns it.
- Applied generally, the clause catches every extension: E3 uses `siteAct` on an offset, and E2 uses the `gaugeLink` transport on affine maps. The rule does not ask for that symmetric application.
**Required.**
- Define an element's role as the role a source cited at the pin states for it.
- Require a B2 table that runs each 𝔅 element used in the offset sector through each of E1, E2 and E3. The elements are the transformation class AddAut V, `gaugeLink`, `siteAct`, the `V →+ V` typing, E4 and H-link.
- Replace the single E1-shaped example with neutral examples, or with one example for each extension.
### Should-fix
**F4. J5 is not operationalized, and the E1/E1′ case is nearly pre-decided.**
- "Supports equally well" and "the justification itself selects" are judgement calls with no procedure.
- E1 and E1′ have the same data and transport and therefore the same A2. They differ in A1: b = 0 versus no constraint. So E1 passes J5 only if its justification selects "∀ g" over "g in the stabilizer of b". Whether the "∀ g" quantifier of `A6Cov`, which C-LIN preserves, counts as that selection is not decided.
- The rule does not record that the relation is symmetric. E3's listed variants ("other transformation laws for b") include the trivial representation, which *is* E1, so E1 and E3 are each other's J5 variants.
**Required.**
- A variant counts as equally supported unless a cited source at the pin, or the extension's own stated motivation, states the feature that distinguishes it.
- State in advance whether conformity with `A6Cov`'s quantifier counts as selection.
- Record the E1↔E3 variant relation in §2.4.
**F5. C-CC: E★ can be rejected for the wrong reason, and a subtler tuned extension is not tested.**
- E★ is built on E1's data and covariance. It therefore inherits whatever rejects E1 (F3's B2, F4's E1′ variant, F1(b)). I8 accepts *any* failing clause, so the countercontrol can pass without testing J3, the clause meant to catch target-tuning.
- E★'s justification names hypercharge explicitly, so it is caught trivially. A tuned extension whose stated reason sounds neutral could pass J3: C2's "target-defined" rests on "the stated reason" or on inferring design. An example is identifying offsets modulo the A₁-block phase "because offsets are background data".
**Required.**
- Require E★'s rejection to come from J3, alone or together with D2/D3 (I8 to match).
- Build E★ on E2's or E3's data so that it does not inherit E1-specific failures.
- Add a second countercontrol with a neutral-sounding justification.
- Decide whether C2 includes a functional test: an assumption whose only role is to fix or to keep b counts as target-defined. That is the owner's "chosen merely to eliminate affine offsets". If it is included, apply it symmetrically to elimination and retention.
**F6. D3 is broader than Q2 and would catch E2 and E3 for a reason the baseline shares.**
- Q2 concerns amplitude *shifts*. D3 adds "any identification of rules that differ in b".
- Under E2 and E3, (M, b) and (gaugeLink g M, siteAct g b) are covariantly related rules that differ in b. `A6Cov` relates M and gaugeLink g M in exactly this way.
**Required.** Scope D3 to:
- identifications by maps outside the transformation class (translations, time-dependent maps); or
- a declared physical identification beyond the covariance relation.
**F7. C-LIN does not discriminate, and its "same class" clause silently excludes the affine-group half of Q3.**
- **Non-vacuity.** E1, E2, E3 and E★ all reduce to `A6Cov` at b = 0 by definition. C-LIN as written can fail no listed candidate. To show it is not vacuous, add a negative case that must fail, for example an A6Inv-based "E-inv" extension or an extension whose local class is affine.
- **Scope.** The requirement that "the transformation class is the same" fails any extension whose local group is Aff(V). That is the first clause of the core file's Q3 ("AddAut(V) or the affine group").
- §1.1 excludes such extensions, and §2.4 lists only *subgroup* variants.
- The owner's go is "compare E1–E3 as proposed", and c.6719886996 frames the comparison as E1–E3. So the exclusion is within scope.
- But the file should state that no outcome bears on the affine-local-group question. It should also state that, under Q2, gauging translations would need a justification of their gauge status.
- It should decide whether an Aff(V) reading counts as a J5 variant when an extension's own justification supports it, as "link couplings may be affine maps" arguably does for E2.
**F8. The owner record c.6719886996 exists and must be cited.**
- It was posted at 2026-11-08T09:36:19Z, 37 seconds after the commit (09:35:42Z). §7's "This drafting session did not locate its record" was accurate when written and is now stale.
- The comment records the earlier guidance verbatim: compare against existing A6 sources, identify imports, recommend whether any extension is independently justified, and "must not simply choose the extension that produces the desired gauge group … may be that none … is selected".
- It also records the unit boundary: "Q3 may read the local transformation class directly from each extension's definition. It may not derive any promotion to local gauge invariance."
**Required.**
- Quote it in the header with author and time.
- Reclassify the §7 row as support by quotation.
- Cite its boundary sentence as A3's source. A3 matches it exactly.
**F9. §A.42 item 8: the D3 safeguard quotation is not traced.** D3 quotes "the #1049 safeguard" ("as OI gauge transformations must be established separately"). Its source is the #1049 Issue body ("Scope and safeguards"), which is not on `main`. The quotation is accurate, but the §7 table does not list it. Add a row (support, by quotation) and give the full sentence.
**F10. J_c and its hypotheses.**
- A hypothesis that admits an extension to J_c should itself be classified under C2. A target-adjacent or target-defined hypothesis cannot make an extension conditionally justified. H-b is the likely case.
- Separately, E4 is in 𝔅 without qualification. The Q4 note's Q4a ("Does E4 apply to the offset (H-b)?") records that E4's application to the offset is open. State that E4 used on b is a B1/B2 import and not baseline.
### Nits
- **N1.** #1169 c.6719386464: the first quoted sentence ("A restriction designed to exclude a particular construction is treated as tuned to the target.") is refinement 1 as worded by the coordinating session, which the owner approved. It is not quoted owner speech. The second is quoted owner speech. Label them accordingly. Applying the #1169 Stage 1 standard to Q3 is this file's choice ([D]); no owner record extends it.
- **N2.** I1 and I2 assume a single checkpoint-1 commit whose parent is `9c201475`. A pre-assessment revision answering this review would break I1 as written, or would be forced into `amendments/`. State that revisions before any assessment land as a new checkpoint-1 commit, with I1 re-measured on it.
- **N3.** §A.41 coverage. Two stated obligations have no checkpoint:
- "the assessment … must report each addition" (§2.4);
- the C3 search record (§A.19).
Also, I4's "every step was done by hand" is a self-report. That is acceptable, but say so.
- **N4.** C-TI table: also list D4-P4. Controls (C-b) and (C-c) are Theorem 7 and Theorem 15, which are T2 outputs. They are used as controls "on the linear class", so they are identical for every candidate, but they belong in the table. List the F1(b) sources as well.
- **N5.** E2 restatement: b_i = Σ_{j∈N i} a_ij reaches every b only where N i is nonempty. This is trivial on the torus. Say so, or drop it.
- **N6.** 𝔅's "affine rule class" rests on amplitude-scale gauge, which Substratum:272 marks "open, referee-grade" and calls an adjoined principle. State that every verdict is conditional on it.
- **N7.** C2's "exclude a particular construction (S1, or the class of offset-carrying rules)" gives examples on one side only. Add the mirror cases (the linear class; the Stage 2(d) construction), so that the symmetry stated in C-TI is visible in C2 itself.
***
## What I checked
**Owner records**, fetched from the GitHub API: author, time and body.
- c.6719806528 (amaybaum, 2026-11-08T09:27:26Z): the quoted GO paragraph matches verbatim. The "same comment records" sentence is in the coordinating session's text of that comment.
- c.6719886996 (amaybaum, 09:36:19Z): present; see F8.
- c.6719386464 (amaybaum, 08:41:15Z): both sentences found; see N1 for their attribution.
- c.6624263637 (amaybaum, 2026-11-04T06:28:45Z): Q1 and Q2 match verbatim.
- #1049 Issue body: the safeguard sentence found; see F9.
**Commit structure.** `git show --stat` lists exactly DESIGN.md, and the parent is `9c201475`, so I1 holds as stated.
**N9 quotation.** §2.2 matches the core file at `9c201475`, lines 320–332, verbatim. I checked the E1 case analysis by hand:
- (λ−1)b = 0 for all units gives b ∈ {0, q/2} for even q;
- a transvection e_l ↦ e_l + e_k moves any b with b_k ≠ 0.
**Lean restatement** against BackgroundIndependence.lean at the pin:
- line numbers: `siteAct` :92, `A6Inv` :104, `A6Glob` :111, `linkF` :118, `gaugeLink` :124, `A6Cov` :131, `leap_siteAct` :144, `a6cov_all` :161;
- A6Instantiation.lean: `pk3e_A5` :306, `pk5_symmetric_point` :366, `cx1_complex_covariance` :411, `cx2_unitary_gaugeLink` :459, and K = 6 (`Fin 6 → ZMod q`).
The covariance checks:
- Cov_E1 reduces through `a6cov_all` to siteAct g b = b for all g, as N9 states.
- Cov_E2 holds identically for g in AddAut V. Its induced law on b_i = Σ a_ij is b ↦ siteAct g b, the same as E3's (recorded for A4; it is not an assessment).
- Cov_E3 holds identically.
The restatements are faithful. "The adopted meaning" of A6 = `A6Cov` is supported by A6Instantiation.lean:14–16 and the ROADMAP P1 row (:75).
**Pins.**
- Substratum:92–104, :163 (singlet-block U(1) as hypercharge), :270–274;
- SM:92–96, :104, :112–118, :224–240, :374;
- Main:726, items (vi), (vii), (xii), (xiii) and the "(xii) restricts no rule" ledger sentence;
- in the core file: §1.2 C1–C8, Proposition 2.6(a), 𝒜_C and 𝒜_W (§3.3), §6 Q3;
- in the Q4 note: G_0, G_v, (L), (A-lin), (A-aff), H-b, resonance, (C-a)–(C-c), N7's E1 remark (quoted correctly), Q4a and Q4b, S6 (rule-level versus coupling-level).
All resolve at `9c201475`.
**C-TI table** against §3–§4: see F1 and N4 for the omissions.
**Variants** E1′, E2's split and E3's representations: checked against N7 and N9 (F4).
**Register.** The only all-caps tokens are file and identifier names and the status label. No §A.32 or §A.33 phrase-family hits. The file is in `verification/`, so I13 is self-imposed.
**Not checked.** I did not re-read `a6-status-adjudication/result.md` beyond its opening, or the ROADMAP P1 section beyond the row and the anchor lines. I ran no Lean or code.
***
***
# Re-review at d7b6d32b
- **Object:** `DESIGN.md` at `f71bdc87` together with `amendments/A1-prereg-review.md` at `d7b6d32bb07f19a8fe0141791faa29660a75759f`, read as the operative preregistration. A1 governs where the two differ.
- **Commit:** single parent `f71bdc87`. It adds only A1, 498 lines.
- **Diff from `9c201475`:** only the two `.md` files under `q3-a6-offsets-20261108/`. No assessment file is in the tree.
- **Method:** read-only, no fetching. Every source line A1 newly cites was read at `9c201475`.
## Verdict: **ACCEPT WITH CHANGES**
The three blocking findings are resolved in substance:
- **F1.** C2 is judged on the assumption alone. The "imposes no condition" sources are graded out of scope on the offset sector, identically for every extension.
- **F2.** C-POS has been added. There are now two sets, J₁₋₄ and J₁₋₆. "Not evaluable within the authorized scope" now covers a J6 consequence that the O5 boundary puts out of reach.
- **F3.** "Role" is defined by a source at the pin. There are mandatory, symmetric B1 rows for the offset law, and a symmetric B2 table.
F4–F10 and N1–N7 are resolved or nearly so.
Four should-fix points remain: G1–G4. Each touches what an outcome means or whether a control can fail for the wrong reason. They are local text changes. They should land as amendment A2 under A1's own N2 procedure, with I1 re-measured, **before any assessment text exists**. A delta check of A2 against G1–G4 is enough. A full re-review is not needed.
***
## Status of the original findings
| Finding | Status | Note |
|---|---|---|
| F1(a) | **resolved** | C2: "Equivalence and presupposition are judged for the assumption on its own, without 𝔅"; what an assumption yields with 𝔅 goes in A1 only. The mandatory B1 offset rows are transformation laws for b, the trivial law included, so the functional test exempts them. All three extensions are treated alike. |
| F1(b) | **resolved** | D1 pre-grades the four sources as out of scope on b ≠ 0 and consistent on the linear class, for every extension. The reasons given are checked against the sources: Substratum:102 sits beside :100 (A5); SM:118 refers to SM:116's linear transport; Main:726 (xii) says "in the form formalized"; BackgroundIndependence:52–55 is scoped to link-coupled rules. Both sources are in C-TI. One residue is minor: see H1. |
| F2 | **resolved, with G1** | C-POS was added, with a predicted profile; the baseline is predicted to fail J6. J₁₋₄ and J₁₋₆ are reported. A3 and A4 do not count for J6. Non-differential failures are reported. The coordinator's departure (outcome on J₁₋₄) is assessed in G1. |
| F3 | **resolved** | Role = the role a source at the pin states. The three neutral B2 patterns are each source-backed: `A6Cov`'s docstring (:127–129, "the coupling is transported and nothing needs preserving"), the `gaugeLink` typing, and the `siteAct` docstring (:87–91). The table runs every element across E1–E3. One cell carries derived content: see H2. |
| F4 | **resolved, with G1** | J5 is operationalized. The "∀ g" selection is decided in advance, and only among variants that differ in the domain of the quantifier. That is source-based (`A6Cov`) and does not select among offset laws. The E1↔E3 relation is recorded. Residual tunability: G1(b). |
| F5 | **resolved, with G3** | E★ was rebuilt on E3. E☆ was added. Both must be rejected through J3 by the added stipulation (I8). The functional test is symmetric. A gap remains for tuned variants phrased as a law: G3. |
| F6 | **resolved** | D3 is scoped to maps outside the class and to declared identifications beyond the covariance relation. Covariant transport of b under E2 and E3 is explicitly not an identification. |
| F7 | **resolved** | The E-inv negative control fails C-LIN on the transport clause (fixed coupling, not `gaugeLink`), so C-LIN can fail. The affine-local-group exclusion is stated. Aff(V) readings are reported and not counted. |
| F8 | **resolved, nit H3** | c.6719886996 is quoted verbatim with author and time; it matches the API text I fetched in the first review. It is reclassified as support and cited for A3. |
| F9 | **resolved** | The #1049 safeguard pair is quoted in full and matches the Issue body I fetched in the first review. It is traced in §7 as mutable and dated. |
| F10 | **resolved** | J_c hypotheses are classified under C2; only independent ones, or mixed ones with a sufficient independent part, qualify. E4 and H-link used on the offset are B1 imports (Q4a). |
| N1 | **resolved** | The #1169 sentences are attributed separately; the application to Q3 is marked [D]. |
| N2 | **resolved** | Amendment-file procedure. I1 re-measured: `f71bdc87` adds only `DESIGN.md` (parent `9c201475`); `d7b6d32b` adds only A1 (parent `f71bdc87`). |
| N3 | **resolved** | I14 and I15 added. I4's self-report is noted. |
| N4 | **resolved, nit H4** | D4-P4 and the F1(b) sources are in C-TI. |
| N5 | **resolved** | |
| N6 | **resolved** | Substratum:272 is quoted correctly. I17 added. |
| N7 | **resolved** | C2's excluded-construction examples are mirrored. |
***
## Remaining findings
### Should-fix
**G1. Outcome on J₁₋₄: this resolves the J6 overclaim, but drops J5, which is part of "independently justified as the extension". J5 can also be satisfied by a motivation the assessor writes.**
**(a) The departure.** Basing the outcome on J1–J4 rather than J1–J6 does resolve my F2 point. (N) no longer asserts the absence of an independent consequence, which the baseline itself is predicted to lack. But A1 moves **J5** out of the outcome together with J6, and the two are not alike.
- `DESIGN.md` §1.1 asks whether any of E1–E3 is "independently justified as *the* extension of A6 to affine rules".
- J5 tests exactly that: whether an extension's justification selects it over variants with different consequences for b.
- An extension whose sourced justification supports, equally well, a variant with a different A1 or A2 has justified a family, not that extension. The case at issue is an offset-law variant: E1 with the trivial law against E3 with the g-law, or an E3 law given by another representation.
- An outcome of (S), "exactly one extension is independently justified", would then overstate.
- The objection to J6 does not carry over. C-POS predicts the baseline holds J5, so J5 does not make (N) structural.
**(b) Tunability.** J5's escape clause is "or the extension's own stated motivation states the feature that distinguishes it". E1–E3 have no stated motivations in N9: they are "three natural extensions". So the assessor would compose the motivation that does the distinguishing.
**Required.**
- Either base the outcome on J1–J5, with J6 reported alongside as "adoptable as a premise",
- or keep J₁₋₄ and make the outcome line state, for each member, whether it holds J5. In that case (S) is worded "exactly one extension meets J1–J4", and "the extension" is not used unless J5 holds.
- In both cases, restrict "the extension's own stated motivation" in J5 to the motivation located and cited under C1. Text composed in the assessment does not count.
**G2. C-CAL can fail for reasons unrelated to C2's calibration, or pass because the assessor was told which reading to take.** The author's flag is confirmed.
- **The anchor's referent.** At Substratum:98 the anchor sentence reads "(The second sense is what the wave-equation derivation of Stage 2 uses. **Its** observational anchor is the homogeneity of physical law …)". Grammatically, "Its" is the second sense, the no-self-term clause. A1 §5.1 instructs the assessment to "record that reading", meaning the translation reading. A pass/fail control whose source reading is supplied by the rule is weakly informative. An assessor who declines the reading would find no stated motivation ("none found"), and the rule would then be void for a sourcing reason, not a C2 defect.
- **The clause itself.** A4's translation clause is "commutes with lattice translations **up to gauge**" (Substratum:98). C-CAL's item is exact commutation. Under "up to gauge" the offset need not be uniform: the core file §6 lists "offsets under A4 'up to gauge'" as open. So the item is a strengthening of A4, which is itself an import.
**Required.** Replace the item with one whose source is unambiguous. A natural choice: E4 applied to the whole rule, "F commutes with the lattice rotations". Its source is Substratum:82, "Observed physics is rotationally invariant; no spatial direction is preferred", with SM:238. It is a statement about the whole rule, so the functional test does not catch it. It constrains b's pattern, which is recorded in A1. Its motivation presupposes no T. Alternatively, keep the A4 item but:
- state it with "up to gauge"; and
- stipulate that a C-CAL result traceable to sourcing, rather than to C2's definitions, makes C-CAL **not evaluable** and requires a replacement by amendment, instead of voiding C2.
**G3. A target-tuned assumption written as a transformation law escapes the functional test, and the countercontrols do not probe this route.**
- C2 exempts every "law for how the offset transforms". The exemption is needed for the mandatory B1 rows. But it also covers a tuned law.
- An example: on the lift, b transforms by ρ(A, B, z) = (A, B, 1), so U(1)_S acts trivially on b. Glob then contains U(1)_S, the global group returns to G_0, and that is T2. The law can be given a neutral-sounding reason ("offsets carry no singlet charge").
- Only a C1 "none found", or a B2 import, would reject it. Neither countercontrol tests that path: E★ and E☆ are both identifications, and both are caught by the functional test.
**Required.** Do one of the following:
- **Narrow the exemption** to laws given by the extension's own transformation class acting on b: g itself, the trivial law, or the law induced by the transport of the extension's data. Treat any other action on b alone as an identification for the functional test.
- **Or add a third countercontrol, E☆-law**, built on E3's data, with the ρ above and a neutral reason. Require it to be rejected through J3 (I8, §5.5).
**G4. [L]-only support for J3.**
- C-POS predicts the baseline holds J3 only through a mixed classification whose independent part is "the standard gauge principle … [L]". [L] means literature from memory, not re-read.
- Allowed as written, a J3 "independent" for an *extension* could rest on an un-reread recollection. §A.46 item 7 bars unverified material from serving as verification.
- This does not void C-POS, which is a reported calibration, not a gate.
**Required.**
- Before any [L] item is used, the C3 search must cover the corpus for an internal motivation. Candidates are SM:104's contrast with general relativity, and the name and wording of Substratum:102.
- An [L] citation must name the specific work and claim.
- Any J3 classification resting on [L] alone, for the baseline or an extension, must be labelled as such in the per-extension verdict and the outcome line. The same standard applies to the baseline and to the extensions.
### Nits
- **H1.** D-grades. "Out of scope" overlaps "tension" ("carries the source's characterization outside the source's stated scope"). Restrict "out of scope" to the D1 sentences pre-graded in A1, or state which grade takes precedence. Otherwise every D1 source could be graded out of scope on b ≠ 0, which would leave the comparison with the A6 sources that the owner asked for empty.
- **H2.** B2 table, E1 transformation-class cell: "every g is required to commute with an untransported b". This is the A1 consequence, obtained only through `a6cov_all`, written into Block B. Write the cell as read from the definition: "quantified over all g; b not transported".
- **H3.** c.6719886996's "Boundary for the unit" sentence lies outside the owner's blockquote; it is the coordinating session's text in the owner-account comment. Attribute it as N1 does for #1169.
- **H4.** C-TI table: add J5's advance decision that the "∀ g" quantifier selects E1 over E1′. Its effect correlates with T1 (b = 0 against no constraint), even though it is source-based.
- **H5.** §2's "E2 ↔ E3" line (E2 induces b ↦ g_i b_i) is a one-line derivation, not a definition. Label it [D], to be re-derived in the assessment, so that the preregistration states no result.
- **H6.** E☆'s expected rejection asserts "C1 finds no source … for 'the phase of background data is not observable'". That predicts a search result. Amplitude-scale gauge (Substratum:270; :163, "removes only the common overall phase") is a near-source on the lift. Rejection through the functional test is enough and is the required route. Mark the C1 line as an expectation.
- **H7.** B2 table, `V →+ V` row: "`linkSubstratum_A5` :147" names no file. It is A6Instantiation.lean:147.
***
## Confirmations requested
- **Original findings.** F1–F10 and N1–N7 are each resolved, as tabulated above. The residues are G1 (F2/F4), G3 (F5) and H1 (F1(b)).
- **Controls: non-vacuous and able to fail.**
- C-LIN can fail, as E-inv shows.
- E★ and E☆ can fail to be rejected, and each is rejected for the right reason, through J3, by its stipulation (functional test; for E★ also the stated T2 reason). E3 does not share that reason.
- C-CAL can fail, but for the wrong reason (G2).
- C-POS is a reported calibration, not a gate. Its J3 prediction rests on [L] (G4).
- C-TI is complete except for H4.
- **Bias toward T1 or ¬T.** I found no remaining clause that scores T1 or ¬T as a merit or demerit.
- The D1 pre-grading and C2-on-its-own remove the E1-specific demerit routes.
- The J5 "∀ g" decision favours E1 over E1′ on a cited source.
- The functional test is symmetric.
- Tunable routes remain: J5's assessor-composed motivation (G1(b)) and law-phrased tuning (G3).
- **No results in the file.** The file contains no result apart from H5 and H2's cell, both trivial and both recorded as not scored. The C-POS profile is labelled a prediction [D].
**Not checked.** I did not re-fetch the GitHub records; the comparison is against the texts I fetched in the first review. I ran no code or Lean.
***
***
# Delta check at ab0e1dac
**Object.** `git diff d7b6d32b ab0e1dac` adds only `amendments/A2-rereview.md`, 183 lines. The commit `ab0e1dac4a7288bf72df90d9caf337eb00dee3fc` has the single parent `d7b6d32b`. Read as the operative preregistration: `DESIGN.md` (at `f71bdc87`), A1 and A2, with A2 governing where they differ.
- Across the whole branch, `git diff --name-only 9c201475 ab0e1dac` lists only `DESIGN.md`, A1 and A2. There is no assessment file, and nothing outside `q3-a6-offsets-20261108/` (I1, I4, I5).
- The check was read-only, with no fetching.
## Verdict: **ACCEPT FOR ASSESSMENT**
G1–G4 and H1–H7 are resolved. Two non-blocking nits follow, K1 and K2. Neither can change a verdict on E1–E3, because the candidates and their transports are fixed in `DESIGN.md` §2.3. They can be carried into the assessment's record, or applied in a later pre-assessment amendment.
## Item by item
| Item | Status | Check |
|---|---|---|
| G1 | **resolved** | The outcome rests on \|J₁₋₅\| ("independently justified as the extension"). J₁₋₄ ("within its family") and J₁₋₆ ("adoptable as a premise") are reported alongside. "The extension" is used only of members of J₁₋₅, and the outcome line states J5 and J6 for each extension. J5's motivations are restricted to those located and cited under C1, so text composed in the assessment does not count. C-POS predicts the baseline holds J5, so J5 does not make (N) structural. The ∀-quantifier advance decision is unchanged and source-based (`A6Cov`). |
| G2 | **resolved** | C-CAL is now E4 on the whole rule, with rotations acting on site labels. Both quotations match the pin: Substratum:82 verbatim, SM:238 verbatim. Because the item acts on site labels only, H-link is not used, which keeps it apart from the open Q4a/H-b question. It is a statement about the rule, so the functional test does not apply to it. A failure traced to C2's definitions voids C2; a failure traced to sourcing makes C-CAL not evaluable. The withdrawn A4 item and its two defects are recorded correctly. |
| G3 | **resolved (K2)** | The exemption is narrowed to (i) g itself, (ii) the law induced by the stated transport, and (iii) the trivial law. E1, E2 and E3 fall under (iii), (ii) and (i) respectively, which is symmetric. Other representations are treated as stipulations, both for removing an effect of the offset and for keeping one. E☆-law has been added; its rejection must come from the stipulation through J3. Its C-LIN is stated on the same class ι → G_0, so it cannot be rejected for the wrong reason (class restriction). |
| G4 | **resolved** | The corpus is searched first, with a minimum list of locations: SM:104, Substratum:102, Main:726 (xii) and SM:114–118, all checked at the pin. [L] items name the work and the claim. Yang–Mills, *Phys. Rev.* 96, 191 (1954), and Wilson, *Phys. Rev. D* 10, 2445 (1974): the citations and the claims attributed to them are correct as far as I recall; they are [L] here too. A J3 pass resting on [L] alone is labelled "J3 ([L] only)" and counts as held, and the outcome line also gives the count of J₁₋₅ with such passes excluded. The same standard applies to the baseline, E1–E3 and the countercontrols. I18 is added. |
| H1 | **resolved** | "Out of scope" is reserved for the pre-graded D1 sentences. |
| H2 | **resolved** | E1's cell reads "quantified over all g; b not transported". |
| H3 | **resolved** | "Boundary for the unit" is attributed to the coordinating session's text. A3 also rests on the owner's blockquoted "O5 … remain unapproved". |
| H4 | **resolved** | Three C-TI rows are added: the ∀ decision, recorded as correlating with T1 and applied to every extension; the narrowed exemption, applied symmetrically; and E☆-law. |
| H5 | **resolved** | The E2 ↔ E3 line is labelled [D], to be re-derived in the assessment. |
| H6 | **resolved** | The C1 line is an expectation. The amplitude-scale near-source is named (Substratum:270, :163). |
| H7 | **resolved** | A6Instantiation.lean:147, confirmed. |
## The two points the author raised
**1. A baseline J3 pass resting on [L] alone.** This is acceptable as specified, for three reasons:
- C-POS is a reported calibration, not a gate.
- The pass is labelled "J3 ([L] only)".
- The outcome line gives the J₁₋₅ count with [L]-only passes excluded.
So a reader sees directly whether any (S) or (M) depends on unread literature, for the baseline and the extensions alike. §A.46 item 7 is respected, because the outcome is a labelled recommendation for owner decision after review, not an established claim.
One consequence should be stated in the result if it occurs. If the baseline is [L]-only and an extension's J3 pass is also [L]-only for the same reason, that pass is non-differential (A1 §4).
**2. Does SM:238's Lorentz-invariance motivation presuppose T?** I agree with the author that it does not. T1 is b = 0; T2 is the Stage 2(d) internal group and its descendants; ¬T is their negation. Lorentz invariance is a spacetime symmetry at observer level.
- It does not presuppose b = 0. On the item as stated, it constrains only the site pattern of b.
- It does not presuppose any internal group. Rotations act on site labels, with no H-link.
- It is not supported only by a consequence of T.
- It is not designed to exclude S1 or the linear class.
That Lorentz invariance is observer-level, and here applied to the microscopic rule, raises a B2 role question. It does not raise a C2 presupposition question. C-CAL tests only C2. The corpus itself makes this application at SM:238, in the derivation of the rule's form.
## Do the new controls fail for the right reason?
**C-CAL.** It fails only if C2's definitions misfire on a clean item:
- the functional test applied to a statement about the whole rule;
- equivalence judged together with 𝔅 rather than on its own, which F1(a) forbids;
- presupposition read into an observational input.
Each of these is a genuine miscalibration, and a failure traced to sourcing is routed away from voiding C2.
**E☆-law.** It is rejected through J3 by ρ, which is none of (i)–(iii) and acts on b alone. E3 does not share that stipulation. A C-LIN failure produced by restricting the class is excluded as a rejection reason.
My own hand check, not part of the file and not scored: with E3's covariance and b transported by ρ, the covariance condition reduces to ρ(g)b = g b for all g in G_0. That holds iff (z − 1)b₁ = 0 for all z, so b₁ = 0. On the uniform, cubic-invariant offsets of the Q4 note (b ∈ V_1), E☆-law therefore forces b = 0. Its global group is G_0 because ρ is trivial on U(1)_S. So it is tuned toward both T1 and T2. That makes it a stronger countercontrol, and it shows why A1 must stay unscored: the rejection has to come from ρ, never from the consequence for b.
## Nits (non-blocking)
**K1.** E☆-law's description says "E3's data and covariance". With b transported by ρ, the covariance is no longer an identity: it is the predicate obtained by putting ρ(g)b in place of g·b, which is a constraint. Wording such as "E3's data, with covariance in E3's form and b transported by ρ" would avoid implying an identity. This changes nothing in the required rejection.
**K2.** Exemption (ii) covers "the law induced by the extension's stated transport of its data". A variant could choose a transport of its data in order to induce ρ on b, for example link offsets a_ij transported by ρ(g_i), and so pass through (ii). For E1–E3 this has no effect: E2's transport is the fixed g_i ∘ A_ij ∘ g_j⁻¹ of `DESIGN.md` §2.3, and variants are judged under J5 for support, not under the functional test. Reading (ii) as "induced by transport of the data under g itself, as in `DESIGN.md` §2.3" closes the gap.
## Mechanics
**Pins.** Every line A2 newly cites resolves at `9c201475`:
- Substratum:82, :98, :102, :163, :270;
- SM:104, :114–118, :238;
- Main:726 (xii);
- A6Instantiation.lean:147.
**Invariants.** I1 is re-measured and holds. I2, I8, I9 and I16 are extended, and I18 is added.
**Off-main references (§A.42 item 8).** §7 adds the re-review as provenance and the H3 sentence as attributed support.
**Register.** The only all-caps tokens are file names and the quoted verdict labels. There are no hits for the §A.32 or §A.33 phrase families.
**Results.** The file states none. The E☆-law and B1-row classifications under (i)–(iii) are readings of definitions. The E2 ↔ E3 line is labelled [D].
**Not checked.** I did not re-read the [L] items (they are from memory, as labelled). I ran no code or Lean, and fetched nothing.Generated by Claude Code |
…NVERIFIED) Applies the preregistered rule (DESIGN.md f71bdc8 with A1 d7b6d32 and A2 ab0e1da) to E1-E3, the variants and the countercontrols. All controls green. Outcome (N): no extension independently justified as the extension on the record at 9c20147; conditional on amplitude-scale gauge. Paper-only; nothing adopted; A5 unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
Applies R1-R4 and n1-n4 of the results review of 118fd9c to ASSESSMENT.md: relabelling-gauge sources added to the search record; E3's import and H-passive reclassified mixed (insufficient); [L1](b) credited to neither offset law and [L2](b) marked target-adjacent, so E1 fails J3 on two grounds; SM:493 classified none found with the O5 note; E1's amplitude-relabelling tension added; reviewer rulings recorded. No set changes; outcome (N) stands. 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 Q3 (ASSESSMENT at
|
| Reviewed SHA | Verdict | File mtime (UTC, unattested) | sha256 |
|---|---|---|---|
118fd9c2 |
ACCEPT WITH CHANGES (R1–R4, n1–n4); (N) stands | 2026-11-08 10:24:27 | a15af2b6f5fcd7c5cedc34287347c140c93bb15010c61897a9dc564dc4771b19 |
25384b13 |
ACCEPT; results review closed; one optional nit (revision-history sentences in a verification record) | (same file) | (same file) |
REVIEW-RESULT-118fd9c2.md
# Independent results review: A5-Q3 assessment (#1049), checkpoint 2
**Object.** `verification/programmes/substratum/a5-linear-affine-20261104/q3-a6-offsets-20261108/ASSESSMENT.md`
at `118fd9c22a78e6232ade59aef3bec7f6865fb81c`. It has a single parent, `ab0e1dac`, and is 460 lines long.
**Operative rule.** `DESIGN.md` at `f71bdc87`, amended by A1 at `d7b6d32b` and by A2 at `ab0e1dac`. The rule text was not changed after `ab0e1dac`: `git diff ab0e1dac 118fd9c2` adds only ASSESSMENT.md (I2).
**Scope of the commit.** `git diff --name-only 9c201475 118fd9c2` lists four `.md` files, all under the round directory (I4, I5).
**Reviewer.** I reviewed the preregistration earlier; I did not write the assessment. I worked read-only and fetched nothing.
## Verdict: **ACCEPT WITH CHANGES**. The outcome (N) stands.
- Every J3 failure is supported once the record is corrected. I found no pass that the rule, as written, would award and the assessment missed.
- The Block A algebra is correct.
- The controls are green for the right reasons.
- The outcome is generated from |J₁₋₅| as preregistered.
Four should-fix findings correct the record without changing any set.
**R1. The C3 corpus search missed a route.** That route is the corpus's relabelling notion of gauge, which bears on H-passive and on E3. With those sources added, E3's import and H-passive should be classified **mixed, with an insufficient independent component**, not "none found". The verdict, J3 not held, is unchanged.
**R2. [L1](b) is applied asymmetrically, and [L2](b) states T1's content.** The assessment credits [L1](b) as motivation for E1's offset law and refuses it for E3. And [L2](b), as cited, states that no non-singlet constant appears, which is T1's content.
**R3. The SM:493 classification needs grounding in C2's own wording.**
**R4. E1's D1 entry omits a tension with amplitude-scale relabelling.**
I also rule on the author's sensitivities. **(1)** H-passive cannot enter through [L1](b), and its corpus route is mixed and insufficient, so E3 stays out of J₁₋₅ and J_c. **(2)** E1's J3 failure is robust.
***
## 1. Block-by-block check against the rule
| Block | Check | Result |
|---|---|---|
| A1 | E1 case analysis (−1; odd units fix q/2; transvection I + E_lk; the lift); E1′; E2 identity through additivity and g_j⁻¹(0) = 0, with induced law b_i ↦ g_i b_i; E3 identity | **correct**; re-derived by hand. Matches N9 and the H5 line |
| A2 | E1: G_0 as the commutant of generic block-scalar M. E1′ and E3: G_v under H-b. E2: ∩ Stab(a_ij) ⊆ Stab(b_i), with equality iff every a_ij ∈ V_1, and a smaller group for zero-sum splits outside V_1. (A-aff) unrealized | **correct**. The inclusion for E2 holds because Σ_j a_ij = b_i |
| A3 | Local class read from each definition; no promotion | **correct**; within c.6719886996's boundary (I10) |
| A4 | E2 and E3 induce the same law; E1 is E3 with the trivial law; E1 and E3 coincide on Fix(AddAut V); E3 embeds into E2 | **correct** |
| B1 | Mandatory offset-law rows; E1′'s class | **correct** as rows. Their classification is affected by R1 and R2 |
| B2 | The class role, "containment for an identity in which nothing needs preserving; not the manuscripts' group" | **sourced**: BackgroundIndependence.lean:30, :127–129; A6Instantiation.lean:70, :408–410 ("Reporting the general statement as a `U(6)` theorem … is a defect"). E1 constrains an untransported datum, so it is outside the role. E2's `gaugeLink` on affine maps and E3's `siteAct` on b are outside by patterns 2 and 3. The test is symmetric across the three |
| C | See R1–R3 | three classification corrections; no verdict changes |
| D | E1, E1′, E2, E3 graded tension; no inconsistency. The pre-graded D1 sentences are out of scope | **correct**, except R4 (an omitted tension for E1) |
| J table | J1, J2, J4, J6 entries | **correct**. J6: E2 is "not evaluable within the authorized scope" (A1 §4); E1 and E3 are not held, as the baseline is |
| Outcome | J₁₋₅ = J₁₋₄ = J₁₋₆ = J_c = ∅ gives (N), conditional on amplitude-scale gauge; the count with [L]-only passes excluded is 0 | **generated correctly** from the rule (I9, I17) |
## 2. Cited lines at `9c201475`
All cited lines resolve and say what the assessment reports. I read each one:
- **Substratum:** :82, :98, :102, :104, :163, :270, :272, :274.
- **SM:** :96, :104, :114, :116–118, :240, :342, :376, :382, :493, :523, :681, :954, and the "spurion" hits at :1082, :1312 and :1410. "Tadpole" first occurs at :756.
- **Main:** :726 item (xii).
- **Book:** `book/ch02-substratum.md:86`, `book/glossary.md:13`, `book/ch05-gauge-structure.md:137`.
- **Lean:** BackgroundIndependence.lean :30, :87–91, :104, :118, :121–123, :127–129, :161; A6Instantiation.lean :70, :147, :408, :455.
One reading is the assessment's own: SM:681 calls the gauge field "the state-dependent coupling matrix M of §3.1", and §3.1 contains both SM:104 and A6 (SM:114). The table's statement that SM:681 concerns only the state-dependent-graph principle is a reading, and should be marked as one (nit).
## 3. Corpus search (§A.19): my own search
I searched `papers/*.md` and `book/*.md` at the pin for:
- relabel, conjugat, passive, frame, background field, external source, source term, spurion;
- affine connection / gauge / group / link / holonomy, torsion, Poincaré gauge, teleparallel, translation gauge, inhomogeneous transformation;
- descriptive redundancy, master principle, indistinguishable transformations are gauge.
I then read the A6 sources and the hits.
**Affine links (E2).** No corpus or remembered-literature motivation exists for affine link data under a *linear* structure group.
- The corpus's links are V⊗V* (SM:523), and the constant sits in the site update (SM:240, Substratum:274).
- The only "torsion" hits (SM:302, book/ch05:95) concern additive 2-torsion and center terms of the fermionic description. They are not offsets.
- Affine-connection literature ([L4], and gauge theories of the Poincaré or affine group) gauges translations as well, so it describes an Aff(V) class, which is outside the candidate set.
The assessment's "none found" for E2 is confirmed.
**Fixed or transported constants (E1, E3).** The assessment's search missed these sources:
| Location | Content | Bearing |
|---|---|---|
| Substratum:270 | Amplitude-scale gauge: "These affine relabellings are exactly the site-wise relabellings that preserve … ω(k) …, so amplitude-scale gauge is one instance of the framework's master principle that *observationally indistinguishable transformations are gauge*" | A corpus principle under which gauge transformations are relabellings. Under a relabelling, a rule's constant is re-expressed by conjugation: b ↦ λb for the global unit rescaling λ. That is the E2/E3 law on that subgroup |
| Substratum:163 | "the field-value-scale freedom — the additive-automorphism relabellings of the alphabet" (K = 6 context) | The same freedom in the internal-index setting. The assessment itself notes that this "acts on the field and offset together" |
| BackgroundIndependence.lean:26–30 | "The internal index enters **only through the alphabet** … `V := K → ZMod q`" | Contradicts §1's dismissal of SM:96 and Substratum:270 as "the alphabet's relabellings, not … internal-index transformations". For the K-component alphabet, the alphabet's additive automorphisms *are* A6's class |
| Substratum:98 | A4 "up to gauge", "with gauge acting by site-wise bijections of each site's (previous, current) pair" | A site-dependent gauge in the corpus that acts on the rule by conjugation |
| Methodology:463 | "Gauge freedom is descriptive redundancy … constituted by the observer's inability to tell the representatives apart" | States the criterion for gauge status: observational indistinguishability |
| Substratum:272, and Theorem 24's generators (Substratum:251–262) | State relabelling in 𝒢_sub "relabels hidden states only" | The corpus's conjugation gauge does not cover visible data |
| Substratum:102 / book ch02:86 | "not the stronger fixed-background condition that the same transformations leave the dynamics invariant with the coupling held fixed" | The corpus's reason for transporting data rather than holding them fixed. A6Instantiation.lean:359–365 ties that reason to "exactly the site-dependent transformations the gauge reading needs" |
The search-result sentence "No location at the pin states a transformation law for a site offset under A6" remains literally true. But the C3 record must list these sources and classify what they support (R1).
## 4. Findings
### Should-fix
**R1. E3's offset law and H-passive should be classified "mixed, independent component insufficient", not "none found".** The sources in §3 give one independent component and one target-adjacent component.
- **Independent component.** Amplitude-scale gauge treats the rescaling λ, for a global unit λ, as a relabelling. Its motivation is operational (Substratum:270) and is the principle on which the whole outcome is already conditional. Under conjugation it transforms a rule constant as the field. That is the E2/E3 law, but **only on the global scalar subgroup** of A6's class.
- **Extending to A6's site-dependent class.** Extending the law to the whole class requires A6's transformations to be relabellings: gauge in the Methodology:463 and Substratum:270 sense. Three obstacles stand in the way:
- Gauge status needs observational indistinguishability. At Main's absolute interface (Q1), visible site-wise relabellings are distinguishable: core file §3.3.8 item 6, and Proposition 2.6(b), which is [D] there.
- 𝒢_sub's conjugation gauge is hidden-only (Substratum:272).
- The #1049 safeguard requires the gauge status of site-dependent transformations to be established separately.
- **Target-adjacent component.** What remains is the identification of A6's transformations as gauge at SM:118, Substratum:163 and Main:726 (xii). Those are T2- and O5-directed. So is Substratum:102's reason for transport over a fixed background (A6Instantiation.lean:362).
So the import is mixed, and its independent component does not motivate it on its own for the class (`DESIGN.md` J3). E3's J3 is still not held. H-passive cannot place E3 in J_c, because A1 F10 admits only independent hypotheses or mixed hypotheses with a sufficient independent component.
**Required.**
- Add the §3 sources to the C3 record.
- Correct §1's alphabet-versus-internal-index dismissal, citing BackgroundIndependence.lean:26–30.
- Reclassify E3's B1/B2 imports and H-passive as mixed (insufficient).
- Restate §8 from "no independent physical motivation was located for any of the three laws" to: "none located that suffices on its own for the class. Amplitude-scale relabelling supports the E2/E3 law on the global scalar subgroup only."
**R2. [L1](b) is applied asymmetrically, and [L2](b) is target-adjacent.**
- **The asymmetry.**
- §4 credits "[L2](b) and [L1](b)" as an independent motivation for E1's B1 ("b not transformed").
- It refuses [L1](b) for E3, reading it as excluding "a physically significant fixed direction rather than transport[ing] one".
- One source cannot be read in E1's favour and against E3. As the assessment states it, [L1](b) (frame orientation has no physical significance) is a premise about frames for dynamical fields. It is neutral between "a non-dynamical constant is held fixed" and "it is re-expressed under a frame change". It motivates neither law, and applying it to a rule constant is a step the assessor composes.
- **[L2](b) is target-adjacent.** As cited, [L2](b) reads: "no term linear in a non-singlet site field appears". It states, in the literature's setting, that non-singlet constants are absent. Judged on its own (A1 C2), that is T1's content, so it is target-adjacent.
**Required.**
- Reclassify E1's B1 as target-adjacent, or as mixed (insufficient).
- Remove [L1](b) from both E1 and E3 as a motivation for an offset law, or credit it for both.
- Note that E1's J5 entry ("[L2](b) distinguishes E1 from E3") then rests on a target-adjacent item.
- Update §8's count bullet on E1's B1.
**Effect.** None on any set. E1 already fails J3 on its B2 import, and would now fail on B1 as well. If [L1](b) were instead credited to both, E1 would still fail on B2. E3 would then pass J3 only on [L] alone, and only through a reading C1 does not license (see the ruling on (1)).
**R3. Ground SM:493's classification in C2's text.**
- "Each located physical class is specified only as part of the T2 construction" is not one of C2's criteria as worded.
- SM:493 ("The substratum dynamics is locally U(6) invariant") carries no stated motivation of its own:
- its scalar-M basis (SM:376, "Remark below") is withdrawn at SM:382;
- its stabilizer use rests on H-cust (SM:342);
- its local character is the A6 promotion itself (Substratum:163, "promotes … to local gauge invariance").
**Required.** Classify it **none found**, after C3, with that context. Record that adopting local U(6) as A6's physical class would itself be an O5-type promotion, which c.6719886996's boundary excludes. G_0 is T2 and remains target-adjacent. The verdict is unchanged.
**R4. E1's D1 entry omits a tension.**
- For the constant scalar elements λ of A6's class, the corpus's amplitude-scale relabelling transforms a rule constant (b ↦ λb by conjugation; Substratum:270, :163).
- E1 holds b fixed under the same elements, and so requires λb = b.
- These are two principles, not a contradiction, so the grade is **tension**.
**Required.** Add this to E1's D1 cell. It has no J4 effect.
### Nits
- **n1.** Add relabel, conjugat, fixed-background, frame, background and "gauge freedom" to §1's term list, with the hits in §3 above.
- **n2.** §10 says of [L1]–[L4]: "No outcome entry rests on them." The outcome (N) does not. C-POS's J3 and the E1-B1 entry do. Say so.
- **n3.** Mark the SM:681 row as a reading (§2 above).
- **n4.** I could not verify the attribution and wording of the review record c.6720120379, because I fetched nothing.
***
## 5. Rulings on the author's sensitivities
**(1) E3 and H-passive.** Under the preregistered C1 and C2, [L1](b) does not supply a passage that motivates transporting a non-dynamical rule constant. The claim concerns the insignificance of frame orientation for dynamical fields. Reading it as "every internal-index-valued datum of the rule transforms" is the assessor's own extension. That is the kind of composed motivation A2 G1 excludes from J5, and it is not "the passage that motivates" the import under C1.
The corpus route to H-passive does exist (R1): relabelling gauge. But it is **mixed with an insufficient independent component**. The independent part reaches only the global scalar subgroup. Extending it to A6's site-dependent class needs observational indistinguishability, which Main's absolute interface denies for visible relabellings, or else T2- and O5-directed identifications.
So H-passive is correctly *rejected*, but under the wrong label. E3 enters neither J₁₋₅ nor J_c. The §9 scenario, (S) with E3, would require crediting [L1](b), and under R2 that credit would also go to E1. **(N) stands.**
**(2) E1's class role and SM:493.**
- The formal role of AddAut V is source-stated (B2 above), and E1's use of it to constrain an untransported datum lies outside that role.
- SM:493's local U(6) has no independent stated motivation (R3), and taking it as A6's physical class would itself be an O5 promotion.
- Even granting a physical class, the motivation for holding b fixed would be [L2](b), which is target-adjacent (R2).
E1's J3 is correctly not held, on two independent grounds once R2 is applied.
**(3) The [L] items.** The labels and handling meet A2 G4 and I18: the corpus is searched first; each item names its work and claim; "[L] only" passes are labelled; the count excluding them is 0. As far as I recall, the citations are accurate:
- Yang–Mills, *Phys. Rev.* 96, 191 (1954);
- Wilson, *Phys. Rev. D* 10, 2445 (1974);
- Georgi, *Weak Interactions and Modern Particle Theory* (1984), on spurions;
- Kobayashi–Nomizu I (1963), ch. III, linear and affine connections.
I did not re-read them either. No set membership rests on them.
## 6. Pressure test (§A.31), both directions
**Manufactured failures?**
- E1's B2 rests on a role that the kernel's own docstrings state.
- E2's "none found" is confirmed by my search.
- E3's failure survives the strongest corpus route found (R1).
No J3 failure is manufactured. Two labels are wrong (R1, R2), and one grounding is loose (R3).
**Missed passes?**
- The only candidate route is E3 by relabelling.
- It fails J3's sufficiency clause for the class.
- It would at most reach J_c through a hypothesis that is itself mixed and insufficient, which F10 bars.
No pass is missed.
**C-TI.** No verdict cites an A1 or A2 entry as its reason, and E1's failure does not rest on b = 0. R2's asymmetry favoured E1's B1 (the T1-producing law) and was not decisive. Correcting it removes a T1-leaning credit and does not add a T1 penalty.
## 7. Controls
- **C-LIN.** Passes for E1, E1′, E2, E3, E★ and E☆, and for E☆-law on the class ι → G_0. E-inv fails on the transport clause, as required. Not vacuous (I7).
- **C-POS.** The observed profile matches the prediction: J1, J2, J4 and J5 held; J3 held through a mixed classification, labelled "[L] only"; J6 not held. It is reported, not gated (I16).
- **C-CAL.** E4 on the whole rule is classified independent, correctly (Substratum:82; SM:238). It is a statement about the whole rule, it presupposes no T, and the functional test does not apply.
- **C-TI.** Passes (§6).
- **E★.** Rejected through J3 by its stated T2 reason and by the functional test on the identification. Also not held under J4 through D3 and D2. The right reason.
- **E☆.** Rejected through J3 by the functional test. The right reason.
- **E☆-law.** Rejected through J3, because ρ is outside exemptions (i)–(iii) under K2. Its A1 constraint, (z − 1)b_{i,1} = 0, is recorded and not scored. The right reason.
- **Void conditions.** None fired, correctly.
**Invariants.**
- I1, I2, I4 and I5 hold, as measured above.
- I13 (register): the only all-caps tokens are file names, status labels and quoted verdicts. There are no hits for the §A.32 or §A.33 phrase families.
**Not checked.** I fetched nothing from GitHub, re-read no [L] item, and ran no code or Lean.
***
***
# Confirmation at 25384b13
**Object.** `git diff 118fd9c2 25384b13`.
- `25384b13526dfa23909bbd63a119508091f467c7` has the single parent `118fd9c2`.
- The commit changes ASSESSMENT.md only (+136/−66).
- `git diff --name-only ab0e1dac 25384b13` lists only ASSESSMENT.md, so **DESIGN.md, A1 and A2 are untouched** (I2).
- Checked read-only, with no fetching.
## Verdict: **ACCEPT**. The outcome (N) stands, and the Q3 results review is closed.
| Item | Status | Check |
|---|---|---|
| R1 | **resolved** | The relabelling-gauge table carries all seven sources of my §3, each with the bearing I gave it: Substratum:270, :163, BackgroundIndependence.lean:26–30, Substratum:98, Methodology:463, Substratum:272/251–262, and Substratum:102/ch02:86/A6Instantiation.lean:359–365. The alphabet-versus-internal-index dismissal is withdrawn with the kernel citation. E3's import and H-passive are "mixed, with an insufficient independent component", for my reason: the independent component, amplitude-scale relabelling (b ↦ λb), reaches only the global scalar subgroup. Extending it needs gauge status, and the obstacles are listed: observational distinguishability at the absolute interface, 𝒢_sub being hidden-only, and the #1049 safeguard. The remaining route is T2/O5-directed. H-passive is barred from J_c under F10, with the reason. §1's search result and §8 are restated to match |
| R2 | **resolved, symmetric** | [L1](b) is neutral and credited to neither law: at its definition (§1) and in E1's and E3's C entries. [L2](b) is target-adjacent. E1's B1 is target-adjacent with no independent component. E1's J5 entry notes that [L2](b) is target-adjacent. The C-TI note records that the correction removed a T1-leaning credit and added no T1 penalty. The §8 count bullet is updated |
| R3 | **resolved** | SM:493 is none found after C3, with its context: the SM:382 withdrawal, H-cust (SM:342) and the A6 promotion (Substratum:163). The O5-type note is present. G_0 is target-adjacent. H-active is updated to match |
| R4 | **resolved** | The amplitude-scale tension is added to E1's D1 cell, graded tension, not a contradiction. No J4 effect |
| n1 | **resolved** | Search terms are added, with their hits in the new table |
| n2 | **resolved** | §9.3 and §10 now state that C-POS's J3 and E1's B1 rest on [L], and that the outcome and the sets do not |
| n3 | **resolved** | The SM:681 row is marked as the assessment's reading and is not used as a motivation |
| n4 | **resolved as attributed** | The verification of c.6720120379 is attributed to the coordinating session. I did not verify it myself, since I fetched nothing |
| Rulings | **recorded faithfully** | §9 states the three rulings as I gave them |
**No set changed.**
- The per-candidate table is unchanged: J3 is not held for E1, E1′, E2 and E3.
- J5 and J6 are as before.
- J₁₋₅ = J₁₋₄ = J₁₋₆ = J_c = ∅.
- The count with [L]-only passes excluded is 0.
- The outcome remains (N), conditional on amplitude-scale gauge.
**Nothing new is wrong.** One optional nit follows.
- The new E1 entries now fail on two grounds, B1 and B2, as my ruling (2) stated.
- No new verdict cites an A1 or A2 entry as its reason (C-TI).
- The register scan of the added lines found no all-caps emphasis.
**Optional nit.** A few added sentences narrate the file's own revisions:
- "The earlier entry here dismissed … That dismissal is withdrawn" (§1);
- "At `118fd9c2` the writer noted …" (§9);
- "It is corrected here" (C-TI).
I13 adopts the §A.33 history-phrase family for this round, so a strict reading would state these timelessly and leave the revision history in §10 and in the commit. The programme's own records carry "Revision" notes, and this is a verification record, not paper prose, so this is not blocking.Generated by Claude Code
Owner
Author
Merge record: #1202 (owner-approved, chat, 2026-11-08)The owner (amaybaum) approved this in chat with the coordinating session on 2026-11-08:
Merged as Checks:
Scope of the conclusion. Outcome (N): none of E1–E3 has an established independent justification as the extension of A6 to affine offsets within the reviewed scope. This is not a proof that no valid extension exists. No manuscript or status changed. Main's push CI is running and will be reported here. Generated by Claude Code |
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 paper record. Independently reviewed: outcome (N). CI and the owner's integration decision are still pending.
25384b13526dfa23909bbd63a119508091f467c7, from main9c201475.verification/programmes/substratum/a5-linear-affine-20261104/q3-a6-offsets-20261108/:DESIGN.md: the preregistration (f71bdc87).amendments/A1-prereg-review.md(d7b6d32b) andamendments/A2-rereview.md(ab0e1dac): amendments made before the assessment.ASSESSMENT.md: the result.Outcome: (N)
None of E1, E2 or E3 is independently justified as the extension of A6 to affine offsets, on the record at
9c201475. The outcome is conditional on amplitude-scale gauge (Substratum:272). All four sets are empty: J₁₋₅, J₁₋₄, J₁₋₆ and J_c.Review record (independent model reviewer; texts posted verbatim)
f71bdc87;d7b6d32b;ab0e1dac.118fd9c2;25384b13.Not authorized: computation; any change to A5 or to the manuscripts; adoption of any extension; O5; the §7 computation; the D16/R10/D3 record changes; merge. Integration is a separate owner decision.
🤖 Generated with Claude Code
https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb