feat(u4): add fixed-symbol occurrence count

knowledge/catalog.json

@@ -934,6 +934,79 @@
         "OP-003"
       ]
     },
+    {
+      "id": "arithmetic/u4-count",
+      "name": "Checked fixed-symbol u4 occurrence count",
+      "class": "arithmetic/word",
+      "summary": "Range-checked u4 batch count for one public generation-time target nibble.",
+      "status": "active",
+      "evidence": "locally-reproduced",
+      "execution": "unclassified",
+      "as_of": "2026-09-17",
+      "knowledge_page": "knowledge/primitives/u4-count.md",
+      "implementation": "src/arithmetic/u4/count.rs",
+      "documentation": "src/arithmetic/u4/README.md",
+      "tests": [
+        "arithmetic::u4::count::tests::counts_boundary_and_repeated_symbols",
+        "arithmetic::u4::count::tests::rejects_invalid_nibbles_and_generation_bounds",
+        "arithmetic::u4::count::tests::preserves_surrounding_main_and_alt_stack_items",
+        "arithmetic::u4::count::tests::counts_nonminimal_numeric_encodings_and_preserves_boundary_state",
+        "arithmetic::u4::count::tests::exact_stack_frontier_admits_max_preserved_and_rejects_one_more",
+        "arithmetic::u4::count::tests::preserved_state_stack_frontier_is_exact",
+        "primitive_metrics::u4_symbol_count_metrics_are_current"
+      ],
+      "references": [
+        "bitcoin-script-locked",
+        "bitcoin-scriptexec-locked"
+      ],
+      "techniques": [
+        "digit-arithmetic",
+        "constant-embedding",
+        "range-check"
+      ],
+      "security": "Every hostile nibble is range-checked before equality scans; the target is public generation-time data, the numeric count is bounded by the batch length, and no terminal predicate is supplied.",
+      "stack_contract": "Consumes preserved | nibble[0] ... nibble[n-1] and returns preserved | count(target), with the last input on top and count in 0..=n.",
+      "configurations": [
+        {
+          "id": "checked-target-zero-batch16",
+          "label": "u4_nibbles_count(0, 16)",
+          "parameters": {
+            "nibble_count": 16,
+            "target": 0,
+            "input_check": true,
+            "data_items": 16,
+            "hint_items": 0
+          },
+          "includes": "fragment-only: 16 numeric range checks, 16 numeric target-equality tests, count accumulation, and input cleanup; witness_bytes and witness_bytes_max describe the canonical 16-item profile, not larger accepted nonminimal encodings; excludes input pushes, witness serialization, terminal predicate, unrelated live state, and transaction context",
+          "script_bytes": 266,
+          "witness_bytes": 33,
+          "witness_bytes_max": 33,
+          "max_stack_items": 19,
+          "executed_opcodes": null,
+          "validation_weight": null,
+          "setup_script_bytes": 0,
+          "per_use_script_bytes": 266,
+          "metric_keys": [
+            "u4_symbol_count_16",
+            "u4_symbol_count_16_witness",
+            "u4_symbol_count_16_stack",
+            "u4_symbol_count_16_opcodes"
+          ],
+          "static_non_push_opcodes": 186
+        }
+      ],
+      "limitations": [
+        "The equality scan is linear in batch length for one target",
+        "Counts one public target rather than returning a complete histogram",
+        "Static non-push opcode count is not a dynamic execution measurement",
+        "No Bitcoin Core consensus or relay-policy validation"
+      ],
+      "open_problems": [
+        "OP-001",
+        "OP-002",
+        "OP-003"
+      ]
+    },
     {
       "id": "arithmetic/u4-trichotomy",
       "name": "Checked u4 embedded-threshold trichotomy",

knowledge/comparisons/arithmetic.md

@@ -54,6 +54,7 @@ the current byte-oriented and decode/re-encode configurations below.
 | 32 checked nibbles to nonzero-power-of-two bits | `u4_nibbles_to_power_of_two(32)` | 440 | 50-item peak; one predicate bit per input |
 | 32 checked nibbles to modulo-three residues | `u4_nibbles_to_mod3(32)` | 440 | 50-item peak; one residue per input |
 | 32 checked nibbles to parity bits | `u4_nibbles_to_parity(32)` | 440 | 50-item peak; one output bit per input |
+| Fixed-symbol u4 occurrence count | `u4_nibbles_count(0, 16)` | <!-- metric:u4_symbol_count_16 -->266<!-- /metric:u4_symbol_count_16 --> | <!-- metric:u4_symbol_count_16_stack -->19<!-- /metric:u4_symbol_count_16_stack -->-item peak; one count output; target embedded; numeric equality |
 | 32 checked nibbles transition count | `u4_nibbles_transition_count(32)` | 588 | 35-item peak; 391 static non-push opcodes; one compact count; no table |
 | 32 checked nibbles to adjacent-equality bits | `u4_adjacent_equal_mask(32)` | 558 | 64-item peak; 31 output bits; 361 static non-push opcodes; no lookup table or hints |
 | Checked odd u4 inverse | `u4_odd_inverse_mod16` | 9 | 20-item peak; 16-item table; one data item; zero hints |

knowledge/primitives/index.md

@@ -21,6 +21,7 @@ the source. Read a page together with its comparison page and evidence record.
 - [Checked u4 nonzero-power-of-two predicate](u4-power-of-two.md)
 - [Checked u4 modulo-three projection](u4-mod3.md)
 - [Checked u4 parity projection](u4-parity.md)
+- [Checked fixed-symbol u4 occurrence count](u4-count.md)
 - [Checked u4 transition count](u4-transition-count.md)
 - [Checked u4 adjacent-equality mask](u4-adjacent-equality.md)
 - [Checked odd u4 inverse modulo 16](u4-odd-inverse-mod16.md)

knowledge/primitives/u4-count.md

@@ -0,0 +1,41 @@
+# Checked fixed-symbol u4 occurrence count
+
+`arithmetic::u4::count::u4_nibbles_count` consumes a batch of checked u4
+nibbles and returns the number of occurrences of one generation-time target
+nibble. The result is a numeric ScriptNum in `0..=n`; the target is public
+locking-script data.
+
+## Boundary and comparison
+
+Every hostile input is range-checked before the numeric equality scans. The
+target is validated at script-generation time and must be in `0..=15`. The
+operation accepts nonminimal numeric encodings when the execution profile
+permits them, preserves unrelated lower main-stack and alt-stack state, and
+consumes only the input batch. A standalone batch is limited to 997 items;
+composition must satisfy `n + 3 + preserved_items <= 1000`. Strict local frontier
+tests measure a 1,000-item peak at the maximum for batches 1, 16, 500, and
+997 and with preserved main/alt items, and reject one more live item with
+`StackSize`.
+
+The representative configuration counts target `0` across 16 canonical
+one-byte witness nibbles. It includes all range checks, numeric equality tests,
+Boolean-to-count additions, and input cleanup; it excludes input pushes, the
+terminal predicate, unrelated live state, and transaction context. The 33-byte
+witness figure is the canonical 16-item profile, not a maximum over accepted
+nonminimal encodings. No hints are required.
+
+Evidence is `locally-reproduced`; execution is `unclassified`. The strict local
+executor enforces the combined 1,000-item stack limit. No Bitcoin Core
+consensus or relay-policy validation is claimed.
+
+This is a fixed-alphabet counting primitive, not a packed histogram or a
+duplicate detector by itself. Callers can compare the count to zero, one, or a
+protocol-specific bound.
+
+## Reproduction
+
+```sh
+cargo test --locked arithmetic::u4::count::tests --lib
+cargo test --locked --test primitive_metrics u4_symbol_count_metrics_are_current -- --exact
+python3 tools/kb.py validate
+```

src/arithmetic/u4/README.md

@@ -12,6 +12,9 @@ these operations, but this module contains no hash-specific round logic.
   `1..=3` bit counts unless their function documents otherwise.
 - `parity::u4_nibbles_to_parity(nibble_count)` takes a checked batch size in
   `1..=982`.
+- `count::u4_nibbles_count(value, nibble_count)` takes a checked batch size in
+  `1..=997` without preserved stack items; composition must satisfy
+  `nibble_count + 3 + preserved_items <= 1000`.
 - `cyclic_equality::u4_nibbles_to_cyclic_equality(nibble_count, offset)` takes
   a checked batch size in `1..=499` and returns a wrapped equality bit per
   input nibble.
@@ -146,6 +149,7 @@ each input with the same output-restoration boundary.
 | `lexicographic_le(128)` | <!-- metric:u4_lexicographic_le_128 -->7500<!-- /metric:u4_lexicographic_le_128 --> bytes | <!-- metric:u4_lexicographic_le_128_stack -->259<!-- /metric:u4_lexicographic_le_128_stack --> items | <!-- metric:u4_lexicographic_le_128_opcodes -->4354<!-- /metric:u4_lexicographic_le_128_opcodes --> |
 | `lexicographic_le_constant(128)` | <!-- metric:u4_lexicographic_le_constant_128 -->7628<!-- /metric:u4_lexicographic_le_constant_128 --> bytes | <!-- metric:u4_lexicographic_le_constant_128_stack -->259<!-- /metric:u4_lexicographic_le_constant_128_stack --> items | <!-- metric:u4_lexicographic_le_constant_128_opcodes -->4354<!-- /metric:u4_lexicographic_le_constant_128_opcodes --> |
 | Checked parity batch, 32 nibbles | <!-- metric:u4_parity_batch32 -->440<!-- /metric:u4_parity_batch32 --> bytes | <!-- metric:u4_parity_batch32_stack -->50<!-- /metric:u4_parity_batch32_stack --> items | <!-- metric:u4_parity_batch32_opcodes -->328<!-- /metric:u4_parity_batch32_opcodes --> |
+| Fixed-symbol count, 16 nibbles | <!-- metric:u4_symbol_count_16 -->266<!-- /metric:u4_symbol_count_16 --> bytes | <!-- metric:u4_symbol_count_16_stack -->19<!-- /metric:u4_symbol_count_16_stack --> items | <!-- metric:u4_symbol_count_16_opcodes -->186<!-- /metric:u4_symbol_count_16_opcodes --> |
 | Checked cyclic equality batch, 32 nibbles, offset 7 | <!-- metric:u4_cyclic_equality_batch32 -->569<!-- /metric:u4_cyclic_equality_batch32 --> bytes | <!-- metric:u4_cyclic_equality_batch32_stack -->65<!-- /metric:u4_cyclic_equality_batch32_stack --> items | <!-- metric:u4_cyclic_equality_batch32_opcodes -->368<!-- /metric:u4_cyclic_equality_batch32_opcodes --> |
 | Checked transition-count batch, 32 nibbles | <!-- metric:u4_transition_count_batch32 -->588<!-- /metric:u4_transition_count_batch32 --> bytes | <!-- metric:u4_transition_count_batch32_stack -->35<!-- /metric:u4_transition_count_batch32_stack --> items | <!-- metric:u4_transition_count_batch32_opcodes -->391<!-- /metric:u4_transition_count_batch32_opcodes --> |
 | Checked adjacent-equality batch, 32 nibbles | <!-- metric:u4_adjacent_equal_batch32 -->558<!-- /metric:u4_adjacent_equal_batch32 --> bytes | <!-- metric:u4_adjacent_equal_batch32_stack -->64<!-- /metric:u4_adjacent_equal_batch32_stack --> items | <!-- metric:u4_adjacent_equal_batch32_opcodes -->361<!-- /metric:u4_adjacent_equal_batch32_opcodes --> |
@@ -204,6 +208,8 @@ generated table setup is <!-- metric:u4_odd_inverse_mod16_table -->16<!-- /metri
 <!-- metric:u4_popcount_total_batch32_witness -->65<!-- /metric:u4_popcount_total_batch32_witness --> serialized witness bytes for the representative checked total-popcount batch.
 
 
+The fixed-symbol count fixture uses <!-- metric:u4_symbol_count_16_witness -->33<!-- /metric:u4_symbol_count_16_witness --> serialized witness bytes for <!-- metric:u4_symbol_count_16_witness_items -->16<!-- /metric:u4_symbol_count_16_witness_items --> canonical data items and returns one numeric count. Nonminimal numeric encodings may be accepted under a permissive execution profile and can serialize larger.
+
 <!-- metric:u4_parity_batch32_witness -->65<!-- /metric:u4_parity_batch32_witness --> serialized witness bytes for the representative parity batch.
 <!-- metric:u4_msb_batch32_witness -->65<!-- /metric:u4_msb_batch32_witness --> serialized witness bytes for the representative MSB batch.