diff --git a/research/euclidean-orthogonal-detector/PROOF.md b/research/euclidean-orthogonal-detector/PROOF.md
new file mode 100644
index 0000000000..0390000a45
--- /dev/null
+++ b/research/euclidean-orthogonal-detector/PROOF.md
@@ -0,0 +1,167 @@
+# A Euclidean guard for complete orthogonal register programs
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+This is a scoped written proof. The finite checker corroborates its identities
+and implementation; it is not a formal proof-kernel certificate.
+
+## Exact boundary
+
+There are finitely many independent real registers, each in R^d. All registers
+are returned. Instructions are:
+
+- `apply`: replace a register by O or O^T applied to its old value;
+- `query`: add c O or c O^T applied to an old source to an old destination;
+- `linear`: replace a register by a finite rational linear combination of old
+  registers, including repeated occurrences and its own old value.
+
+Each named O is exactly orthogonal. Queries may alias source and destination.
+The two program sides receive the same exact initial bank, whose register
+Euclidean norms are at most R>=1. Initial coordinates belong to the working
+grid h Z, h=2^-p. The special basis input of PR5339 satisfies this condition
+for every p. Arbitrary nongrid inputs need their own input-error term.
+
+Truncate every forward matrix entry toward zero to h Z. The stored inverse
+is the transpose of this table. At each instruction form the complete new
+destination using old register values and exact rational scalar arithmetic,
+then truncate each of its coordinates toward zero once to h Z. Other
+registers retain their values. These are the numerical semantics of Ali
+Romman's [PR5339](https://github.com/CrocSwap/integer-mult-bounds/pull/5339),
+now bounded with a different bank norm. Rounded matrices need not be
+orthogonal; the proof explicitly charges their perturbation.
+
+## Per-instruction constants
+
+Use the bank norm ||x||=max_j ||x_j||_2. Let s=ceil(sqrt(d)). Set
+
+| Instruction | beta | gamma |
+| --- | --- | --- |
+| linear with coefficients c_j | max(1, sum_j abs(c_j)) | 0 |
+| apply | 1 | d |
+| query with coefficient c | 1+abs(c) | d abs(c) |
+
+The exact bank operator has norm at most beta. Each entry error is less
+than h, so the matrix perturbation has Frobenius, and hence operator, norm
+at most d h. Transposition preserves this bound. The rounded bank operator
+therefore has norm at most beta+gamma h and differs from the exact one by
+at most gamma h. These inequalities hold on alias because both summands
+use the same old source. A linear assignment sums repeated old values.
+Unchanged registers explain the harmless maximum with one.
+
+The final coordinate truncations produce a bank residual of norm at most
+sqrt(d) h <= s h. This residual is charged for every instruction, even
+when the actual arithmetic is exact on the grid.
+
+## Whole-side error bound
+
+For one side of length m, define
+
+    G_i = product_(j<=i) beta_j,  G=G_m,
+    A = sum_i gamma_i/beta_i,
+    K = G (R A + s m).
+
+Empty products are one and empty sums are zero. Exact prefix magnitudes are
+at most R G_i. If E_i is the bank error after instruction i, then
+
+    E_i <= (beta_i+gamma_i h) E_(i-1)
+           + gamma_i h R G_(i-1) + s h.                 (1)
+
+This compares the two maps on the exact input and applies the rounded map
+to the previous error. It does not assume the approximate bank stays below
+the exact bank's magnitude envelope.
+
+For nonnegative a_i=gamma_i/beta_i and h A<1,
+
+    product_i (1+h a_i) <= 1/(1-h A).                  (2)
+
+Indeed the coefficient of h^k in the finite product is at most A^k, so the
+product is bounded by the geometric series. The same bound applies to
+every suffix. Unrolling (1) and dividing a suffix product by G_i gives
+
+    E_m <= h G/(1-h A)
+           [R sum_i gamma_i/beta_i + s sum_i 1/G_i]
+         <= h K/(1-h A).                              (3)
+
+The last inequality uses beta_i>=1, hence G_i>=1. Equation (3) is zero
+for an empty side. If h A<=1/2, it gives E_m<=2h K. It also bounds every
+prefix using that prefix's own G,A,K.
+
+For the two sides let A_max=max(A_left,A_right) and K_total=K_left+K_right.
+Every coordinate of their returned difference has error at most
+
+    2 K_total h,
+
+provided h A_max<=1/2. Both sides' errors and every returned role are
+included. No factor of the number of registers occurs in this bank norm.
+
+## A funded exact endpoint decision
+
+Assume a positive rational eta such that a selected exact endpoint f either
+vanishes or has abs(f)>=eta. It suffices to choose integer p>=0 with
+
+    2^p >= max(1, 2 A_max, 8 K_total/eta).              (4)
+
+Then the returned difference f_hat has abs(f_hat-f)<=eta/4. Consequently
+abs(f_hat)>eta/2 decides f!=0. A zero at one tuple is not a universal
+program-identity certificate.
+
+For the rational Cayley path parameter t=A0/B in lowest terms, 0<t<=1/4,
+dimension d, and q named calls across both sides, PR5339 supplies the cited
+separator
+
+    eta = 1/[C (3B)^(dq)],
+
+where C is the product of every scalar coefficient denominator occurrence.
+This separator and its source proof are premises here; their mathematical
+verification is not this contribution. No refined matrix-denominator or
+program-cancellation result is used.
+
+The allocator uses this coarse separator for the source basis input or an
+integer initial bank. Integer linear combinations of the same input columns
+retain its common denominator. A noninteger grid input requires its input
+denominator in the separator as well; the allocator supplies no such
+extension. The error theorem (1)-(4), with a separately justified eta,
+still applies to exact grid inputs under its stated radius contract.
+
+For apply-only programs, G=1, A=d m, and K=m(Rd+s). At R=1 the new rounding
+factor is linear in m and d. The older guard uses the product d^q as a
+coordinate-norm gain, although its operators are exactly orthogonal.
+For one side with d=4, q=m=12, B=4 and no scalar coefficients, the same
+coarse eta gives 182 bits by (4), versus 228 by the old sufficient guard.
+These are sufficient bounds, not minimum precisions. No universal strict
+improvement over the old guard is asserted for arbitrary scalar programs.
+
+## Arithmetic work and limitations
+
+The new allocator uses rational products and sums over the explicit program.
+Its coefficients and precision requirement have polynomial binary size in
+the program, scalar, parameter and dimension input sizes. After the path
+and rational matrices are supplied, the literal integer-grid replay still
+uses q d^2 matrix-entry products and m d coordinate truncations, plus all
+scalar linear combinations, parsing, preparation and returned-bank work.
+This result reduces a sufficient data precision. It supplies no wall-clock
+speedup, cheaper native invocation or full tape invoice.
+
+Orthogonality is an essential premise. General approximately unitary or
+nonorthogonal generators need their own exact gains. Nongrid inputs, complex
+coordinate rounding, floating hardware, and repeated use of a stored inverse
+as an exact undo are outside this stated implementation. Dirty values are
+covered within the radius and grid contract; the detector does not erase or
+restore them by fiat. Native compatibility, physical allocation, compiler,
+stock, selected precision/tape policy and analytic recovery remain separate.
+
+## Credit and relation to prior work
+
+Ali Romman / PR5339 supplies the complete numerical detector, coarse
+separator and open optimization question. His PR5315 supplies the rational
+orthogonal witness. Krzysztof Wojt / PR5262 supplies the complete inverse
+grammar and shortest-word compiler; zxv / PR5235 and the retained
+dirty-echo/tensor/phase lineage keep their credit. Nick Petalas / PR5941
+changes the separation lattice through exact matrix denominators. This
+proof holds that lattice bound fixed and changes error amplification. It
+does not pursue PR5941's cancellation or native-binding questions.
+
+Euclidean orthogonal invariance, Frobenius domination and forward-error
+propagation are classical. The new result is the explicit complete-grammar
+guard (3)-(4), its allocator, and the strictly smaller sufficient grid for
+the specified literal consumer. No general literature priority is claimed.
diff --git a/research/euclidean-orthogonal-detector/README.md b/research/euclidean-orthogonal-detector/README.md
new file mode 100644
index 0000000000..86c0502b27
--- /dev/null
+++ b/research/euclidean-orthogonal-detector/README.md
@@ -0,0 +1,155 @@
+# A smaller Euclidean guard for complete orthogonal-witness detection
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped written proof with exact finite corroboration; no new kappa. A new
+whole-bank Euclidean error bound reduces the sufficient fractional grid of
+one literal four-dimensional, twelve-call detector from **228 to 182 bits**.
+The same coarse endpoint separator is used in both bounds. The new result
+changes accumulated rounding amplification, without using a refined matrix
+or program denominator.
+
+For a side of m instructions, define its exact norm gains beta_i, entry
+perturbation constants gamma_i, input radius R>=1, and
+
+```text
+s = ceil(sqrt(d))
+G = product beta_i
+A = sum gamma_i/beta_i
+K = G (R A + s m)
+```
+
+Each exact orthogonal apply has beta=1. Aliased queries and arbitrary rational
+scalar assignments have the fully charged bounds in [PROOF.md](PROOF.md).
+At grid h=2^-p with hA<1, the complete side's register error is at most
+`h K/(1-h A)`. For two sides it suffices to choose
+
+```text
+2^p >= max(1, 2 max(A_left,A_right), 8 (K_left+K_right)/eta)
+```
+
+to obtain endpoint error at most eta/4 and an exact zero/nonzero decision
+under the credited separation premise. For apply-only words, K is linear
+in the number of calls and dimension. No minimum-precision claim or strict
+improvement for every scalar program is made.
+
+## Evidence and reproduction
+
+From the repository root with the CPython 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/euclidean-orthogonal-detector/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/euclidean-orthogonal-detector/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/euclidean-orthogonal-detector
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/euclidean-orthogonal-detector --check-source-history
+```
+
+Another CPython 3.12 executable can replace the displayed local path. The
+standalone marker is `PASS_EUCLIDEAN_ORTHOGONAL_DETECTOR`; the registered
+launcher also prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Normal and optimized
+warning-strict commands are registered with 120-second caps. The direct
+verifier writes nothing and emits a generated JSON receipt binding all eight
+package files. Redirect it outside the checkout to retain the receipt.
+
+The exact finite evidence includes:
+
+- 1,218 complete program/input cases over dimensions two through seven and
+  Cayley parameters 1/4 and 1/7. Seven program-pair patterns include
+  noncommuting order changes, restored inverse words, aliased queries,
+  repeated scalar sources, zero coefficients, empty sides and scalar gains
+  and denominators as large as 2^40. There are 84 mixed dirty input cases;
+  the other cases enumerate every independent input column.
+- 9,048 intermediate returned banks, comprising 138,528 scalar coordinates,
+  checked against their own prefix Euclidean envelopes. Every final
+  coordinate also has its difference error and selected threshold decision
+  checked against a separate rational interpreter.
+- A nonzero four-dimensional, twelve-call fixture executed at both 228 and
+  182 bits, with the same eta=12^-48. Its exact selected endpoint is
+  `33658561053084102656/87507831740087890625`. The new bound fails its
+  sufficient inequality at 181 bits; this does not prove 182 is necessary.
+- 240 finite product inequalities, 256 precision-rounding cases, fourteen
+  invalid-input controls and four semantic controls. The latter detect
+  omitted coefficient quantization, a wrong inverse table, use of updated
+  values in an aliased query, and one fewer bit in the stated sufficient
+  guard.
+
+The universal statement rests on the written proof. These finite executions
+corroborate it and the new implementation. No predecessor scientific program,
+receipt or census is imported or replayed.
+
+## Source, scope and credit
+
+Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision
+8, selected PR6030. The selected binding-only baseline passed. [TASK.json](TASK.json)
+records the explicit change from `formal-interface-lemma` to a quantitative
+written precision-interface proof. [SOURCES.json](SOURCES.json) pins historical
+provenance; there are no external runtime inputs or pending Git dependencies.
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363345)
+reserves this accumulated-error question. Discovery stopped at the first
+verified strict grid improvement.
+
+Credit Ali Romman / [PR5339](https://github.com/CrocSwap/integer-mult-bounds/pull/5339)
+for the complete detector, coarse separator and open optimization question,
+and [PR5315](https://github.com/CrocSwap/integer-mult-bounds/pull/5315) for the
+orthogonal realization. Krzysztof Wojt / PR5262 supplies the inverse grammar
+and witness compiler; zxv / PR5235 and the retained dirty-echo/tensor/phase
+lineage keep their credit. Nick Petalas / PR5941 concerns exact matrix
+separation denominators, a different step held fixed here. Euclidean
+orthogonal invariance, Frobenius domination and forward-error propagation
+are classical. No global literature priority is claimed.
+
+Live open/account PRs, active Discussions, recent handoffs, main README
+searches, merged general-form searches and local reservations were checked.
+Cached overlap scanning has sparse historical-note coverage; unpublished work
+and arbitrary historical diffs remain limits. These are bounded overlap
+checks, not a guarantee of novelty.
+
+## Limits and implementation bounds
+
+The error theorem assumes exact real orthogonality, old-value instructions,
+exact rational scalar arithmetic and once-per-output coordinate truncation.
+Initial data must be exactly on the working grid and have the stated norm
+radius. The allocator's coarse separation bound is for integer initial banks
+and matching Cayley matrices. Nongrid input errors and noninteger-input
+separation need separate treatment. Orthogonality and these caller premises
+are essential; stored rounded matrices need not be orthogonal.
+
+A zero at one selected endpoint is not a universal identity certificate.
+The 46-bit reduction is a sufficient precision improvement, not a runtime,
+optimality, native-call or exponent improvement. Matrix preparation, scalar
+arithmetic, movement, ownership/restoration, stock, compiler, actual selected
+precision/tape use and analytic recovery remain separate obligations. No
+selected scientific replay, native suite, Lean or Docker build was run.
+Independent human and formal proof-kernel review are unclaimed. The five
+selected framework assumptions and selected frontier retain their status.
+
+Build the Lever led to the explicit rational allocator and standalone replay.
+Prove It Works led to complete intermediate-bank checks and literal execution
+at the smaller grid. Power of Ten inspection found no recursion, subprocess,
+network, dynamic evaluation or background work. Functions fit within 60 lines.
+Allocation validates at most sixteen dimensions, four roles, three operators,
+64 instructions per side, eight terms per scalar row, and 128-bit scalar
+numerators and denominators. The fixed verifier uses dimensions at most seven,
+three roles and at most 24 instructions on a side. Source-hash reads are
+capped at 256 KiB per file. Exact exceptions survive optimized Python.
+
+Power of Ten rule 3 deviation: CPython allocates managed rational and integer
+objects during the bounded offline calculation. Fixed domains, explicit API
+capacities and 8-by-256-KiB source capacity bound live state; runtime allocation
+itself is not instrumented. A fixed-storage runtime would be required before
+claiming that property. Rule 9 deviation: local `map` calls have only the
+visible built-in or rational constructor targets and finite collections.
+Rule 10 diagnostics are warning-strict normal/optimized execution and in-memory
+AST compilation. No separate static analyzer or proof assistant is claimed.
+Widening the stated capacities requires a new resource assessment.
+
+## Open next questions
+
+- Can one native-compatible orthogonal witness use this guard with a fully
+  charged caller? Pin its actual operators, input grid and radius, then count
+  preparation, arithmetic, movement and restoration. Native source binding
+  and a complete physical bill are missing.
+- Can exact instruction norms reduce a scalar-heavy guard further? Start
+  with one fixed linear or aliased-query instruction and retain matrix
+  quantization and data truncation. No optimal-norm or least-precision theorem
+  is supplied. Structured relevance and blockers are in TASK.json.
diff --git a/research/euclidean-orthogonal-detector/SOURCES.json b/research/euclidean-orthogonal-detector/SOURCES.json
new file mode 100644
index 0000000000..203c74fe39
--- /dev/null
+++ b/research/euclidean-orthogonal-detector/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "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/orthogonal-witness-precision/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "36d4c06875c7346e437227a4206f0eb474c53e76",
+      "sha256": "762ef04f95edc3a55347d5f58a166cde77a100e9331326e180cffa9eef88eaaa"
+    },
+    {
+      "path": "research/orthogonal-witness-precision/README.md",
+      "usage": "provenance",
+      "git_blob": "0bd504969b70f7eb97f74b7bd84754adb2b18e08",
+      "sha256": "e41efda1fc15fcaf188359578c60fb24ce57068c56f08fc510cc44695d7534b4"
+    },
+    {
+      "path": "research/orthogonal-witness-precision/detector.py",
+      "usage": "provenance",
+      "git_blob": "1c7d7d8f7212dacc771f60263fca3120fe3fa8f6",
+      "sha256": "986637ef31cdf46976d466e25b58b2cc2de7fb60939bda1b4693e72541b3c7af"
+    }
+  ]
+}
diff --git a/research/euclidean-orthogonal-detector/TASK.json b/research/euclidean-orthogonal-detector/TASK.json
new file mode 100644
index 0000000000..8af4b84c3e
--- /dev/null
+++ b/research/euclidean-orthogonal-detector/TASK.json
@@ -0,0 +1,128 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove a complete-register Euclidean rounding-error guard for the PR5339 detector and construct a strict smaller-grid fixture, holding its coarse endpoint separator fixed.",
+  "scope_change_reason": "This is a new quantitative written proof and exact finite corroboration for an error interface. It is not a proof-kernel formalization or an audit of predecessor mathematics.",
+  "bottleneck_link": "Scoped precision side result: exact orthogonal calls need not multiply the magnitude bound by the path dimension. Source/native binding and a complete physical bill are still required before any supplier or kappa consequence.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved and exactly corroborated smaller sufficient grid; package it without extending the research.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the complete-grammar error guard; verify.py prints PASS_EUCLIDEAN_ORTHOGONAL_DETECTOR with 1,218 program/input cases, 9,048 prefix banks, 14 invalid and four semantic controls, and literal 228-to-182-bit executions. The generated stdout receipt binds all eight package files.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a native-compatible orthogonal witness use this guard with a fully charged caller?",
+      "why_it_matters": "Only an actual caller and complete price can turn the local precision improvement into a supplier benefit.",
+      "first_step": "Pin one caller, its real orthogonal operators, exact input grid and radius; apply the guard and count preparation, arithmetic, movement and restoration.",
+      "blocked_by": "No native-compatible source binding, physical bill or selected caller is supplied."
+    },
+    {
+      "question": "Can exact program-specific beta values further reduce a scalar-heavy guard?",
+      "why_it_matters": "The new triangle bounds need not improve every scalar program.",
+      "first_step": "For one fixed linear or aliased-query instruction, bound its exact bank norm and retain all matrix quantization and final truncation terms.",
+      "blocked_by": "No optimal-norm or least-precision claim is proved here."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363345",
+  "claim_type": "scoped written proof with exact finite corroboration",
+  "environment": {
+    "python": "CPython 3.12.15",
+    "dependencies": "standard library"
+  },
+  "overlap": {
+    "source": "PR #5339",
+    "source_author": "aliromman",
+    "predecessor_author": "aliromman",
+    "recent_source_uses_before_this": 1,
+    "distinct_from": "PR5941 changes per-matrix separation denominators; this work holds the separator fixed and changes accumulated rounding amplification.",
+    "limits": "Live open/account lists, active Discussions, recent handoffs, main README and merged/general-form searches checked. Cached scan and sparse historical notes have explicitly limited coverage; unpublished work and arbitrary diffs are not covered."
+  },
+  "finite_evidence": {
+    "proof": "PROOF.md",
+    "direct_marker": "PASS_EUCLIDEAN_ORTHOGONAL_DETECTOR",
+    "program_inputs": 1218,
+    "dirty_inputs": 84,
+    "checked_prefixes": 9048,
+    "checked_prefix_coordinates": 138528,
+    "strict_grid_bits": {
+      "old": 228,
+      "new": 182,
+      "saving": 46
+    }
+  }
+}
diff --git a/research/euclidean-orthogonal-detector/VERIFY.json b/research/euclidean-orthogonal-detector/VERIFY.json
new file mode 100644
index 0000000000..9d96d166b8
--- /dev/null
+++ b/research/euclidean-orthogonal-detector/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Written-guard exact finite corroboration: complete rational and integer-grid executions, every prefix and returned coordinate, dirty/basis inputs, aliases, scalar extremes, strict 228-to-182-bit fixture, 14 rejecting and four semantic controls, generated source-bound stdout receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Written-guard exact finite corroboration: complete rational and integer-grid executions, every prefix and returned coordinate, dirty/basis inputs, aliases, scalar extremes, strict 228-to-182-bit fixture, 14 rejecting and four semantic controls, generated source-bound stdout receipt."
+    }
+  ]
+}
diff --git a/research/euclidean-orthogonal-detector/guard.py b/research/euclidean-orthogonal-detector/guard.py
new file mode 100644
index 0000000000..2014c43ccf
--- /dev/null
+++ b/research/euclidean-orthogonal-detector/guard.py
@@ -0,0 +1,139 @@
+"""Rational Euclidean guards for complete orthogonal register programs.
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+The complete grammar and coarse separator are credited in PROOF.md.
+"""
+
+from dataclasses import dataclass
+from fractions import Fraction as Q
+from math import isqrt
+
+
+@dataclass(frozen=True)
+class Step:
+    op: str
+    dst: int
+    src: int = 0
+    label: int = 0
+    direction: int = 1
+    coefficient: Q = Q(1)
+    terms: tuple = ()
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def scalar(value):
+    need(type(value) in (int, Q), "exact scalar required")
+    result = Q(value)
+    need(max(abs(result.numerator).bit_length(), result.denominator.bit_length()) <= 128,
+         "scalar capacity exceeded")
+    return result
+
+
+def validate(program, dimension, roles, labels):
+    need(type(dimension) is int and 1 <= dimension <= 16, "dimension capacity")
+    need(type(roles) is int and 1 <= roles <= 4, "role capacity")
+    need(type(labels) is int and 1 <= labels <= 3, "operator capacity")
+    need(type(program) is tuple and len(program) == 2, "two program sides required")
+    for side in program:
+        need(type(side) is tuple and len(side) <= 64, "instruction capacity")
+        for step in side:
+            need(type(step) is Step and step.op in ("apply", "query", "linear"),
+                 "invalid instruction")
+            need(type(step.dst) is int and 0 <= step.dst < roles, "invalid destination")
+            if step.op == "linear":
+                need(type(step.terms) is tuple and len(step.terms) <= 8, "term capacity")
+                for term in step.terms:
+                    need(type(term) is tuple and len(term) == 2, "invalid scalar term")
+                    source, coefficient = term
+                    need(type(source) is int and 0 <= source < roles, "invalid term role")
+                    scalar(coefficient)
+            else:
+                need(type(step.label) is int and 0 <= step.label < labels, "invalid operator")
+                need(type(step.direction) is int and step.direction in (-1, 1), "invalid inverse")
+                if step.op == "query":
+                    need(type(step.src) is int and 0 <= step.src < roles, "invalid source")
+                    scalar(step.coefficient)
+
+
+def coefficients(step):
+    if step.op == "linear":
+        return tuple(Q(value) for _, value in step.terms)
+    if step.op == "query":
+        return (Q(step.coefficient),)
+    return ()
+
+
+def instruction_bounds(step, dimension):
+    if step.op == "linear":
+        return max(Q(1), sum(map(abs, coefficients(step)), Q(0))), Q(0)
+    if step.op == "apply":
+        return Q(1), Q(dimension)
+    amount = abs(Q(step.coefficient))
+    return 1 + amount, dimension * amount
+
+
+def side_statistics(side, dimension, radius):
+    gain, sensitivity = Q(1), Q(0)
+    for step in side:
+        beta, gamma = instruction_bounds(step, dimension)
+        gain *= beta
+        sensitivity += gamma / beta
+    coordinate_radius = isqrt(dimension - 1) + 1
+    credit = gain * (radius * sensitivity + coordinate_radius * len(side))
+    return gain, sensitivity, credit
+
+
+def ceil_log2(value):
+    need(value > 0, "positive precision requirement")
+    bits = max(0, value.numerator.bit_length() - value.denominator.bit_length())
+    return bits + int(Q(1 << bits) < value)
+
+
+def allocate(program, dimension, roles, labels, parameter, radius=Q(1)):
+    """Fund the cited Cayley separator for integer initial banks of norm <= radius.
+
+    Matching exact Cayley operators are a caller premise, as in PR5339.
+    Nongrid input errors and noninteger-input separation are not supplied.
+    """
+    validate(program, dimension, roles, labels)
+    parameter, radius = scalar(parameter), scalar(radius)
+    need(0 < parameter <= Q(1, 4), "Cayley parameter outside contract")
+    need(radius >= 1, "input radius must be at least one")
+    denominator, calls, old_gain, old_gamma = 1, 0, Q(1), Q(0)
+    for side in program:
+        for step in side:
+            beta, gamma = instruction_bounds(step, dimension)
+            if step.op != "linear":
+                calls += 1
+                beta = Q(dimension) if step.op == "apply" else 1 + gamma
+            old_gain *= beta
+            old_gamma = max(old_gamma, gamma)
+            for value in coefficients(step):
+                denominator *= value.denominator
+    separator_denominator = denominator * (3 * parameter.denominator) ** (dimension * calls)
+    eta = Q(1, separator_denominator)
+    statistics = tuple(side_statistics(side, dimension, radius) for side in program)
+    sensitivity = max(row[1] for row in statistics)
+    credit = sum((row[2] for row in statistics), Q(0))
+    requirement = max(Q(1), 2 * sensitivity, 8 * credit / eta)
+    bits = ceil_log2(requirement)
+    old_error = sum(map(len, program)) * old_gain * (old_gamma * radius * old_gain + 1)
+    old_bits = ceil_log2(4 * max(Q(1), old_error) / eta)
+    error = 2 * credit / (1 << bits)
+    need(sensitivity / (1 << bits) <= Q(1, 2) and error <= eta / 4,
+         "unfunded Euclidean guard")
+    return dict(bits=bits, old_bits=old_bits, eta=eta, error=error,
+                radius=radius, statistics=statistics, calls=calls,
+                steps=sum(map(len, program)), scalar_denominator=denominator)
+
+
+def prefix_error(side, dimension, radius, bits):
+    gain, sensitivity, credit = side_statistics(side, dimension, radius)
+    del gain  # The complete credit already includes this factor.
+    h = Q(1, 1 << bits)
+    need(h * sensitivity < 1, "rounding sensitivity is not funded")
+    return h * credit / (1 - h * sensitivity)
diff --git a/research/euclidean-orthogonal-detector/linear.py b/research/euclidean-orthogonal-detector/linear.py
new file mode 100644
index 0000000000..0ec540893a
--- /dev/null
+++ b/research/euclidean-orthogonal-detector/linear.py
@@ -0,0 +1,125 @@
+"""Standalone rational and integer-grid interpreters for finite evidence.
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+"""
+
+from fractions import Fraction as Q
+
+from guard import need, validate
+
+
+def transpose(matrix):
+    return [list(row) for row in zip(*matrix)]
+
+
+def multiply(left, right):
+    columns = transpose(right)
+    return [[sum((a * b for a, b in zip(row, column)), Q(0))
+             for column in columns] for row in left]
+
+
+def inverse(matrix):
+    size = len(matrix)
+    need(1 <= size <= 16, "inverse capacity")
+    rows = [list(map(Q, row)) + [Q(i == j) for j in range(size)]
+            for i, row in enumerate(matrix)]
+    for column in range(size):
+        pivot = next((i for i in range(column, size) if rows[i][column]), None)
+        need(pivot is not None, "singular matrix")
+        rows[pivot], rows[column] = rows[column], rows[pivot]
+        scale = rows[column][column]
+        rows[column] = [value / scale for value in rows[column]]
+        for i in range(size):
+            if i != column:
+                scale = rows[i][column]
+                rows[i] = [a - scale * b for a, b in zip(rows[i], rows[column])]
+    return [row[size:] for row in rows]
+
+
+def cayley(word, labels, parameter):
+    size = len(word) + 1
+    need(1 <= size <= 16 and 1 <= labels <= 3, "matrix fixture capacity")
+    need(all(type(label) is int and 0 <= label < labels for label in word), "path labels")
+    result = []
+    for label in range(labels):
+        skew = [[Q(0) for _ in range(size)] for _ in range(size)]
+        for i, edge in enumerate(word):
+            if edge == label:
+                skew[i][i + 1], skew[i + 1][i] = Q(1), Q(-1)
+        minus = [[Q(i == j) - parameter * skew[i][j] / 2
+                  for j in range(size)] for i in range(size)]
+        plus = [[Q(i == j) + parameter * skew[i][j] / 2
+                 for j in range(size)] for i in range(size)]
+        result.append(multiply(inverse(minus), plus))
+    return result
+
+
+def check_matrices(matrices, dimension):
+    need(1 <= len(matrices) <= 3, "matrix count")
+    identity = [[Q(i == j) for j in range(dimension)] for i in range(dimension)]
+    for matrix in matrices:
+        need(len(matrix) == dimension and all(len(row) == dimension for row in matrix),
+             "matrix shape")
+        need(multiply(transpose(matrix), matrix) == identity, "orthogonal matrices required")
+
+
+def exact_trace(side, matrices, initial):
+    values = [list(map(Q, row)) for row in initial]
+    trace = []
+    for step in side:
+        if step.op == "linear":
+            new = [sum((Q(c) * values[src][j] for src, c in step.terms), Q(0))
+                   for j in range(len(values[0]))]
+        else:
+            matrix = matrices[step.label]
+            if step.direction == -1:
+                matrix = transpose(matrix)
+            source = values[step.dst if step.op == "apply" else step.src]
+            new = [sum((a * b for a, b in zip(row, source)), Q(0)) for row in matrix]
+            if step.op == "query":
+                new = [old + Q(step.coefficient) * value
+                       for old, value in zip(values[step.dst], new)]
+        values[step.dst] = new
+        trace.append([row[:] for row in values])
+    return trace
+
+
+def trunc(value):
+    value = Q(value)
+    return value.numerator // value.denominator if value >= 0 else -((-value.numerator) // value.denominator)
+
+
+def rounded_trace(side, matrices, initial, bits, wrong_inverse=False):
+    scale = 1 << bits
+    tables = [[[trunc(scale * value) for value in row] for row in matrix]
+              for matrix in matrices]
+    need(all(Q(value * scale).denominator == 1 for row in initial for value in row),
+         "input is not on the working grid")
+    values = [[int(value * scale) for value in row] for row in initial]
+    trace = []
+    for step in side:
+        if step.op == "linear":
+            new = [trunc(sum((Q(c) * values[src][j] for src, c in step.terms), Q(0)))
+                   for j in range(len(values[0]))]
+        else:
+            matrix = tables[step.label]
+            if step.direction == -1 and not wrong_inverse:
+                matrix = transpose(matrix)
+            source = values[step.dst if step.op == "apply" else step.src]
+            dots = [sum(a * b for a, b in zip(row, source)) for row in matrix]
+            if step.op == "apply":
+                new = [trunc(Q(value, scale)) for value in dots]
+            else:
+                new = [trunc(old + Q(step.coefficient) * Q(value, scale))
+                       for old, value in zip(values[step.dst], dots)]
+        values[step.dst] = new
+        trace.append([[Q(value, scale) for value in row] for row in values])
+    return trace
+
+
+def checked_traces(program, matrices, initial, bits):
+    dimension, roles = len(initial[0]), len(initial)
+    validate(program, dimension, roles, len(matrices))
+    check_matrices(matrices, dimension)
+    return tuple((exact_trace(side, matrices, initial),
+                  rounded_trace(side, matrices, initial, bits)) for side in program)
diff --git a/research/euclidean-orthogonal-detector/verify.py b/research/euclidean-orthogonal-detector/verify.py
new file mode 100644
index 0000000000..184864b070
--- /dev/null
+++ b/research/euclidean-orthogonal-detector/verify.py
@@ -0,0 +1,243 @@
+"""Finite exact corroboration of the new guard, without predecessor imports.
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+"""
+
+import ast
+from fractions import Fraction as Q
+from hashlib import sha256
+import json
+from pathlib import Path
+import platform
+import sys
+
+ROOT = Path(__file__).resolve().parent
+sys.path.insert(0, str(ROOT))
+
+from guard import Step, allocate, ceil_log2, need, prefix_error, validate
+from linear import cayley, checked_traces, check_matrices, exact_trace, rounded_trace
+
+
+def squared_norm(row):
+    return sum((value * value for value in row), Q(0))
+
+
+def compare_rows(expected, actual, bound):
+    need(len(expected) == len(actual), "returned role count")
+    for left, right in zip(expected, actual):
+        error = [a - b for a, b in zip(left, right)]
+        need(squared_norm(error) <= bound * bound, "Euclidean error envelope")
+
+
+def run_case(program, matrices, parameter, initial, radius):
+    dimension, roles = len(initial[0]), len(initial)
+    need(all(squared_norm(row) <= radius * radius for row in initial), "input norm")
+    plan = allocate(program, dimension, roles, len(matrices), parameter, radius)
+    traces = checked_traces(program, matrices, initial, plan["bits"])
+    prefixes = coordinates = 0
+    endpoints = []
+    for side, (exact, rounded) in zip(program, traces):
+        for index, (expected, actual) in enumerate(zip(exact, rounded)):
+            bound = prefix_error(side[:index + 1], dimension, radius, plan["bits"])
+            compare_rows(expected, actual, bound)
+            prefixes += 1
+            coordinates += roles * dimension
+        endpoints.append((exact[-1] if exact else initial,
+                          rounded[-1] if rounded else initial))
+    for role in range(roles):
+        for coordinate in range(dimension):
+            value = endpoints[0][0][role][coordinate] - endpoints[1][0][role][coordinate]
+            rounded = endpoints[0][1][role][coordinate] - endpoints[1][1][role][coordinate]
+            need(abs(value - rounded) <= plan["error"], "complete difference error")
+            need(value == 0 or abs(value) >= plan["eta"], "fixture separation")
+            need((abs(rounded) > plan["eta"] / 2) == (value != 0), "endpoint decision")
+    return prefixes, coordinates
+
+
+def programs():
+    apply = tuple(Step("apply", 0, label=i % 2, direction=1) for i in range(12))
+    closed = apply + tuple(Step("apply", 0, label=step.label, direction=-1)
+                           for step in reversed(apply))
+    return (
+        (apply, ()),
+        (closed, ()),
+        ((Step("apply", 0), Step("apply", 0, label=1)),
+         (Step("apply", 0, label=1), Step("apply", 0))),
+        ((Step("query", 1, src=0, coefficient=Q(2, 3)),
+          Step("query", 1, src=1, label=1, direction=-1, coefficient=Q(-3, 2)),
+          Step("linear", 2, terms=((1, Q(5, 7)), (2, Q(-1)), (1, Q(-2, 7)))),
+          Step("apply", 2, label=1)),
+         (Step("query", 2, src=0, direction=-1, coefficient=Q(1, 5)),)),
+        ((Step("linear", 0, terms=((0, Q(1 << 40)), (1, Q(1, 1 << 40)))),
+          Step("query", 0, src=0, label=1, coefficient=Q(-1, 3)),
+          Step("apply", 0, direction=-1)),
+         (Step("linear", 0, terms=((0, Q(1 << 40)),)),)),
+        ((Step("linear", 1, terms=()), Step("query", 1, src=0, coefficient=Q(0))),
+         (Step("linear", 1, terms=((0, Q(1, 3)), (0, Q(-1, 3)))),)),
+        ((), ()),
+    )
+
+
+def finite_program_checks():
+    count = prefixes = coordinates = dirty = 0
+    for dimension in range(2, 8):
+        word = tuple(i % 2 for i in range(dimension - 1))
+        for parameter in (Q(1, 4), Q(1, 7)):
+            matrices = cayley(word, 2, parameter)
+            for program in programs():
+                for input_column in range(3 * dimension):
+                    initial = [[Q(int(i * dimension + j == input_column))
+                                for j in range(dimension)] for i in range(3)]
+                    new_prefixes, new_coordinates = run_case(program, matrices, parameter,
+                                                             initial, Q(1))
+                    count += 1
+                    prefixes += new_prefixes
+                    coordinates += new_coordinates
+                initial = [[Q((i + 2 * j) % 7 - 3) for j in range(dimension)]
+                           for i in range(3)]
+                new_prefixes, new_coordinates = run_case(program, matrices, parameter,
+                                                         initial, Q(3 * dimension))
+                count += 1
+                dirty += 1
+                prefixes += new_prefixes
+                coordinates += new_coordinates
+    return dict(program_inputs=count, dirty_inputs=dirty,
+                checked_prefixes=prefixes, checked_prefix_coordinates=coordinates)
+
+
+def strict_fixture():
+    dimension, parameter = 4, Q(1, 4)
+    program = (tuple(Step("apply", 0, label=i % 2) for i in range(12)), ())
+    matrices = cayley((0, 1, 0), 2, parameter)
+    initial = [[Q(0), Q(0), Q(0), Q(1)]]
+    plan = allocate(program, dimension, 1, 2, parameter)
+    need(plan["bits"] == 182 and plan["old_bits"] == 228, "strict grid consequence")
+    exact = exact_trace(program[0], matrices, initial)[-1]
+    need(exact[0][0] != 0, "fixture must be a nonzero selected endpoint")
+    for bits in (plan["bits"], plan["old_bits"]):
+        actual = rounded_trace(program[0], matrices, initial, bits)[-1]
+        compare_rows(exact, actual, plan["eta"] / 4)
+        need(abs(actual[0][0]) > plan["eta"] / 2, "strict fixture detector")
+    return dict(dimension=dimension, calls=12, parameter=str(parameter),
+                old_bits=plan["old_bits"], new_bits=plan["bits"],
+                saved_bits=plan["old_bits"] - plan["bits"],
+                selected_exact_value=str(exact[0][0]),
+                separation=str(plan["eta"]), error_bound=str(plan["error"]))
+
+
+def product_bound_checks():
+    count = 0
+    for denominator in range(2, 17):
+        for length in range(1, 17):
+            amounts = [Q((i * 3 + length) % 7, 7 * length) for i in range(length)]
+            total, product = sum(amounts, Q(0)), Q(1)
+            h = Q(1, denominator)
+            for amount in amounts:
+                product *= 1 + h * amount
+            need(product <= 1 / (1 - h * total), "finite product bound")
+            count += 1
+    for numerator in range(1, 257):
+        requirement = Q(numerator, 7)
+        bits = ceil_log2(requirement)
+        need(Q(1 << bits) >= requirement, "precision upper rounding")
+        need(bits == 0 or Q(1 << (bits - 1)) < requirement, "precision minimal integer")
+    return dict(product_inequalities=count, precision_rounding_cases=256)
+
+
+def reject_invalid(case):
+    try:
+        if case == 0:
+            validate(((), ()), 0, 1, 1)
+        elif case == 1:
+            validate(((), ()), 17, 1, 1)
+        elif case == 2:
+            validate(((), ()), 2, 5, 1)
+        elif case == 3:
+            validate(((Step("apply", 1),), ()), 2, 1, 1)
+        elif case == 4:
+            validate(((Step("query", 0, src=1),), ()), 2, 1, 1)
+        elif case == 5:
+            validate(((Step("apply", 0, direction=0),), ()), 2, 1, 1)
+        elif case == 6:
+            validate(((Step("linear", 0, terms=((0, 0.5),)),), ()), 2, 1, 1)
+        elif case == 7:
+            validate(((Step("apply", 0),) * 65, ()), 2, 1, 1)
+        elif case == 8:
+            allocate(((), ()), 2, 1, 1, Q(1, 3))
+        elif case == 9:
+            allocate(((), ()), 2, 1, 1, Q(1, 4), Q(1, 2))
+        elif case == 10:
+            check_matrices([[[Q(2), Q(0)], [Q(0), Q(1)]]], 2)
+        elif case == 11:
+            rounded_trace((), [[[Q(1)]]], [[Q(1, 3)]], 10)
+        elif case == 12:
+            prefix_error((Step("apply", 0),), 4, Q(1), 0)
+        else:
+            validate(((Step("linear", 0, terms=((0, 1 << 129),)),), ()), 2, 1, 1)
+    except ValueError:
+        return
+    raise ValueError(f"control {case} did not reject")
+
+
+def semantic_controls():
+    matrices = cayley((0,), 1, Q(1, 4))
+    initial = [[Q(1024), Q(0)]]
+    side = (Step("apply", 0),)
+    exact = exact_trace(side, matrices, initial)[-1]
+    rounded = rounded_trace(side, matrices, initial, 4)[-1]
+    error = squared_norm([a - b for a, b in zip(exact[0], rounded[0])])
+    need(error > Q(2, 16) ** 2, "omitted coefficient-quantization control")
+    side = (Step("apply", 0), Step("apply", 0, direction=-1))
+    exact = exact_trace(side, matrices, [[Q(1), Q(0)]])[-1]
+    wrong = rounded_trace(side, matrices, [[Q(1), Q(0)]], 100, wrong_inverse=True)[-1]
+    need(squared_norm([a - b for a, b in zip(exact[0], wrong[0])]) > Q(1, 8),
+         "wrong inverse transpose control")
+    alias = (Step("query", 0, src=0),)
+    exact = exact_trace(alias, matrices, [[Q(1), Q(0)]])[-1][0]
+    wrong_first = Q(1) + matrices[0][0][0]
+    wrong_second = matrices[0][1][0] * wrong_first
+    need(exact[1] != wrong_second, "old-value alias control")
+    q, dimension = 12, 4
+    eta = Q(1, 12 ** (q * dimension))
+    need(Q(2 * q * (dimension + 2), 1 << 181) > eta / 4,
+         "one fewer bit must fail the sufficient error inequality")
+    return 4
+
+
+def receipt():
+    paths = sorted(path for path in ROOT.iterdir() if path.is_file())
+    need(len(paths) == 8, "package file inventory")
+    hashes = {}
+    maximum_function = 0
+    for path in paths:
+        size = path.stat().st_size
+        need(size <= 256 * 1024, "package source capacity")
+        payload = path.read_bytes()
+        hashes[path.name] = sha256(payload).hexdigest()
+        if path.suffix == ".py":
+            tree = ast.parse(payload, filename=path.name)
+            compile(tree, path.name, "exec")
+            for node in ast.walk(tree):
+                if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)):
+                    maximum_function = max(maximum_function, node.end_lineno - node.lineno + 1)
+    need(maximum_function <= 60, "function inspection ceiling")
+    return hashes, maximum_function
+
+
+def main():
+    result = finite_program_checks()
+    result.update(product_bound_checks())
+    result["strict_fixture"] = strict_fixture()
+    for case in range(14):
+        reject_invalid(case)
+    result["invalid_controls"] = 14
+    result["semantic_controls"] = semantic_controls()
+    hashes, maximum = receipt()
+    result.update(marker="PASS_EUCLIDEAN_ORTHOGONAL_DETECTOR",
+                  python=platform.python_version(), implementation=platform.python_implementation(),
+                  source_sha256=hashes, maximum_function_lines=maximum)
+    print(json.dumps(result, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()