Bound rounded QQ16 transcript capacity and one-ulp recovery

research/qq16-rounded-transcript-capacity/PROOF.md

@@ -0,0 +1,96 @@
+# Capacity and packing proof
+
+## 1. Quantized observations
+
+Let X be a finite input set and T_p:X -> R^m any deterministic map. Neither
+linearity, continuity nor a computational bound is assumed. Each component
+belongs to2^-(p+g) Z and has absolute value at most R*2^-p, for integers p,g>=0
+and R>=0. A separate record h_p(x) has at most D states. The decoder receives
+only(T_p(x),h_p(x)) and input-independent parameters including p.
+
+Each component's integer numerator lies in[-R*2^g,R*2^g], so has at most
+K=2 floor(R*2^g)+1 values. The complete record has at most C=D*K^m states,
+regardless of dependencies. Branch-dependent use of a fixed tuple is allowed
+if the branch is counted in h and absent slots are padded with0. No uncounted
+branch information or extra source observation is free.
+
+If the demanded real quantity a(x) has N distinct values, exact reconstruction
+requires C>=N by pigeonhole. If N inputs have pairwise demands more than
+2 epsilon apart, recovery within epsilon on every input also requires C>=N:
+two equal transcripts produce the same decoder output, which cannot belong
+to both disjoint closed epsilon balls. This applies to arbitrary nonlinear
+decoders under deterministic worst-case correctness. Randomized average-error
+guarantees are not claimed. The same proof permits p-dependent m,R,g,D.
+
+## 2. Actual bounded dyadic line
+
+Use PR2384's exact four-pair QQ16 model, owner action and66-port set. Put
+f_b(d)=bit_0(db), which is0 or1 at every owner. Its ordinary witness has
+h44=-f25, h49=-f145, h58=-f4, h70=f4, with every other component0.
+Let H=B0 h and P_A be the actual selected injection R_A^T/4 including its
+owner routes. Define w by X_U=h,Y_U=0,X_A=-P_A H,Y_A=P_A H, all other fields0.
+The pinned proof establishes H!=0, B_s h=0 for s=1..8, and the complete zero
+observation trace for the fixed19events. Function-dictionary cancellation
+proves identities at every owner without assuming bit-function independence.
+Payload-constant fields remove translation dependence at any fixed depth.
+
+Set v=2w. The verifier derives its original selected X_A components as
+
+    f145-f4, f145-f25, f4-f25, 0,
+    f145-f4, f25-f145, f25-f4, 0.
+
+Y_A is their negative; ordinary nonzero components are twice signed bit
+functions. Hence v is integer-valued and ||v||_infinity<=2. At the identity
+owner the first original X_A component is1. The granted exact observations
+of tv vanish for every real t by linearity of the retained logical schedule.
+Homogeneous selected controllers also receive zero exact fields. The rounded
+claim still requires their whole retained transcript to obey the stated error
+and capacity contract; unbounded internal state is not free.
+
+For p>=1, take t_k=k*2^-p,0<=k<=2^(p-1). All x_k=t_k v are p-grid inputs
+in the unit box. Their demanded coordinate is t_k, giving
+N_exact=2^(p-1)+1 distinct values. For p>=3 restrict k to multiples of4.
+This gives N_ulp=2^(p-3)+1 inputs with demand spacing4*2^-p>2*2^-p.
+One-ulp approximate recovery therefore requires N_ulp transcript states;
+exact recovery requires N_exact.
+
+## 3. The entire declared tuple
+
+Let W be the finite number of owner/payload points at the chosen depth. No
+estimate of W is required because the source identities hold at every point.
+The initial S values are zero: h is supported on four unread ports. They
+contribute4*2*66=528 complex slots per point. After each of19events, all
+4*2*16=128 selected A/T values and all528 S values vanish. After event1(B1)
+through event18, all4*96=384 completed-X ordinary descendants vanish at18cuts.
+At terminal event18 the completed-X side becomes Y, so that side is observed;
+former-Y final X is excluded. All five eight-component forward histories are
+zero, adding40slots. The overgranted tuple thus has
+(528+19*656+18*384+40)W=19944W complex, or m=39888W real components.
+Duplicated slots can only decrease its capacity.
+
+Let T_p be any rounded/nonlinear implementation of this tuple whose components
+are on the(p+g(p))-grid and differ from their ideals by at most R(p)*2^-p.
+Include every other retained scalar/metadata value in these components or a
+record with at most D_p states. The ideal tuple is zero on our line, so
+section1 proves the README inequalities. The conclusion is independent of
+the arithmetic that produces the residues. This is a necessary interface
+condition, not proof of any particular implementation's R,g,D bounds.
+
+## 4. Eventual failure and deliberate escapes
+
+For fixed W, polynomial R(p), g(p)=O(log p) and log2(D_p)=o(p), we have
+log2(C_p)=o(p), while log2(N_ulp)>=p-3. Eventually C_p<N_ulp. More generally
+the sufficient obstruction is exactly
+
+    log2(D_p)+m(p)*log2(2 floor(R(p)*2^g(p))+1) < log2(N_ulp).
+
+There is no inference when this inequality fails. Fixed-depth asymptotics
+alone do not reject a coupled depth=depth(p), and no useful small-p threshold
+is claimed.
+
+Finer quantization is a real escape: F_p(t)=2^-p*t is injective on our line
+and belongs to the2p-grid, although |F_p(t)|<=2^-p/2 relative to ideal0.
+Here g=p supplies enough states. Likewise T_p=0 plus h_p(t_k)=k is injective
+when D_p is large enough. Early original-A observation detects t directly.
+These controls demonstrate why small absolute error or an exact kernel alone
+does not establish this conclusion. No physical cost is claimed for escapes.

research/qq16-rounded-transcript-capacity/README.md

@@ -0,0 +1,111 @@
+# Rounded residues and the hidden QQ16 input
+
+This extends commdata2338's exact 66-port counterexample
+[PR2384](https://github.com/CrocSwap/integer-mult-bounds/pull/2384) to arbitrary
+nonlinear rounded observations and decoders under an explicit finite-capacity
+contract. Subexponential transcript capacity cannot reconstruct its bounded
+dyadic hidden line, even to one input ulp. This does not certify an actual
+rounded controller's error bound or reject a changed observation contract.
+
+For a fixed owner/payload domain of size W, the overgranted tuple below has
+m=39888W real components. Suppose each component lies on the (p+g)-bit
+fractional grid, within R(p)*2^-p of its ideal value, and all other retained
+metadata has at most D_p states. Then its capacity is at most
+
+    C_p = D_p * (2 floor(R(p) 2^g) + 1)^m.
+
+Exact recovery requires C_p >= 2^(p-1)+1. Recovery with worst-case absolute
+error at most2^-p requires C_p >= 2^(p-3)+1 for p>=3. Fixed W, polynomial R,
+g=O(log p), and log2(D_p)=o(p) therefore fail eventually. There is no claimed
+useful small-p threshold: W can be enormous. For growing depth/count use the
+exact capacity inequality in [PROOF.md](PROOF.md), not the fixed-W corollary.
+
+## Complete declared observation boundary
+
+Fix the retained19-event QQ16 logical schedule, A/T/U partition, four X/Y pair
+banks, and PR2384's66ordinary read ports S. At every owner/payload point grant:
+
+| Observations | Complex scalar slots |
+| --- | ---: |
+| Initial X/Y values on S, all four pairs | 528 |
+| All A/T and S values after each of19events | 19*(128+528)=12464 |
+| Completed-X ordinary descendants after events1 through18 | 18*384=6912 |
+| Five eight-component forward query histories | 40 |
+| Total | 19944 |
+
+Indices are zero-based: event0 is F0, event1 is B1. At the terminal rotation,
+completed X is the new Y side. Former-Y final X is not granted. Repeated reads
+of a stored value and deterministic postprocessing add no information. We count
+both real and imaginary components despite the hidden family being real.
+
+This is a complete *defined* contract, not every internal primitive of an
+unspecified native implementation. Any additional retained intermediate value,
+branch identifier, timing information or precision-dependent control record
+must appear among the m components or D_p states. Extra source reads and early
+original-A records change the contract. PR2540/PR2651's early records are an
+explicit escape, not targets of this result.
+
+## Source binding and validation
+
+The predecessor at b9ef408b1cb0fcd34ab1f1bdbe645573d5de188f is retained
+byte-for-byte in vendor/pr2384 with its notice. Its verifier authenticates six
+main inputs and two archive members, proves all-owner routes and the19-event
+zero transcript, and rejects eight controls. We replay its complete receipt
+before deriving the integral hidden line and observation ledger; the wrapper
+only redirects its source root to this checkout.
+
+The line is v=2w for that exact witness. Its nonzero ordinary fields have
+coefficients {-2,-2,-2,+2} on ports{44,49,58,70}. Its original selected fields
+also have integral coefficients and coefficient L1 norm at most2. Original
+A0(identity)=1. Thus x_k=k*2^-p*v, 0<=k<=2^(p-1), is a unit-box p-grid family
+with zero exact observations and distinct demanded coordinate k*2^-p. The
+fields are constant in payload addresses at any fixed finite depth.
+
+New finite checks cover normalization, the complete slot ledger, one-ulp
+packing, a sharp nine-transcript toy boundary, exact grid-interval counts,
+and two deliberate escapes: finer output precision and extra side metadata.
+The written pigeonhole proof establishes the universal result; finite controls
+do not replace that proof or sample away the all-owner source identities.
+
+Run Python3.12+, standard library only:
+
+```sh
+python3 -I -O -B research/qq16-rounded-transcript-capacity/verify.py
+python3 scripts/research_package.py --package research/qq16-rounded-transcript-capacity
+```
+
+Replay is read-only, works in a Git-free dependency export, and compares the
+complete typed receipt. --write creates a new receipt exclusively.
+[VALIDATION.md](VALIDATION.md) records actual commands and outcomes.
+
+## Scope and family decision
+
+This closes only the bounded-precision nonlinear escape under the specified
+error, quantization, observation and metadata hypotheses. Larger error, finer
+outputs, exponentially many metadata states, a growing observation count,
+extra reads or a changed consumer can escape. No native error theorem, physical
+cost floor, supplier admission, new kappa or multiplication impossibility follows.
+
+Revision5 decision: finish this precision audit and stop. The complete boundary
+is the tuple plus metadata above. Proved quantities are information capacity and
+the source line; the scalar count upper-bounds observation storage. Native work,
+hosting, restoration and actual rounded errors remain unknown, not zero costs.
+The consumer must change the boundary or meet its capacity requirement. This
+does not expand the newer early-record construction.
+
+Base1884c509, priority5, picker93caa43d0e7c6f6fdbd0977d213fdccc. The baseline
+binding command passed before this refinement of uniform-transfer-audit.
+SOURCES.json/TASK.json retain exact provenance, overlap coverage and limitations.
+
+Credit commdata2338(PR2384), kyzer1023(PR2354), adamgall(PR2093),
+AliRomman(PR1969), and the retained joint-query/QQ16 authors. Prepared by ywz65
+with substantial OpenAI Codex assistance in proof, code and writing.
+Apache-2.0; retained notices remain intact.
+
+## Open next questions
+
+Can a specific rounded controller prove a uniform observation error and count
+all metadata at its actual coupled depth/precision? Inventory the emitted
+boundary and bound each component error, then evaluate the exact capacity
+criterion. Until then this is a conditional audit, not rejection of that
+controller. No further exact-linear coefficient census is proposed here.

research/qq16-rounded-transcript-capacity/RESULT.json

@@ -0,0 +1,147 @@
+{
+  "complex_slots_per_point": 19944,
+  "coordinate_l1_bound": 2,
+  "demand_at_identity": 1,
+  "fine_grid_escape": [
+    {
+      "inputs": 5,
+      "p": 3
+    },
+    {
+      "inputs": 9,
+      "p": 4
+    },
+    {
+      "inputs": 17,
+      "p": 5
+    },
+    {
+      "inputs": 33,
+      "p": 6
+    },
+    {
+      "inputs": 65,
+      "p": 7
+    },
+    {
+      "inputs": 129,
+      "p": 8
+    },
+    {
+      "inputs": 257,
+      "p": 9
+    }
+  ],
+  "integer_selected_line": [
+    {
+      "145": "1",
+      "4": "-1"
+    },
+    {
+      "145": "1",
+      "25": "-1"
+    },
+    {
+      "25": "-1",
+      "4": "1"
+    },
+    {},
+    {
+      "145": "1",
+      "4": "-1"
+    },
+    {
+      "145": "-1",
+      "25": "1"
+    },
+    {
+      "25": "1",
+      "4": "-1"
+    },
+    {}
+  ],
+  "packing": [
+    {
+      "exact_inputs": 5,
+      "one_ulp_packing": 2,
+      "p": 3
+    },
+    {
+      "exact_inputs": 9,
+      "one_ulp_packing": 3,
+      "p": 4
+    },
+    {
+      "exact_inputs": 17,
+      "one_ulp_packing": 5,
+      "p": 5
+    },
+    {
+      "exact_inputs": 33,
+      "one_ulp_packing": 9,
+      "p": 6
+    },
+    {
+      "exact_inputs": 65,
+      "one_ulp_packing": 17,
+      "p": 7
+    },
+    {
+      "exact_inputs": 129,
+      "one_ulp_packing": 33,
+      "p": 8
+    },
+    {
+      "exact_inputs": 257,
+      "one_ulp_packing": 65,
+      "p": 9
+    },
+    {
+      "exact_inputs": 513,
+      "one_ulp_packing": 129,
+      "p": 10
+    },
+    {
+      "exact_inputs": 1025,
+      "one_ulp_packing": 257,
+      "p": 11
+    },
+    {
+      "exact_inputs": 2049,
+      "one_ulp_packing": 513,
+      "p": 12
+    }
+  ],
+  "rational_interval_checks": 180,
+  "real_components_per_point": 39888,
+  "rejected_controls": [
+    "unscaled half-integral line is not p-grid integral",
+    "former-Y endpoint is not a zero observation",
+    "omitted imaginary channels are not the declared real tuple",
+    "two-ulp separation does not give disjoint closed balls",
+    "negative radius",
+    "capacity equality is not an impossibility"
+  ],
+  "retained_controls": [
+    "flip coefficient on port 70",
+    "reuse first axis with no original defect",
+    "reverse initial A cancellation sign",
+    "add a read of witness port 44",
+    "omit owner action at one source",
+    "omit cancelling bridge",
+    "wrong F2 bank binding",
+    "observe former-Y terminal output"
+  ],
+  "schema_version": 1,
+  "scope": "conditional finite transcript capacity; no actual rounded error bound or new kappa",
+  "slot_categories": {
+    "completed": 6912,
+    "history": 40,
+    "initial": 528,
+    "post": 12464
+  },
+  "source_head": "b9ef408b1cb0fcd34ab1f1bdbe645573d5de188f",
+  "status": "PASS_QQ16_ROUNDED_TRANSCRIPT_CAPACITY",
+  "toy_capacity": 9,
+  "toy_over_capacity_inputs": 17
+}