diff --git a/research/p104-sharp-block-hall-dimension/PROOF.md b/research/p104-sharp-block-hall-dimension/PROOF.md
new file mode 100644
index 0000000000..f8aeb29ca6
--- /dev/null
+++ b/research/p104-sharp-block-hall-dimension/PROOF.md
@@ -0,0 +1,315 @@
+# Proof: the two fourteen-port subsystems have different sharp dimensions
+
+All port numbers denote zero-based positions in the authenticated P104 source
+array identified in [README.md](README.md). The zero relation is
+
+\[
+Z(v,w)\iff v\ne w\quad\text{and}\quad
+\operatorname{popcount}(p_v\mathbin{\&}p_w)\equiv0\pmod2.
+\]
+
+Throughout, `k` is a positive integer, `F` is an arbitrary field, and
+`U_v,W_v` are `k × d` matrices over `F` satisfying the stated zero relation
+and invertible diagonal pairings. A smaller subsystem imposes only the
+constraints among its retained ports.
+
+## 1. Rank axioms from asymmetric labels
+
+Put `V_v=im(U_v^T)` and
+
+\[
+f(A)=\dim_F\!\left(\sum_{v\in A}V_v\right).
+\]
+
+The diagonal invertibility gives `dim(V_v)=k`: if `U_v^T x=0`, then
+`W_v U_v^T x=0`, whence `x=0`. Also `f(empty)=0`, `f(A)<=d`, and `f` is
+monotone. The dimension formula, together with
+`span(V_{A intersection B})` contained in
+`span(V_A) intersection span(V_B)`, gives submodularity:
+
+\[
+f(A)+f(B)\ge f(A\cup B)+f(A\cap B).
+\]
+
+If `v` is forced zero to every member of `A`, then `W_v` annihilates
+`span(V_A)` and is injective on `V_v`. Their intersection is therefore zero,
+so
+
+\[
+f(A\cup\{v\})-f(A)=k. \tag{Z}
+\]
+
+This uses no symmetry assumption. Every subsequent inequality concerns
+integer dimensions, so the rational certificate coefficients do not require
+division by two in the field.
+
+## 2. Original subsystem: lower bound `ceil(17k/2)`
+
+Define
+
+\[
+I=\{74,81,86,91\},\qquad
+S=\{62,63,69,99,67,68,95,100,101\}.
+\]
+
+The original fourteen-port set in #6846 is `R0=I union S union {57}`.
+Every member of `I` is forced zero to every member of `S` and to the other
+members of `I`. Thus repeated application of (Z) gives
+`f(I union S)=4k+f(S)`. Thirteen ports already suffice for the lower bound.
+
+To prove `2f(S)>=9k`, set
+
+~~~text
+A = {62,69,99,68,100}
+B = {62,99,67,95,100}
+C = A union B
+E = {69,67,100}
+F = {62,100}
+Q = {69,99,67,68,100}
+T = {62,69,67}
+~~~
+
+The following finite premises are checked directly against the pinned ports:
+`63` is forced zero to `A`; `101` to `B`; `99` to `F`; `95` to `Q`;
+`68` to `E`; and the three members of `T` are pairwise forced zero.
+The relevant set identities are
+
+\[
+A\cap B=F\cup\{99\},\quad E\cap F=\{100\},\quad
+Q\cup\{95\}\subseteq C,\quad E\cup\{68\}\subseteq Q,
+\quad T\subseteq E\cup F.
+\]
+
+Consequently,
+
+\[
+\begin{aligned}
+2f(S)
+&\ge f(A)+f(B)+2k &&\text{by (Z) and monotonicity}\\
+&\ge f(C)+f(F)+3k &&\text{by submodularity and (Z) for 99}\\
+&\ge f(Q)+f(F)+4k &&\text{by (Z) for 95 and monotonicity}\\
+&\ge f(E)+f(F)+5k &&\text{by (Z) for 68 and monotonicity}\\
+&\ge f(E\cup F)+f(\{100\})+5k &&\text{by submodularity}\\
+&\ge 3k+k+5k=9k. &&\text{since T is pairwise forced zero}
+\end{aligned}
+\]
+
+Therefore
+
+\[
+d\ge f(I\cup S)=4k+f(S)\ge\frac{17k}{2}.
+\]
+
+Since `d` is an integer, `d>=ceil(17k/2)`. The verifier independently expands
+the displayed argument into 17 elementary axiom rows whose exact sum is
+`2f(S)-9k>=0`, including every monotone inclusion and the empty-set identity.
+
+## 3. Original subsystem: matching upper bound for every field and block size
+
+A coordinate group assigns one ambient standard basis coordinate to every
+port listed in that group. Let the rows of `U_v=W_v` be the distinct standard
+coordinates assigned to port `v`. If every port receives `k` coordinates and
+every forced-zero pair receives disjoint coordinate sets, the diagonal
+pairing is `I_k` and all required off-diagonal products vanish over every
+field. The ordering of the rows within a port can be fixed by increasing
+coordinate index.
+
+For `k=2,d=17`, use two coordinates for each group in the first row and one
+for each group in the second:
+
+| Multiplicity | Coordinate groups |
+|---|---|
+| 2 | `{74}`, `{81}`, `{86}`, `{91,57}`, `{99,67}`, `{69,100}` |
+| 1 | `{62,68}`, `{62,95}`, `{63,95}`, `{63,101}`, `{68,101}` |
+
+There are `12+5=17` coordinates. Every original port receives two distinct
+coordinates. Every two-port group is an allowed pair, as checked against the
+source. This proves the `k=2,d=17` upper bound without arithmetic cancellation
+or characteristic restrictions.
+
+For `k=1,d=9`, use one coordinate for each group
+
+~~~text
+{74}, {81}, {86}, {91,57}, {99,67}, {69,100}, {62,68}, {63,95}, {101}.
+~~~
+
+For `k=2q+r`, `r in {0,1}`, take the direct sum of `q` copies of the first
+construction and `r` copies of the second. Its inner dimension is
+
+\[
+17q+9r=\left\lceil\frac{17k}{2}\right\rceil.
+\]
+
+Together with Section 2 this proves exactness for the original fourteen
+ports. Restricting the same constructions proves exactness for the
+thirteen-port lower-bound subset `I union S` as well. The nine-core `S`
+itself has exact minimum `ceil(9k/2)`, by deleting the four isolated coordinate
+blocks (each of dimension `k`) from the construction.
+
+## 4. Replacing port 57 by 61: the Petersen core
+
+Let
+
+\[
+P=S\cup\{61\}=\{61,62,63,67,68,69,95,99,100,101\}.
+\]
+
+All four members of `I` are forced zero to every member of `P`; in fact `P`
+is their complete common forced-zero neighborhood among all 104 ports.
+The graph of allowed distinct pairs on `P` is the Petersen graph. An explicit
+isomorphism to its outer-pentagon / inner-pentagram presentation is
+
+~~~text
+outer = [61,69,100,62,95]
+inner = [99,101,67,68,63].
+~~~
+
+Its edges are exactly `outer[i]--outer[i+1]`, `outer[i]--inner[i]`, and
+`inner[i]--inner[i+2]`, with indices modulo five. The verifier compares the
+complete unordered edge sets; degree counts alone are not used to identify
+the graph. The following rank argument is checked directly against the
+source relation and does not rely on recognizing the graph name.
+
+### Exact all-field certificate for `f(P)>=5k`
+
+The file [petersen-dual.json](petersen-dual.json) contains 43 rows. The ordered
+vertex list is `P` in the ascending order displayed above. For a subset mask
+`s`, its set is `{P[i] : the i-th bit of s is 1}`. The row meanings are:
+
+| Descriptor | Left side | Right side | Type |
+|---|---|---|---|
+| `["mono",s,i]` | `f(s)-f(s+i)` | `0` | `<=` |
+| `["submod",s,i,j]` | `f(s)+f(s+i+j)-f(s+i)-f(s+j)` | `0` | `<=` |
+| `["zero",s,i]` | `f(s+i)-f(s)` | `k` | `=` |
+| `["empty"]` | `f(empty)` | `0` | `=` |
+
+Here `s+i` denotes adjoining `P[i]`, not integer addition; each named vertex
+is required to lie outside `s`. Every `zero` row has all its required
+forced-zero contacts checked. All 26 inequality multipliers are `-1/2`, so
+each multiplied inequality has the correct `>=` orientation. The 16
+zero-additivity rows have signed half-integer multipliers; equalities allow
+either sign. The remaining row is the empty-set equality.
+
+Adding the rows gives **exactly**
+
+\[
+f(P)\ge5k.
+\]
+
+More explicitly, the coefficient of `f(P)` is `1`; the coefficients of all
+other subset-rank variables are zero; and the weighted sum of the
+zero-additivity right sides is `5k`. Multiplying the entire certificate by
+two yields integer coefficients. `verify.py` reconstructs the rows as
+frozensets of actual port IDs and checks this identity with rational
+arithmetic. The separately written `audit_petersen.py` reconstructs the rows
+using bitmask variables and a different coefficient accumulator. Neither
+uses numerical tolerances or trusts the reported LP objective.
+
+This finite exact axiom combination is a proof for every field and every
+positive integer `k`, because Section 1 proves each axiom for every such
+label system. A numerical linear program was used only to discover it.
+
+It follows that the replacement subsystem
+`R1=I union P=(R0 minus {57}) union {61}` satisfies
+
+\[
+d\ge f(I\cup P)=4k+f(P)\ge9k.
+\]
+
+The replacement subsystem attains `9k` over every field. Assign one block of
+`k` standard coordinates to each singleton in `I` and to each matching edge
+
+~~~text
+{61,69}, {62,95}, {63,101}, {67,100}, {68,99}.
+~~~
+
+These are five allowed disjoint edges covering all ten core ports. Every
+port receives exactly one coordinate block, with `U_v=W_v` its standard
+basis rows. This proves exactness of `9k` on `R1`, and of `5k` on `P`.
+
+## 5. Consequence for the full mask and its limits
+
+Any realization of all 104 ports restricts to `R1`, hence has `d>=9k` over
+every field. In every characteristic-two field, interpreting each original
+nine-bit port as a vector gives a scalar realization: odd weight makes the
+diagonal one, and even overlap makes each forced-zero product zero. Tensoring
+with `I_k` attains `9k`. Thus the full-mask minimum is exactly `9k` in
+characteristic two.
+
+Over other characteristics, a binary dot product that is zero modulo two
+need not be zero in the field. The argument therefore supplies only the
+full-mask lower bound there. It supplies no necessity theorem for the label
+pattern in a legal multiplication circuit and no reduction in complete
+supplier cost. **No new κ.**
+
+The general Petersen lower bound and four-isolate construction precede this
+work: see Thiago's #1744 and its credit to Blasiak, Kleinberg and Lubetzky.
+The source-specific advance is the explicit P104 transfer, the sharp
+original-subsystem contrast, and the exact closure of the open block
+interval in DreamingOfClouds' #6846.
+
+## 6. Exact nonlinear binary broadcast corollary
+
+Use the same allowed-pair graph as a side-information graph. Each vertex `v`
+has an independent uniform `k`-bit message `X_v`; receiver `v` knows the
+messages at its allowed neighbors and must recover `X_v` without error.
+Let `B` be any deterministic fixed-length binary broadcast, permitting
+arbitrary nonlinear encoding and decoding. Write `V` for the vertex set and
+define, with entropy measured in bits,
+
+\[
+r(S)=H(B\mid X_{V\setminus S}).
+\]
+
+This function satisfies exactly the axioms used in both preceding proofs.
+Deterministic encoding gives `r(empty)=0`. Removing conditioning variables
+proves monotonicity. Moreover
+
+\[
+r(S)=H(B,X_{V\setminus S})-k|V\setminus S|.
+\]
+
+Entropy submodularity, complementation of the index sets, and subtraction of
+the displayed modular function prove submodularity of `r`. If `v` is forced
+zero to every member of `S`, all neighbors of `v` belong to
+`Z=V\setminus(S\cup\{v\})`. Independence and zero-error decoding give
+
+\[
+\begin{aligned}
+r(S\cup\{v\})-r(S)
+ &=I(B;X_v\mid X_Z)\\
+ &=H(X_v\mid X_Z)-H(X_v\mid B,X_Z)=k.
+\end{aligned}
+\]
+
+Thus the same 17-row short proof and 43-row certificate, already checked
+exactly, are also entropy inequalities. In the full 104-port problem the
+certificates bound `r(I union P)`, which is at most `r(V)=H(B)` by
+monotonicity. Since an `L`-bit fixed-length broadcast has `H(B)<=L`, they imply
+
+| Side-information graph | Minimum fixed binary broadcast length |
+|---|---|
+| Original fourteen ports `R0` | `ceil(17k/2)` |
+| Replacement fourteen ports `R1` | `9k` |
+| Complete 104-port graph | `9k` |
+
+Here the lower bounds apply to nonlinear encoders. The upper bounds are
+explicit linear codes. For each coordinate in a subsystem witness, transmit
+the XOR of the message bits assigned to that coordinate. Every other port
+sharing the coordinate is an allowed neighbor, so a receiver subtracts the
+known bits and recovers its own bit. The verified coordinate assignments give
+the stated lengths for every `k`, using direct sums for the original odd-width
+case.
+
+For the full graph, broadcast the nine `k`-bit blocks
+`B_a = XOR_{v: ports[v]_a=1} X_v`. Receiver `v` XORs those blocks selected by
+its port vector. Its own coefficient is one; every other nonzero coefficient
+is on an allowed neighbor, so it can subtract those known messages. The
+existing full binary Gram check verifies all these coefficients.
+
+This is a source-specific index-coding corollary of the same certificate,
+following the established entropy/Petersen method in #1744. The general
+nonlinear Petersen result is credited there to Blasiak, Kleinberg and Lubetzky.
+No new universal entropy inequality is claimed. This fixed-length zero-error
+broadcast model is an explicit assumption and is not a physical reversible
+supplier or a paid multiplication algorithm.
diff --git a/research/p104-sharp-block-hall-dimension/README.md b/research/p104-sharp-block-hall-dimension/README.md
new file mode 100644
index 0000000000..3a0e9f88a2
--- /dev/null
+++ b/research/p104-sharp-block-hall-dimension/README.md
@@ -0,0 +1,212 @@
+# Sharp block dimensions for the P104 Hall mask
+
+**No new κ.** Under the exact asymmetric label-pattern hypothesis of
+CrocSwap/integer-mult-bounds#6846, the complete P104 mask requires inner
+dimension **at least `9k` over every field**, for every positive integer block
+size `k`. This closes the interval `8k < d < 9k` left open there. The proof
+transfers the established four-isolates-plus-Petersen obstruction to an
+authenticated P104 subconfiguration; it does not introduce a new general
+Petersen rank theorem.
+
+The predecessor's original fourteen ports behave differently: their exact
+minimum is **`ceil(17k/2)` over every field**. In particular, `k=2,d=17` is
+possible on that subsystem. Replacing just port `57` by port `61` produces
+another fourteen-port subsystem whose exact minimum is `9k`. The distinction
+explains both why the original Hall witness cannot exclude the whole block
+interval and why the full source mask nevertheless does.
+
+| Object, with the zero convention below | Proven minimum / lower bound |
+|---|---|
+| Original fourteen ports from #6846 | Exact `ceil(17k/2)` over every field |
+| Same selection with `57` replaced by `61` | Exact `9k` over every field |
+| All 104 source ports | At least `9k` over every field |
+| All 104 source ports in characteristic two | Exact `9k` |
+
+No dimension-`9k` upper bound for the full mask in other characteristics is
+asserted. No supplier circuit or complete paid invoice is constructed.
+
+The same exact certificates also give an index-coding corollary: even with
+arbitrary nonlinear deterministic encoding, the minimum fixed-length binary
+broadcast for independent `k`-bit messages is `ceil(17k/2)` on the original
+subsystem and `9k` on the replacement subsystem and full 104-port graph.
+Section 6 of [PROOF.md](PROOF.md) supplies the entropy reduction and explicit
+attaining parity broadcasts. This abstract side-information model does not
+establish a physical supplier or change κ.
+
+## Exact object and hypothesis
+
+The input is the unchanged
+[#5561 word](../p104-designer-toolkit-v2/words/5561.json.gz) at canonical base
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+Its compressed SHA256 is
+`b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44`;
+Git blob `c367d865a154ffd2ae0b6f6053469580a139f487`.
+The `ports` array contains 104 distinct odd-weight nine-bit integers. All
+indices below are zero-based array positions, not port integer values.
+
+For a field `F`, choose arbitrary `k × d` matrices `U_v,W_v` for each retained
+port. Require `W_v U_v^T` to be invertible and require
+`W_v U_w^T=0` whenever `v != w` and
+`popcount(ports[v] & ports[w])` is even. Both ordered products are constrained
+on a forced-zero pair; no symmetry or equality of `U` and `W` is assumed.
+Additional zeros are permitted.
+
+This is exactly the explicit pattern hypothesis in #6846. It is **not**
+established here for every legal multiplier, caller, frame change, or decoder.
+In particular, it must not be confused with the opposite parity convention
+used for the real-valued completion in
+[P104-LEMMAS.md](../p104-designer-toolkit-v2/P104-LEMMAS.md).
+
+## What is new relative to the archive
+
+DreamingOfClouds' #6846 proves impossibility at `d=8k` from
+`K={62,63,69,74,81,86,91,99}` and `O={57,67,68,95,100,101}`.
+Its second open question explicitly leaves intermediate block dimensions
+unsettled. The reviewed predecessor head is
+`01651795be9570c47977a73f9cf3e8eeb3fbe64a` in
+`DreamingOfClouds/integer-mult-bounds`; the scope here is that stated mask and
+question, not an unmerged circuit dependency.
+
+The relevant earlier archive result is Thiago's merged #1744,
+[research/p112-characteristic-two-minrank](../p112-characteristic-two-minrank/README.md),
+head `78033981ec296b545b3cb50435668fe98e764e65`. It already proves the same
+all-field `9k` obstruction on P111 and P112 by embedding four isolates and a
+Petersen graph, with an exact 113-term certificate in an augmented-rank
+formulation. It credits the known Petersen broadcast-rate theorem to
+[Blasiak, Kleinberg and Lubetzky, Fact 5.6(1)](https://www.cs.cornell.edu/~ablasiak/papers/bkl-beta.pdf).
+The present package connects that mechanism to the precise P104 question:
+
+- It authenticates a concrete P104 embedding using only fourteen source ports.
+- It proves the sharp `ceil(17k/2)` value of the predecessor's original
+  fourteen-port selection, including a `k=2,d=17` witness.
+- It gives a separate 43-row exact subspace-rank certificate for the Petersen
+  core and checks it with two separately written implementations.
+- It explicitly separates the full-mask lower bound, subsystem sharpness,
+  characteristic-two full-mask sharpness, and unproved supplier applicability.
+
+The smaller certificate is given for inspectability; its row count is not a
+performance comparison with the different formulation in #1744. No novelty is
+claimed for fractional Haemers representations, coordinate-cover upper
+bounds, the Petersen value, or the natural binary upper construction. See also
+[Bukh and Cox, *On a fractional version of Haemers' bound*, arXiv:1802.00476v2](https://arxiv.org/abs/1802.00476v2),
+Section 2, for the block-fitting framework.
+
+## Proof and exact witnesses
+
+[PROOF.md](PROOF.md) gives the linear-algebra argument and a short hand proof
+of the original subsystem's lower bound. For any admissible labels, let
+`f(A)` be the dimension of the sum of the row spaces of the matrices `U_v`
+for `v in A`. This is a monotone submodular rank function. If `v` is forced
+zero to every member of `A`, the invertible diagonal pairing implies the
+exact identity `f(A+v)=f(A)+k`. This elementary fact handles asymmetric labels
+and every characteristic.
+
+Four ports `I={74,81,86,91}` are isolated in the allowed-pair graph. Their
+common forced-zero neighborhood is exactly
+`P={61,62,63,67,68,69,95,99,100,101}`. The allowed-pair graph on `P` is the
+Petersen graph. The exact certificate establishes `f(P)>=5k`, hence
+`d>=f(P+I)>=9k`. The same four isolated ports combined with
+`S=P-{61}` give the original subsystem's `17k/2` lower bound. A two-coordinate
+assignment per port attains it at `k=2`, and direct sums give all block sizes.
+
+The universal statements follow from the displayed proof and exact axiom
+combination, not from finite searches. The numerical linear programs used to
+discover the certificate are absent from the trusted replay.
+
+## Reproduce and expected result
+
+From the repository root, with Python 3.12 and no external dependencies:
+
+```sh
+python3.12 scripts/research_package.py --package research/p104-sharp-block-hall-dimension
+```
+
+The registered replay runs both verifiers normally and with `-O`. Expected
+markers are `PASS_P104_SHARP_BLOCK_HALL_DIMENSION` and
+`PASS_P104_PETERSEN_EXACT_RANK_PROOF`, each twice. Direct standalone replay is
+`python3.12 -I -B research/p104-sharp-block-hall-dimension/verify.py`.
+
+The main verifier authenticates the source bytes and index convention,
+expands all 17 axiom rows of the short proof, regenerates all 43 Petersen
+certificate rows as sets of actual port IDs, checks their coefficient sum
+exactly, verifies an explicit Petersen isomorphism, checks all ordered
+required pairings of the coordinate witnesses for `k=1,...,12`, and computes
+all 10,816 entries of the binary full-mask Gram matrix. `audit_petersen.py`
+was separately written and checks the same Petersen certificate using an
+integer-mask coefficient accumulator. Neither implementation imports the
+other, a predecessor verifier, or a numerical optimizer.
+
+Ten main negative controls reject a source-byte mutation, a removed required
+zero, the reversed parity convention, a reversed inequality sign, a deleted
+inequality, a changed equality coefficient, a false zero premise, a corrupted
+upper witness, deletion of its seventeenth coordinate, and a singular
+diagonal. The separate audit has four coefficient/premise controls. All
+acceptance gates use explicit exceptions and remain active under `-O`.
+The finite block-size runs check implementations of the explicit witnesses;
+the direct-sum proof establishes all positive integer block sizes.
+
+## Scope, assumptions and completion status
+
+This is a completed rank-geometry side result, not a completed answer to the
+catalogue's supplier-budget question. The original catalogue card is retained
+in [TASK.json](TASK.json), with the scope change recorded. Exact live input and
+historical provenance pins are in [SOURCES.json](SOURCES.json). Reproduction
+commands and input-trigger declarations are in [VERIFY.json](VERIFY.json).
+The coordinated claim was local-only because the connected GitHub interface
+could not post to the current Discussion board; no reservation issue was
+created.
+
+The selected record at the base reports `κ=0.003125804`. This package leaves
+that record and its five framework assumptions untouched: `native_all_columns`,
+`owned_erasure`, `compiler`, `precision_tape`, and `analytic_recovery`. The
+rank proof itself uses none of those assumptions; applying it to a proposed
+supplier requires a separate proof that the supplier obeys the label pattern.
+No partial numerical improvement or optimistic invoice is promoted to a
+multiplication bound.
+
+## Open next questions
+
+1. **Applicability or paid relaxation.** For a particular legal caller, which
+   operations force exactly this zero pattern, and can a priced helper change
+   enough contacts to remove the Petersen witness? A useful first step is to
+   map the fourteen required contacts to that caller's explicit operations,
+   then price every altered boundary, restoration and ownership cost. An
+   abstract graph relaxation alone cannot improve the selected bound.
+2. **Full-mask upper bounds outside characteristic two.** What is the exact
+   block-rank parameter over a specified field such as the rationals or
+   complex numbers? The present `9k` lower bound remains valid, but the binary
+   upper construction does not transfer merely by interpreting its entries
+   as integers. A first step is a source-pinned fitting construction or a
+   stronger exact rank certificate; no such construction is supplied here.
+
+## Attribution
+
+Prepared by **@CubeJerry**, with substantial **OpenAI GPT-6 Astra Pro**
+assistance for mathematical exploration, proof writing, exact checks and
+packaging. The original-subsystem proof and the Petersen extension were
+independently developed within the research team and then cross-checked;
+the two certificate checkers were written separately. The final arguments
+and their precise limits are recorded above.
+
+The entropy corollary was derived separately by the lead and checked by the
+rank-proof worker before integration. It uses the same verified source contacts,
+axiom coefficients and upper-witness Gram entries; no finite experiment is
+presented as a proof about all nonlinear codes.
+
+Credit DreamingOfClouds for the Hall witness and open question in #6846;
+Thiago for the source-bound P111/P112 obstruction and verification approach
+in #1744; Blasiak, Kleinberg and Lubetzky for the underlying Petersen result;
+Bukh and Cox for the fractional Haemers framework; and the authors of #5561
+and its credited predecessors for the unchanged P104 native word. Inputs are
+referenced without modification or re-vendoring. New work is Apache-2.0;
+existing source attribution and licenses remain applicable.
+
+## Concurrent work checked at completion
+
+DreamingOfClouds' open #6854, head
+`3d355ae61f174c5f7101c9eb292722afa5a5f9ac`, excludes dimension exactly `8k`
+for every subset of at least 97 of the 120 E8 lines under its stated mask.
+It explicitly leaves `8k<d<9k` outside its scope. The present result concerns
+the exact P104 source and sharp subsystem dimensions; it does not establish
+the corresponding fractional bound for every 97-line subset, audit that
+contribution's large certificate, or depend on its unmerged files.
diff --git a/research/p104-sharp-block-hall-dimension/SOURCES.json b/research/p104-sharp-block-hall-dimension/SOURCES.json
new file mode 100644
index 0000000000..01d3ff4e2d
--- /dev/null
+++ b/research/p104-sharp-block-hall-dimension/SOURCES.json
@@ -0,0 +1,43 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-designer-toolkit-v2/words/5561.json.gz",
+      "usage": "input",
+      "git_blob": "c367d865a154ffd2ae0b6f6053469580a139f487",
+      "sha256": "b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44"
+    }
+  ],
+  "citation_pins": [
+    {
+      "reference": "CrocSwap/integer-mult-bounds#6846",
+      "repository": "DreamingOfClouds/integer-mult-bounds",
+      "commit": "01651795be9570c47977a73f9cf3e8eeb3fbe64a",
+      "role": "Historical problem statement; not imported by verification."
+    },
+    {
+      "reference": "CrocSwap/integer-mult-bounds#1744",
+      "commit": "78033981ec296b545b3cb50435668fe98e764e65",
+      "path": "research/p112-characteristic-two-minrank/README.md",
+      "role": "Predecessor attribution; the new exact proof is self-contained and does not import its certificate."
+    },
+    {
+      "reference": "CrocSwap/integer-mult-bounds#6854",
+      "commit": "3d355ae61f174c5f7101c9eb292722afa5a5f9ac",
+      "role": "Concurrent scope comparison only; no files imported or scientific claims independently replayed."
+    }
+  ]
+}
diff --git a/research/p104-sharp-block-hall-dimension/TASK.json b/research/p104-sharp-block-hall-dimension/TASK.json
new file mode 100644
index 0000000000..a77aa21e0c
--- /dev/null
+++ b/research/p104-sharp-block-hall-dimension/TASK.json
@@ -0,0 +1,107 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Determine the all-field block inner dimensions of the exact P104 forced-zero label mask and the fourteen-port Hall subsystem of CrocSwap/integer-mult-bounds#6846, including the open interval 8k<d<9k. Derive the corresponding exact deterministic zero-error fixed-length binary broadcast values via the same submodular certificates.",
+  "scope_change_reason": "The orchestrator assigned a precise label-rank geometry audit, seed 68, rather than constructing a decoder itinerary. The investigation transfers the known Petersen obstruction from merged CrocSwap/integer-mult-bounds#1744 to P104 and determines the sharp fractional value of the original Hall subsystem.",
+  "bottleneck_link": "Rank-geometry side result: any source-compatible label compression satisfying this exact mask needs at least 9k dimensions. It does not prove that a general legal supplier must satisfy the pattern and supplies no paid supplier invoice or new kappa.",
+  "budget_minutes": 90,
+  "stop_rule": "Stop after proving and exactly checking a universal obstruction or matching construction for the stated mask. Do not expand into alternate masks, full-mask characteristic-zero upper constructions, or native supplier claims without a new scope. No finite failure is treated as a universal obstruction.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the original subsystem minimum ceil(17k/2); petersen-dual.json and two separately written exact checkers prove a replacement fourteen-port minimum 9k and the full104 all-field lower bound. Explicit coordinate witnesses attain the subsystem bounds; the full104 source attains9k in characteristic two. Registered normal/optimized replay checks source pins, all rank rows, coordinate cases k=1..12, all10816 binary Gram entries and corruption controls. A separately reviewed conditional-entropy reduction proves the nonlinear broadcast corollary; the existing coordinate and full-Gram witnesses certify attaining linear encoders.",
+  "author": "@CubeJerry",
+  "ai_assistance": "Substantial OpenAI GPT-6 Astra Pro assistance for mathematical exploration, independent proof review, separately written exact certificate checks, code and packaging. The mathematical claims and finite verification scopes are explicitly distinguished.",
+  "open_questions": [
+    {
+      "question": "For a specific legal multiplier/caller, does its interface enforce this zero pattern, or can a fully priced helper relaxation remove the Petersen witness?",
+      "why_it_matters": "The rank theorem affects supplier design only when the exact mask is inherited; relaxing an abstract graph does not establish a complete exponent improvement.",
+      "first_step": "Map the fourteen witness ports and required pairings to one source-pinned caller, then price every changed boundary, restoration and ownership operation.",
+      "blocked_by": "No necessity proof for the pattern in every legal caller and no complete paid relaxed-interface construction are supplied."
+    },
+    {
+      "question": "What is the exact full104 block-rank parameter over a specified field outside characteristic two?",
+      "why_it_matters": "The all-field 9k lower bound is universal under the pattern, but full-mask attainment is only proved in characteristic two.",
+      "first_step": "Produce a source-pinned fitting representation over the selected field or a stronger exact rank certificate for the same full mask.",
+      "blocked_by": "Binary parity cancellations do not transfer to other characteristics; no corresponding full-mask upper construction is known from this investigation."
+    }
+  ],
+  "coordination": {
+    "track_seed": 68,
+    "track": "adversarial mathematical audit / label rank geometry",
+    "claim_status": "local-only",
+    "reason": "Connected GitHub tools did not expose a write operation for the current coordination Discussion; no reservation issue was created."
+  },
+  "predecessors": [
+    {
+      "reference": "CrocSwap/integer-mult-bounds#6846",
+      "head": "01651795be9570c47977a73f9cf3e8eeb3fbe64a",
+      "credit": "DreamingOfClouds",
+      "relationship": "Exact P104 zero-mask hypothesis, original14 Hall witness and open block-dimension interval."
+    },
+    {
+      "reference": "CrocSwap/integer-mult-bounds#1744",
+      "head": "78033981ec296b545b3cb50435668fe98e764e65",
+      "credit": "Thiago",
+      "relationship": "Established four-isolates-plus-Petersen all-field obstruction for P111/P112; general mechanism transferred here to P104."
+    },
+    {
+      "reference": "CrocSwap/integer-mult-bounds#6854",
+      "head": "3d355ae61f174c5f7101c9eb292722afa5a5f9ac",
+      "credit": "DreamingOfClouds",
+      "relationship": "Concurrent exact-8k exclusion on all subsets of at least 97 E8 lines; cited only for scope separation, not a dependency or reviewed certificate."
+    }
+  ]
+}
diff --git a/research/p104-sharp-block-hall-dimension/VERIFY.json b/research/p104-sharp-block-hall-dimension/VERIFY.json
new file mode 100644
index 0000000000..0d38d5544a
--- /dev/null
+++ b/research/p104-sharp-block-hall-dimension/VERIFY.json
@@ -0,0 +1,53 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-designer-toolkit-v2/words/5561.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Source-bound rank axioms, original and replacement subsystem witnesses, full binary Gram and ten corruption controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Source-bound rank axioms, original and replacement subsystem witnesses, full binary Gram and ten corruption controls. Assertions disabled."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/audit_petersen.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Separately written exact Petersen coefficient checker and four negative controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-O",
+        "{package}/audit_petersen.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Separately written exact Petersen coefficient checker and four negative controls. Assertions disabled."
+    }
+  ]
+}
diff --git a/research/p104-sharp-block-hall-dimension/audit_petersen.py b/research/p104-sharp-block-hall-dimension/audit_petersen.py
new file mode 100644
index 0000000000..eae4e3fd5d
--- /dev/null
+++ b/research/p104-sharp-block-hall-dimension/audit_petersen.py
@@ -0,0 +1,148 @@
+#!/usr/bin/env python3
+"""Independent exact rank-certificate checker; no numerical solver."""
+from collections import Counter
+from copy import deepcopy
+from fractions import Fraction
+import gzip
+import hashlib
+import itertools
+import json
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+SOURCE = HERE.parents[1] / "research" / "p104-designer-toolkit-v2" / "words" / "5561.json.gz"
+SOURCE_HASH = "b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44"
+P = [61, 62, 63, 67, 68, 69, 95, 99, 100, 101]
+I = [74, 81, 86, 91]
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+def check_dual(certificate, ports):
+    require(certificate["vertices"] == P, "certificate vertex order")
+    full = (1 << len(P)) - 1
+    result = Counter()
+    rhs = Fraction(0)
+    def add(S, a):
+        result[S] += a
+    for kind, entries in (("ub", certificate["ub"]), ("eq", certificate["eq"])):
+        for descriptor, multiplier in entries:
+            a = Fraction(multiplier)
+            if kind == "ub":
+                require(a <= 0, "inequality multiplier sign")
+            tag, *args = descriptor
+            if tag == "empty":
+                require(kind == "eq" and not args, "empty equality")
+                add(0, a)
+                continue
+            require(len(args) in (2, 3), "row arity")
+            S, i, *tail = args
+            require(isinstance(S, int) and 0 <= S <= full, "subset mask")
+            require(isinstance(i, int) and 0 <= i < len(P), "vertex index")
+            b = 1 << i
+            require(not S & b, "vertex must be outside subset")
+            if tag == "mono":
+                require(kind == "ub" and not tail, "monotonicity row")
+                add(S, a)
+                add(S | b, -a)
+            elif tag == "submod":
+                require(kind == "ub" and len(tail) == 1, "submodularity row")
+                j = tail[0]
+                require(isinstance(j, int) and 0 <= j < len(P) and j != i, "second vertex index")
+                c = 1 << j
+                require(not S & c, "second vertex must be outside subset")
+                add(S, a)
+                add(S | b | c, a)
+                add(S | b, -a)
+                add(S | c, -a)
+            elif tag == "zero":
+                require(kind == "eq" and not tail, "zero row")
+                for j in range(len(P)):
+                    if S & (1 << j):
+                        require((ports[P[i]] & ports[P[j]]).bit_count() % 2 == 0,
+                                "zero row uses an allowed contact")
+                add(S | b, a)
+                add(S, -a)
+                rhs += a
+            else:
+                raise ValueError("unknown rank axiom")
+    require({S: a for S, a in result.items() if a} == {full: Fraction(1)},
+            "rank coefficients fail exact identity")
+    require(rhs == 5, "right hand side is not 5k")
+
+def rejected(operation, label):
+    try:
+        operation()
+    except ValueError:
+        return label
+    raise ValueError("negative control accepted: " + label)
+
+def main():
+    source = SOURCE.read_bytes()
+    require(hashlib.sha256(source).hexdigest() == SOURCE_HASH, "source hash")
+    ports = json.loads(gzip.decompress(source))["ports"]
+    require(len(ports) == 104 and len(set(ports)) == 104, "source port count")
+    require(all(isinstance(p, int) and 0 < p < 512 and p.bit_count() % 2 for p in ports), "source format")
+    zero = lambda s, t: s != t and (ports[s] & ports[t]).bit_count() % 2 == 0
+    require(all(zero(s, t) for s, t in itertools.combinations(I, 2)), "isolates mutually zero")
+    require(all(zero(s, t) for s in I for t in P), "isolate/core contacts")
+    require([v for v in range(104) if all(zero(v, i) for i in I)] == P, "common zero neighborhood")
+    edges = {frozenset((s, t)) for s, t in itertools.combinations(P, 2) if not zero(s, t)}
+    require(len(edges) == 15 and all(sum(v in e for e in edges) == 3 for v in P), "core graph")
+    cert = json.loads((HERE / "petersen-dual.json").read_text())
+    check_dual(cert, ports)
+    def match(rest):
+        if not rest:
+            return []
+        s = rest[0]
+        for t in rest[1:]:
+            if frozenset((s, t)) in edges:
+                tail = match([x for x in rest if x not in (s, t)])
+                if tail is not None:
+                    return [(s, t)] + tail
+        return None
+    matching = match(P)
+    require(matching is not None and len(matching) == 5, "perfect matching")
+    groups = [(i,) for i in I] + matching
+    coord = {v: c for c, group in enumerate(groups) for v in group}
+    require(len(coord) == 14, "upper witness coverage")
+    for s, t in itertools.product(I + P, repeat=2):
+        gram = int(coord[s] == coord[t])
+        if s == t:
+            require(gram == 1, "upper witness diagonal")
+        elif zero(s, t):
+            require(gram == 0, "upper witness zero")
+    basis = {}
+    for value in ports:
+        while value:
+            bit = value.bit_length() - 1
+            if bit in basis:
+                value ^= basis[bit]
+            else:
+                basis[bit] = value
+                break
+    require(len(basis) == 9, "full F2 source span")
+    controls = []
+    bad = deepcopy(cert)
+    bad["ub"][0][1] = "1/2"
+    controls.append(rejected(lambda: check_dual(bad, ports), "reversed inequality"))
+    bad = deepcopy(cert)
+    bad["ub"].pop()
+    controls.append(rejected(lambda: check_dual(bad, ports), "missing inequality"))
+    bad = deepcopy(cert)
+    row = next(x for x in bad["eq"] if x[0][0] == "zero")
+    i = row[0][2]
+    j = next(j for j in range(10) if j != i and not zero(P[i], P[j]))
+    row[0][1] = 1 << j
+    controls.append(rejected(lambda: check_dual(bad, ports), "false zero contact"))
+    bad = deepcopy(cert)
+    bad["eq"][-1][1] = "3/2"
+    controls.append(rejected(lambda: check_dual(bad, ports), "altered equality weight"))
+    print(json.dumps({"source_sha256": SOURCE_HASH, "core_lower_bound": "5k", "full_lower_bound": "9k",
+                      "subset_upper_bound": "9k", "matching": matching, "full_F2_minimum": "9k",
+                      "negative_controls_rejected": controls}, indent=2))
+    print("PASS_P104_PETERSEN_EXACT_RANK_PROOF")
+
+if __name__ == "__main__":
+    main()
diff --git a/research/p104-sharp-block-hall-dimension/petersen-dual.json b/research/p104-sharp-block-hall-dimension/petersen-dual.json
new file mode 100644
index 0000000000..033f7e99a4
--- /dev/null
+++ b/research/p104-sharp-block-hall-dimension/petersen-dual.json
@@ -0,0 +1,377 @@
+{
+  "vertices": [
+    61,
+    62,
+    63,
+    67,
+    68,
+    69,
+    95,
+    99,
+    100,
+    101
+  ],
+  "value": 5.0,
+  "ub": [
+    [
+      [
+        "mono",
+        1022,
+        0
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "mono",
+        1020,
+        1
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "mono",
+        1016,
+        2
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "mono",
+        1015,
+        3
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "mono",
+        971,
+        4
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "mono",
+        923,
+        5
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "mono",
+        439,
+        6
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "mono",
+        287,
+        7
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "mono",
+        250,
+        8
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "mono",
+        503,
+        9
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        410,
+        2,
+        0
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        432,
+        3,
+        0
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        945,
+        3,
+        1
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        202,
+        4,
+        0
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        388,
+        4,
+        3
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        472,
+        5,
+        1
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        400,
+        5,
+        3
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        394,
+        6,
+        4
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        284,
+        7,
+        1
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        264,
+        7,
+        2
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        203,
+        8,
+        4
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        138,
+        8,
+        6
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        8,
+        8,
+        7
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        440,
+        9,
+        0
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        433,
+        9,
+        1
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "submod",
+        411,
+        9,
+        6
+      ],
+      "-1/2"
+    ]
+  ],
+  "eq": [
+    [
+      [
+        "empty"
+      ],
+      "1"
+    ],
+    [
+      [
+        "zero",
+        286,
+        0
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        284,
+        0
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "zero",
+        268,
+        0
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        136,
+        1
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        435,
+        2
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        400,
+        2
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "zero",
+        384,
+        2
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        0,
+        3
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        269,
+        4
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        218,
+        5
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        952,
+        6
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        440,
+        6
+      ],
+      "-1/2"
+    ],
+    [
+      [
+        "zero",
+        408,
+        6
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        256,
+        7
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        0,
+        8
+      ],
+      "1/2"
+    ],
+    [
+      [
+        "zero",
+        459,
+        9
+      ],
+      "1/2"
+    ]
+  ]
+}
diff --git a/research/p104-sharp-block-hall-dimension/verify.py b/research/p104-sharp-block-hall-dimension/verify.py
new file mode 100644
index 0000000000..865e675123
--- /dev/null
+++ b/research/p104-sharp-block-hall-dimension/verify.py
@@ -0,0 +1,337 @@
+#!/usr/bin/env python3
+"""Exact source, subspace-inequality and coordinate-witness checks.
+
+Prepared for @CubeJerry with substantial OpenAI GPT-6 Astra Pro assistance.
+No optimizer, numerical rank routine, or predecessor verifier is imported.
+"""
+from __future__ import annotations
+
+import argparse
+from collections import defaultdict
+from copy import deepcopy
+from fractions import Fraction
+import gzip
+import hashlib
+from itertools import combinations, product
+import json
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+SOURCE = HERE.parents[1] / 'research/p104-designer-toolkit-v2/words/5561.json.gz'
+SOURCE_HASH = 'b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44'
+I = frozenset((74, 81, 86, 91))
+S = frozenset((62, 63, 69, 99, 67, 68, 95, 100, 101))
+P = [61, 62, 63, 67, 68, 69, 95, 99, 100, 101]
+OLD = I | S | {57}
+NEW = I | set(P)
+EXPECTED_PORTS = {57:296, 61:112, 62:176, 63:304, 67:224, 68:352,
+                  69:416, 74:478, 81:477, 86:475, 91:471, 95:463,
+                  99:415, 100:351, 101:223}
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def source_ports(raw):
+    require(hashlib.sha256(raw).hexdigest() == SOURCE_HASH, 'source SHA256')
+    ports = json.loads(gzip.decompress(raw))['ports']
+    require(len(ports) == 104 and len(set(ports)) == 104, '104 distinct ports')
+    require(all(type(p) is int and 0 < p < 512 and p.bit_count() % 2 == 1
+                for p in ports), 'odd nine-bit ports')
+    require(all(ports[v] == p for v, p in EXPECTED_PORTS.items()), 'port index convention')
+    return ports
+
+
+def zero_relation(ports):
+    return lambda u, v: u != v and (ports[u] & ports[v]).bit_count() % 2 == 0
+
+
+class RankLedger:
+    """Formal sum in f(A) and k; rank axioms are checked before use.
+
+    Every inequality is oriented >= 0 and has nonnegative weight. Equalities
+    may have signed weights. A zero identity is f(A+v)-f(A)-k = 0.
+    Sets contain actual source port IDs, not subset-mask integer variables.
+    """
+    def __init__(self, vertices, zero):
+        self.vertices = frozenset(vertices)
+        self.zero_pair = zero
+        self.coefficients = defaultdict(Fraction)
+        self.k_coefficient = Fraction()
+        self.rows = 0
+
+    def term(self, vertices, coefficient):
+        vertices = frozenset(vertices)
+        require(vertices <= self.vertices, 'rank set outside universe')
+        self.coefficients[vertices] += Fraction(coefficient)
+
+    def monotonicity(self, smaller, larger, weight=1):
+        weight = Fraction(weight)
+        require(weight >= 0 and set(smaller) <= set(larger), 'monotonicity premise/sign')
+        self.term(larger, weight)
+        self.term(smaller, -weight)
+        self.rows += 1
+
+    def submodularity(self, first, second, weight=1):
+        weight = Fraction(weight)
+        require(weight >= 0, 'submodularity multiplier sign')
+        first, second = frozenset(first), frozenset(second)
+        self.term(first, weight)
+        self.term(second, weight)
+        self.term(first | second, -weight)
+        self.term(first & second, -weight)
+        self.rows += 1
+
+    def zero_additivity(self, base, vertex, weight=1):
+        base, weight = frozenset(base), Fraction(weight)
+        require(vertex in self.vertices and vertex not in base, 'zero identity vertex')
+        require(all(self.zero_pair(vertex, other) for other in base), 'false zero identity')
+        self.term(base | {vertex}, weight)
+        self.term(base, -weight)
+        self.k_coefficient -= weight
+        self.rows += 1
+
+    def empty(self, weight=1):
+        self.term((), weight)
+        self.rows += 1
+
+    def conclude(self, vertices, multiplier, k_bound):
+        actual = {a: c for a, c in self.coefficients.items() if c}
+        require(actual == {frozenset(vertices): Fraction(multiplier)},
+                'rank coefficients do not cancel to stated target')
+        require(self.k_coefficient == -k_bound, 'rank certificate k coefficient')
+        return self.rows
+
+
+def check_nine_core(zero):
+    """Expand the short proof from PROOF.md, including every monotone step."""
+    A = frozenset((62, 69, 99, 68, 100))
+    B = frozenset((62, 99, 67, 95, 100))
+    C = A | B
+    E = frozenset((69, 67, 100))
+    F = frozenset((62, 100))
+    Q = frozenset((69, 99, 67, 68, 100))
+    T = frozenset((62, 69, 67))
+    ledger = RankLedger(S, zero)
+    ledger.monotonicity(A | {63}, S)
+    ledger.zero_additivity(A, 63)
+    ledger.monotonicity(B | {101}, S)
+    ledger.zero_additivity(B, 101)
+    ledger.submodularity(A, B)
+    require(A & B == F | {99}, 'short proof intersection')
+    ledger.zero_additivity(F, 99)
+    ledger.monotonicity(Q | {95}, C)
+    ledger.zero_additivity(Q, 95)
+    ledger.monotonicity(E | {68}, Q)
+    ledger.zero_additivity(E, 68)
+    ledger.submodularity(E, F)
+    require(E & F == {100}, 'short proof final intersection')
+    ledger.monotonicity(T, E | F)
+    ledger.zero_additivity((), 62)
+    ledger.zero_additivity({62}, 69)
+    ledger.zero_additivity({62, 69}, 67)
+    ledger.zero_additivity((), 100)
+    ledger.empty(2)
+    return ledger.conclude(S, 2, 9)
+
+
+def check_petersen(certificate, zero):
+    """Independently translate the lead's bitmask certificate to port sets."""
+    require(certificate['vertices'] == P, 'Petersen vertex order')
+    ledger = RankLedger(P, zero)
+    def subset(mask):
+        require(type(mask) is int and 0 <= mask < 2 ** len(P), 'subset mask')
+        return frozenset(v for i, v in enumerate(P) if (mask >> i) & 1)
+    def vertex(index):
+        require(type(index) is int and 0 <= index < len(P), 'vertex index')
+        return P[index]
+    for descriptor, coefficient in certificate['ub']:
+        require(len(descriptor) in (3, 4), 'inequality descriptor length')
+        coefficient = -Fraction(coefficient)
+        require(coefficient >= 0, 'inequality multiplier sign')
+        base = subset(descriptor[1])
+        v = vertex(descriptor[2])
+        require(v not in base, 'inequality vertex in base')
+        if descriptor[0] == 'mono':
+            require(len(descriptor) == 3, 'monotonicity descriptor')
+            ledger.monotonicity(base, base | {v}, coefficient)
+        else:
+            require(descriptor[0] == 'submod' and len(descriptor) == 4,
+                    'submodularity descriptor')
+            w = vertex(descriptor[3])
+            require(w not in base and v != w, 'submodularity vertices')
+            ledger.submodularity(base | {v}, base | {w}, coefficient)
+    for descriptor, coefficient in certificate['eq']:
+        if descriptor == ['empty']:
+            ledger.empty(coefficient)
+        else:
+            require(len(descriptor) == 3 and descriptor[0] == 'zero', 'equality descriptor')
+            ledger.zero_additivity(subset(descriptor[1]), vertex(descriptor[2]), coefficient)
+    return ledger.conclude(P, 1, 5)
+
+
+def check_petersen_graph(zero):
+    # Standard outer pentagon / inner pentagram presentation, with five spokes.
+    outer = [61, 69, 100, 62, 95]
+    inner = [99, 101, 67, 68, 63]
+    expected = set()
+    for i in range(5):
+        expected.add(frozenset((outer[i], outer[(i+1) % 5])))
+        expected.add(frozenset((outer[i], inner[i])))
+        expected.add(frozenset((inner[i], inner[(i+2) % 5])))
+    actual = {frozenset((u,v)) for u,v in combinations(P, 2) if not zero(u,v)}
+    require(actual == expected and len(expected) == 15, 'Petersen graph isomorphism')
+
+
+def check_isolated_sum(core, zero):
+    require(all(zero(i, j) for i, j in combinations(I, 2)), 'four mutually zero ports')
+    require(all(zero(i, v) for i in I for v in core), 'isolate/core contact')
+    ledger = RankLedger(set(core) | I, zero)
+    previous = frozenset(core)
+    for i in sorted(I):
+        ledger.zero_additivity(previous, i)
+        previous = previous | {i}
+    require({a:c for a,c in ledger.coefficients.items() if c} ==
+            {frozenset(core): Fraction(-1), frozenset(core) | I: Fraction(1)},
+            'isolated-sum identity')
+    require(ledger.k_coefficient == -4, 'isolated-sum constant')
+
+
+OLD_ONE = [(74,), (81,), (86,), (91,57), (99,67), (69,100),
+           (62,68), (63,95), (101,)]
+OLD_TWO = [group for group in [(74,), (81,), (86,), (91,57), (99,67), (69,100)]
+           for _ in range(2)] + [(62,68), (62,95), (63,95), (63,101), (68,101)]
+NEW_ONE = [(74,), (81,), (86,), (91,), (61,69), (62,95), (63,101), (67,100), (68,99)]
+
+
+def coordinates(groups, vertices):
+    result = {v: [] for v in vertices}
+    for coordinate, group in enumerate(groups):
+        require(len(group) == len(set(group)), 'duplicate port in coordinate group')
+        for v in group:
+            require(v in result, 'coordinate uses unknown vertex')
+            result[v].append(coordinate)
+    return result, len(groups)
+
+
+def direct_sum(parts, vertices):
+    result = {v: [] for v in vertices}
+    offset = 0
+    for mapping, dimension in parts:
+        require(set(mapping) == set(vertices), 'direct-sum coverage')
+        for v in vertices:
+            result[v].extend(offset + coordinate for coordinate in mapping[v])
+        offset += dimension
+    return result, offset
+
+
+def check_coordinate_pairings(mapping, dimension, k, vertices, zero):
+    require(set(mapping) == set(vertices), 'upper witness vertex coverage')
+    for v in vertices:
+        require(len(mapping[v]) == k, 'upper witness row count')
+        require(all(type(c) is int and 0 <= c < dimension for c in mapping[v]),
+                'upper witness coordinate outside dimension')
+        diagonal = [[int(a == b) for b in mapping[v]] for a in mapping[v]]
+        require(diagonal == [[int(i == j) for j in range(k)] for i in range(k)],
+                'upper witness diagonal is not identity')
+    for v, w in product(vertices, repeat=2):
+        if zero(v, w):
+            require(all(a != b for a in mapping[v] for b in mapping[w]),
+                    'upper witness violates a forced zero')
+
+
+def check_full_characteristic_two(ports):
+    """Literal 9-bit rows; integer parity checks certify every Gram entry."""
+    rows = [[(p >> bit) & 1 for bit in range(9)] for p in ports]
+    for i, j in product(range(104), repeat=2):
+        entry = sum(x*y for x, y in zip(rows[i], rows[j])) % 2
+        expected = (ports[i] & ports[j]).bit_count() % 2
+        require(entry == expected, 'binary Gram entry')
+        require(i != j or entry == 1, 'binary diagonal')
+    # Exact binary elimination is a consistency check, not the lower proof.
+    basis = {}
+    for value in ports:
+        while value:
+            bit = value.bit_length() - 1
+            if bit in basis:
+                value ^= basis[bit]
+            else:
+                basis[bit] = value
+                break
+    require(len(basis) == 9, 'binary port rank')
+
+
+def rejects(call, label):
+    try:
+        call()
+    except ValueError:
+        return label
+    raise ValueError('negative control was accepted: ' + label)
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--source', type=Path, default=SOURCE)
+    args = parser.parse_args()
+    raw = args.source.read_bytes()
+    ports = source_ports(raw)
+    zero = zero_relation(ports)
+    cert = json.loads((HERE / 'petersen-dual.json').read_text())
+    short_rows = check_nine_core(zero)
+    petersen_rows = check_petersen(cert, zero)
+    check_petersen_graph(zero)
+    check_isolated_sum(S, zero)
+    check_isolated_sum(P, zero)
+    require([v for v in range(104) if all(zero(v, i) for i in I)] == P,
+            'common forced-zero neighborhood')
+    one, two, new = coordinates(OLD_ONE, OLD), coordinates(OLD_TWO, OLD), coordinates(NEW_ONE, NEW)
+    for k in range(1, 13):
+        q, r = divmod(k, 2)
+        old_map, old_d = direct_sum([two] * q + [one] * r, OLD)
+        require(old_d == (17*k + 1)//2, 'old dimension formula')
+        check_coordinate_pairings(old_map, old_d, k, OLD, zero)
+        new_map, new_d = direct_sum([new] * k, NEW)
+        require(new_d == 9*k, 'new dimension formula')
+        check_coordinate_pairings(new_map, new_d, k, NEW, zero)
+    check_full_characteristic_two(ports)
+    controls = []
+    controls.append(rejects(lambda: source_ports(raw[:-1] + bytes((raw[-1] ^ 1,))), 'source-byte mutation'))
+    controls.append(rejects(lambda: check_nine_core(lambda u,v: zero(u,v) and {u,v} != {62,63}),
+                            'missing zero in short proof'))
+    controls.append(rejects(lambda: check_nine_core(lambda u,v: u != v and not zero(u,v)),
+                            'reversed parity convention'))
+    bad = deepcopy(cert); bad['ub'][0][1] = '1/2'
+    controls.append(rejects(lambda: check_petersen(bad, zero), 'reversed inequality multiplier'))
+    bad = deepcopy(cert); bad['ub'].pop()
+    controls.append(rejects(lambda: check_petersen(bad, zero), 'deleted inequality'))
+    bad = deepcopy(cert); bad['eq'][-1][1] = '3/2'
+    controls.append(rejects(lambda: check_petersen(bad, zero), 'altered equality multiplier'))
+    bad = deepcopy(cert)
+    row = next(row for row in bad['eq'] if row[0][0] == 'zero')
+    v = P[row[0][2]]
+    row[0][1] = 1 << next(j for j,w in enumerate(P) if w != v and not zero(v,w))
+    controls.append(rejects(lambda: check_petersen(bad, zero), 'false zero premise'))
+    bad_map = deepcopy(two[0]); bad_map[63][0] = bad_map[62][0]
+    controls.append(rejects(lambda: check_coordinate_pairings(bad_map, 17, 2, OLD, zero),
+                            'forced-zero collision in upper witness'))
+    bad_map = {v: [c for c in cs if c != 16] for v,cs in two[0].items()}
+    controls.append(rejects(lambda: check_coordinate_pairings(bad_map, 16, 2, OLD, zero),
+                            'deleted seventeenth coordinate'))
+    bad_map = deepcopy(two[0]); bad_map[62][1] = bad_map[62][0]
+    controls.append(rejects(lambda: check_coordinate_pairings(bad_map, 17, 2, OLD, zero),
+                            'singular diagonal in upper witness'))
+    print(json.dumps({'source_sha256': SOURCE_HASH, 'short_proof_axiom_rows': short_rows,
+                      'petersen_certificate_rows': petersen_rows,
+                      'original_14_minimum_all_fields': 'ceil(17k/2)',
+                      'replacement_14_minimum_all_fields': '9k',
+                      'full_104_lower_all_fields': '9k',
+                      'full_104_minimum_characteristic_two': '9k',
+                      'coordinate_block_sizes_executed': list(range(1,13)),
+                      'negative_controls_rejected': controls}, indent=2))
+    print('PASS_P104_SHARP_BLOCK_HALL_DIMENSION')
+
+
+if __name__ == '__main__':
+    main()