Independently check #4436 expanded compiler counts (no new κ)

research/direct-flow-expanded-audit/PROOF.md

@@ -0,0 +1,166 @@
+# Expanded count identity, including source complements
+
+This is an independent check of the counting argument in §3 of zxv's
+[PR4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436).
+The construction and claimed bound belong to that predecessor.
+[PR4476](https://github.com/CrocSwap/integer-mult-bounds/pull/4476) explicitly
+excludes this expanded identity from its width and routing
+audit. The result here concerns finite invocation counts under the declared
+compiler interface, not native correctness or physical execution.
+
+## Assumptions and quantities
+
+Fix an integer base threshold `m >= 2` and one raw rule with rank surplus
+`Delta`. At each rank `n >= m`, a finite local flow has:
+
+- integer source counts `S_s >= 0`, with `1 <= s <= n`, and
+  `S_n = sum_s S_s > 0`;
+- integer exit counts `E_e >= 0`, with `1 <= e < n`;
+- `u_n` raw invocations, each with a positive integer column multiplicity
+  `c`, and `q_n = sum_invocations c`, so `0 <= u_n <= q_n`;
+- the local conservation identity
+
+  ```
+  sum_s S_s*s - sum_e E_e*e = Delta*q_n.                 (1)
+  ```
+
+Source and exit counts include every actual boundary job. In particular,
+unmatched paid jobs are exits. These assumptions are checked on the finite
+fixtures; the general local-flow argument remains attributed to PR4436 and
+its lockstep predecessors.
+
+The new flow counter labels a unit by an ordered word of target slots, with
+`W_k` distinct letters of rank `k`. Words with occurrence vector `a` number
+`multinomial(|a|;a) product_k W_k^a_k`, exactly the predecessor's `u(a)`.
+Deleting the final letter `k` bijects the corresponding parent words with
+the child words at `a-e_k` and their labelled `k` target slots. The two jobs
+have the same rank. They match when both units exist; otherwise the existing
+parent job is an exit or the existing child slot is a source. This is the
+Pascal matching identity without implementing a multinomial point matcher.
+
+Unit existence depends only on depth and the products of target and paid
+letters. Thus summing multiplicities of words with equal products preserves
+these counts, even when different occurrence vectors have the same product.
+Paid paths with equal products still count as separate paths. This quotient
+is for counting; it does not identify their fields or construct a physical
+chronological schedule. The literal ordered-word mode and compressed mode
+use this same correspondence; their comparison is an internal control, not
+a claim of two independent mathematical implementations.
+
+Let `B_n` be productive width, `P_n` the number of rank-one leaves, `U_n`
+the number of raw invocation instances after expansion, and `Q_n` the sum
+of those instances' column multiplicities. Owned storage is excluded from
+`B_n`. Below the threshold, including rank zero, set
+
+```
+B_n = 1,  P_n = n,  U_n = Q_n = 0       (0 <= n < m).
+```
+
+Rank-zero calls are empty programs. Recording or omitting such calls has
+the same counts. For `n >= m`, use the declared nested widths
+
+```
+a_n = B_(n-1),             B_n = a_n*S_n.
+```
+
+The compiler replicates the complete local flow `a_n` times. Each of its
+`a_n*S_s` source arrays also receives its complementary rank-`n-s` job.
+Each of its `a_n*E_e` exits receives a rank-`e` job. A width-`B_r` uniform
+program consumes `B_r` jobs of rank `r`, so the child invocation counts are
+
+```
+C_(n,n-s;source s) = a_n*S_s / B_(n-s),
+C_(n,e;exit e)     = a_n*E_e / B_e.                    (2)
+```
+
+Counts at the same child rank add; source and exit jobs are not identified
+merely because their ranks coincide.
+
+## Integer batching and termination
+
+Every width is a positive integer. For `r >= m`, `B_(r-1)` divides `B_r`
+because their quotient is the positive integer `S_r`; smaller widths are
+one. Hence every `B_r`, `r < n`, divides `a_n = B_(n-1)`. Both quotients
+in (2) are nonnegative integers. Since `s > 0`, a complement satisfies
+`0 <= n-s < n`; exits satisfy `1 <= e < n` by assumption. Thus recursive
+expansion terminates by strict rank descent. The count argument does not
+require a favorable moment exponent.
+
+## Telescoping through every child
+
+Write `sum_child C_r X_r` for the sum over both classes in (2), preserving
+their multiplicities. Complete expansion gives the recurrences
+
+```
+P_n = sum_child C_r P_r,
+U_n = a_n*u_n + sum_child C_r U_r,
+Q_n = a_n*q_n + sum_child C_r Q_r.                    (3)
+```
+
+These count actual repeated invocations, not distinct nodes in a memoized
+dependency graph. In particular, `Q_n` is measured by summing raw columns;
+it is not defined by the rank deficit we are about to prove.
+
+We prove simultaneously, by strong induction on `n`,
+
+```
+B_n*n - P_n = Delta*Q_n,             0 <= U_n <= Q_n. (4)
+```
+
+The base definitions make (4) immediate. At a nonbase rank the total
+productive rank mass supplied to the smaller programs is exactly
+
+```
+sum_child C_r B_r*r
+  = a_n * [sum_s S_s*(n-s) + sum_e E_e*e]
+  = B_n*n - a_n*Delta*q_n,                            (5)
+```
+
+where the last step uses (1). Substitute the induction hypothesis
+`P_r = B_r*r - Delta*Q_r` into the first recurrence in (3), then use
+(5) and the third recurrence. This gives the first identity in (4).
+For the second, each local column is a positive integer, so `u_n <= q_n`;
+combine this with `U_r <= Q_r` in the last two recurrences in (3).
+
+This also justifies a flattened interpreter. Replacing each child reference
+by its finite list of raw instances and rank-one leaves preserves (3).
+Induction on rank therefore proves that a literal expansion and a recursive
+aggregate calculation have identical counts, provided the aggregate keeps
+all invocation multiplicities. Sharing the stored description of a child
+does not authorize sharing its executed instances or productive arrays.
+
+If `Delta > 0`, nonnegative leaf counts now give
+
+```
+U_n <= Q_n = (B_n*n - P_n)/Delta <= B_n*n/Delta.       (6)
+```
+
+The identity in (4) itself does not require positive surplus. Positivity is
+essential for (6): at zero surplus it would divide by zero; at negative
+surplus division reverses inequalities and gives no stated upper bound.
+
+## Why complements and ownership qualifications matter
+
+For the valid rule with one target of rank two and one paid rank-one job,
+`Delta=1`. At rank three its local flow has `S_2=E_1=u_3=q_3=1` and
+`B_3=1`. The complete program has one rank-one complement and one rank-one
+exit, hence `P_3=2`, `Q_3=1`, and `3-2=1`. Omitting the complement would
+give `P_3=1`, `Q_3=1`, and the false identity `3-1=1`. A per-flow mass check
+alone would not expose that compiler omission. Wrong batching factors and
+deduplicated child invocations similarly invalidate the expanded inventory.
+
+If every raw invocation uses at most `O_local` separately owned center
+banks, allocating fresh banks to every expanded instance gives at most
+`O_local*U_n` banks. The one-center case is `U_n`. This is a conditional
+bank-count bound, not a bound on bank capacity, peak-optimal storage, router
+scratch, physical movement or initialization/erasure cost. If an actual
+implementation instead needs a bank per column, `Q_n` is the corresponding
+count. Native ownership and tariffs require their own evidence.
+
+No claim here checks the record grammar, encoded constants, direct exponent
+gate, analytic transfer or a complete multiplication theorem. No kappa is
+changed. Credit zxv for PR4436's construction and count claims, Jacob Alan
+Sussman for the lockstep/Pascal construction, and Ryanson Jonathan for the
+PR4456/PR4476 independent flow, width and routing checks that delimit this
+remaining scope. Prepared for Dillon with substantial OpenAI Codex assistance;
+no independent human or proof-assistant review is claimed. Apache-2.0.

research/direct-flow-expanded-audit/README.md

@@ -0,0 +1,134 @@
+# Independent expanded accounting for the direct mixed compiler
+
+The complete recursive accounting in zxv's [PR4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436)
+passes this independent check. Every source complement and exit receives an
+integer number of smaller uniform batches. Counting their repeated instances
+gives
+
+```
+B_n n − P_n = Δ Q_n,       U_n ≤ Q_n ≤ B_n n / Δ   (Δ > 0).
+```
+
+Here `B` is productive width, `P` counts rank-one paid leaves, `U` counts
+expanded raw invocation instances, and `Q` sums their positive integer column
+multiplicities. [PROOF.md](PROOF.md) gives the induction and its assumptions.
+This corroborates the predecessor's theorem; it is not a new construction or
+κ improvement. In particular, the large example below is not a winning supplier.
+
+## Coverage added
+
+Ryanson Jonathan's [PR4456](https://github.com/CrocSwap/integer-mult-bounds/pull/4456)
+checks individual flow mass and normalized leaf costs.
+[PR4476](https://github.com/CrocSwap/integer-mult-bounds/pull/4476) adds widths,
+routing identities and finite growth measurements, while explicitly excluding
+the fully expanded identity above. This package checks that remaining count
+boundary, including raw instances and column multiplicities that cannot be
+recovered from a normalized leaf count alone.
+
+The checker is separate from the producer. `forest.py` labels units by ordered
+target words, matches the last target letter to a child slot, then counts equal
+products by exact convolution. It does not import the producer's multinomial
+matcher. Individually enumerated words check the compression, including
+collisions such as `2·8 = 4·4`.
+
+`accounting.py` constructs a counted call graph and evaluates every edge with
+its full multiplicity. A second evaluation propagates invocation weights from
+the root toward the leaves. `literal.py` separately builds small programs and
+visits every raw instance, routing slot, leaf and child invocation. These paths
+share the new local forest generator; they are not mutually independent local
+flow implementations. None computes `Q` by rearranging the identity under test.
+The literal traversal is an accounting traversal, not a native execution schedule.
+
+## Exact evidence
+
+All five expanded totals match the immutable predecessor receipt: productive
+width, paid leaves, raw instances, raw column mass and routing slots.
+
+| Domain | Checked scope |
+| --- | --- |
+| Two overlap examples | Every compiled rank through 100; complete final counts match PR4436 |
+| Raw p7, surplus 608 | All 880 nonbase ranks 121–1000; all five rank-1000 totals match |
+| Four small rule families | 44 complete literal expansions, including rank zero |
+| Local source controls | All nine released flow fixtures; five equal-product collision fixtures |
+| Failure controls | 14 named semantic rejections, after source authentication |
+
+The larger literal examples make the difference between `U` and `Q` visible:
+
+| Rule and final rank | Width `B` | Leaves `P` | Instances `U` | Column mass `Q` | Visited records |
+| --- | ---: | ---: | ---: | ---: | ---: |
+| Strict overlap, 13 | 8,192 | 91,904 | 12,544 | 14,592 | 265,025 |
+| Source-open equality, 6 | 3,500 | 18,500 | 1,750 | 2,500 | 71,421 |
+| Separated control, 13 | 6,400 | 51,200 | 10,880 | 16,000 | 202,501 |
+
+The p7 width at rank 1,000 has 17,504 bits. Its complete program is counted
+through an exact finite call graph, not literally enumerated. Full integer
+hashes, counts and rejected faults are in [RESULT.json](RESULT.json).
+Faults include omitted complements/exits, missing replication, deduplicated
+child instances, incorrect raw columns, a missing base leaf and a nonintegral
+batch. Zero and negative surplus reject the division-bound guard.
+
+For a hand-checkable example, a rank-two target with one paid rank-one job has
+`Δ=1`. At rank three the complete program needs a rank-one complement and a
+rank-one exit: `3−2=1`. Omitting the complement gives `3−1≠1`, even though
+the unchanged local flow still passes its own conservation check.
+
+## Reproduction and sources
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/direct-flow-expanded-audit
+python3.12 -I -O -B research/direct-flow-expanded-audit/verify.py
+```
+
+Expected marker: `PASS_DIRECT_FLOW_EXPANDED_ACCOUNTING`. The default recomputes
+and compares the full saved receipt. `--emit` prints a newly computed receipt.
+Direct replay also works from an exported package without Git or network.
+
+`SOURCE-EXPORT.json` records exact original commits, paths, Git blobs and
+SHA256 hashes for the unchanged exports. Their bytes were compared directly
+with the original Git objects before retention. PR4436 is pinned at
+`56003680aee2871773de408e5f01cc5dd46b144c`; PR4476 at
+`4e7022aa9128c8673d3e2024052b2deaa18cb6e4`. `SOURCES.json` additionally pins
+the retained bytes to this contribution's source commit. No pending source
+commit is represented as publication ancestry. The p7 tariff comes from the
+original native receipt; native correctness is inherited, not rechecked.
+
+This work starts from canonical main
+`2a13eb1827784206202db90e5dc8327cf8a250db`, priority revision 7. Live PR and
+bounded Discussion overlap coverage is recorded in `TASK.json`. The later
+[PR4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483) changes
+the height and exponent argument; that theorem is outside this audit.
+
+## Limits
+
+The written induction applies to every finite local flow satisfying its stated
+integer, rank-descent and conservation assumptions. Finite tests corroborate
+the implementation; they are not a formal proof of those assumptions for every
+native caller. An `O_local·U` center-bank bound further assumes at most
+`O_local` separately owned banks per invocation. It does not measure bank
+capacity, peak-optimal storage or extra router scratch.
+
+The record/description grammar, encoded precision constants, native correctness,
+physical movement, ownership, exponent convergence, analytic transfer and full
+multiplication theorem are not verified. No selected-frontier file changes.
+
+## Open next questions
+
+The next useful check is to bind one small expanded program to its actual
+native executor: identify each bank allocation, adapter, movement and erasure,
+and charge all router scratch. That would test whether this accounting model
+matches physical use. The missing native and physical contracts are the blocker;
+larger count scans would not discharge them. Structured details are in `TASK.json`.
+
+## Credit
+
+Prepared by Dillon (@dillona) with substantial OpenAI Codex assistance, including
+separate implementation and mathematical review agents. No independent human
+or formal-kernel review is claimed. Apache-2.0.
+
+Credit zxv for PR4436's construction and expanded-count theorem; Jacob Alan
+Sussman for the lockstep/Pascal compiler; Ryanson Jonathan for PR4456 and PR4476
+and their explicit coverage boundary; Cinna Davis for the raw p7 construction;
+and the native, controller, BIT, Clifford, geometry and outer predecessors
+credited by those sources. Original Sussman LICENSE and NOTICE are retained.