Audit fresh-row conditioning in the selected stopped cover

research/selected-cover-fresh-fibers/README.md

@@ -0,0 +1,243 @@
+# Fresh row fibers in the selected stopped cover
+
+**A conditional all-depth address theorem and adversarial audit; no new κ.**
+A large enough row reserve and a restored row endpoint are not, by themselves,
+enough to justify per-edge bad-class averaging. This package proves the missing
+counting implication under the inherited **fresh-field** contract, maps that
+contract to the selected bit producer's source, and gives exact counterexamples
+when either invocation predictability or complete padded execution is removed.
+It does not assert that the selected compiler violates either condition.
+
+## Selected object and source boundary
+
+The scientific base is `564148b82ae9df72163f22106f15e73efca8aff2`, selected #1094,
+κ = `836330098538459/500000000000000000`. The ordinary stopped producer is the
+selected **PR589 bit supplier**, not the complex supplier of dimension 73.
+The frozen PR1087 assembler binds PR589's record by Git blob
+`e293ddc557742637f9f679f083a1a282d87b1b13` and SHA256. It gives nine stages,
+32 replicas, moment dimension `m=1+7*9=64`, live roles `28416`, physical roles
+`28425`, maximum child rank `42`, and the full paid histogram in `RESULT.json`.
+The seven native and seven conservative bootstrap stages use the same bit word;
+only their scalar bootstrap parameter differs. No cutoff arithmetic is repeated.
+
+The actual selected finite record is linked through the selected assembly, not
+identified by a similarly named historical package. The checker authenticates
+all source bytes before parsing, including the archived assembler member. No
+predecessor Python is imported or executed. `SOURCES.json` pins the proof texts
+and the source chain. These texts retain an all-size compiler hypothesis: the
+finite PR589 record is **not** an execution trace over every input width.
+
+### Exact source-to-hypothesis map
+
+The line numbers below refer to the pinned files, not moving web text.
+
+| Source | What it supplies | Use here / what remains conditional |
+|---|---|---|
+| `five-stage-source527-banks/proof/three-stage-cover-bit.tex` 9–15 | weights may read exposed ancestor rows, never fresh invocation roles or data; complete spectators and row restoration | invocation parameters are fixed on each ancestor cylinder; inherited compiler must implement this restriction |
+| same, 32–44 | current routing changes fresh fields; right multiplication changes chart, not the endpoint | current-role routing is a bijection independent of unused descendant stock |
+| same, 122–145 | child weight `A_child[kf+j]=A[i_k f+j] D_P[k]`; parent's current fields become child ancestors; child's roles use disjoint stock | a parent's low-residue/pivot choice may select a child, but may not select using that child's future role coordinate |
+| same, 161–195 | fallback pivot choices use the parent's low class; resulting children have their own descriptor | adaptive fallback is permitted at the **next** depth: its choice is already an ancestor value there |
+| same, 197–218 | `GL_m(Z/q^w Z)` chart `g=g0+qG1`, batched high matrices, role divisor | every low matrix has the same number of high lifts; physical-role factor cancels in the density, not in stock |
+| same, 220–228 | per-edge polynomial bad fraction `2m^3/q`, no simultaneous union bound | justified by complete fibers and a fixed list of edge occurrences at each invocation, not by endpoint restoration alone |
+| `three-stage-cover-rows.tex` 1–15, 29–60 | stock `W(w)^D`, fresh descendant fields, one outer row padding, completed row restoration | supplies the row-layout and return contract to which the theorem below applies |
+| retained PR185 proof, 36–44 | completed inner ordinary leaves borrow internally and return outer spectators | their internal digits are not additional external role factors; their compiler contract is retained |
+| frozen PR1087 `code/assemble.py`, `BIT_L/BIT_T`, `load_bit`, `outer_witness` | the selected PR589 record, dimension 64 and finite bootstrap use | binds this audit to the selected supplier; does not prove its all-size read/write discipline |
+
+The old note's example has dimension 67. We use its **stated structural
+contract**, not its old histogram, depth constant, or row coefficient. The
+selected finite dimension/profile come from PR589. Portability of the contract
+to that selected implementation remains explicitly conditional, as in the
+selected review. The new result discharges an implication of that contract;
+it does not discharge all-size compiler admission.
+
+## One-padding conditional-fiber theorem
+
+Fix integers `W>=2`, `D>=1`, and a genuine row range `Q>=S=W^D`. Let
+
+```
+T = ceil(Q/S),       P = T*S.
+```
+
+Pad **once**, from `[Q]` to `[P]`, and execute over the entire padded range.
+Euclidean division is a bijection
+
+```
+[P] <-> [T] × [W]^D,
+x = (((t*W + r_0)*W + r_1)*W + ...)*W + r_(D-1).
+```
+
+At depth `j`, the slab `t` and fields `r_0,...,r_(j-1)` are ancestors,
+`r_j` is current, and the remaining fields are unused stock. The exact
+hypotheses at every invocation boundary are:
+
+1. The decision that this invocation exists, its width, its fixed edge list and
+   its weights depend only on its ancestors (and fixed program indices), not on
+   current/future row fields or data. An ancestor-dependent union of cylinders
+   is allowed. A child selected by a parent's current residue satisfies this
+   rule because that field has become a child ancestor.
+2. Each current-role route fixes ancestors and unused stock and acts as a
+   permutation of `[W]` depending only on ancestors. In particular, no unused
+   stock value selects that permutation.
+3. Calls have depth at most `D`; a completed child restores its supplied row
+   field and preserves ancestor spectators before a sequential sibling uses
+   it. The ordinary leaf may borrow internally under its own completed contract.
+4. The padded rows are not pruned by the genuine/dummy flag during execution.
+   Only a completed row-restoring endpoint restricts back to `[Q]`.
+
+**Conclusion.** Every live invocation domain is a disjoint union of complete
+suffix cylinders. On fixing one ancestor prefix, each value of its current
+role occurs exactly `W^(D-j-1)` times. Every low type in an equal-fiber
+partition of that current role has its stated uniform frequency. There is
+no per-recursion padding factor: `Q <= P < Q+S <= 2Q`, with `P<2Q` also when
+`Q=S`. The original genuine range is invariant at the completed endpoint.
+
+**Proof.** The root is a full product by Euclidean division. Suppose the claim
+holds at a node. Hypothesis 1 selects entire ancestor cylinders, never a
+proper subset of the fresh suffix. Hypothesis 2 permutes the current factor
+and fixes all later factors, so preserves the full suffix product and its
+counting measure. At a child boundary, fixing the parent's current field
+merely fixes one more prefix coordinate; every later factor remains complete.
+This proves the assertion by induction to depth `D`, including prefix-dependent
+stopping and fallback. Hypothesis 3 restores the child row before reuse, so
+sequential siblings start with the same product rather than consuming or
+multiplying the reserve. The two ordinary-body calls likewise reuse it.
+For padding, `ceil(Q/S)<Q/S+1` gives `P<Q+S<=2Q`; if equality `Q=S` is used
+in the last comparison, actually `P=Q`. At the completed outer endpoint every
+row coordinate is fixed, so the subset `x<Q` is preserved and padding can be
+removed. This last argument does **not** assert that `[Q]` was a complete-fiber
+execution domain at intermediate cuts. ∎
+
+This is an address-counting proof, not an assumption that arbitrary program
+maps preserve a uniform random distribution. There is no random input model.
+The volume is counted over complete address fibers, including padded rows.
+
+## Selected low-residue averaging and full unchanged bill
+
+For the selected cover, use
+
+```
+W(w) = 28425 * |GL_64(Z/q^w Z)|,
+|GL_64(Z/q^w Z)| = |GL_64(F_q)| * q^(4096*(w-1)).
+```
+
+Every lift `g0+qG1` of an invertible low matrix is invertible, and an invertible
+matrix reduces to an invertible low matrix (determinant is a unit iff its
+reduction is nonzero). Thus each low matrix has exactly `q^(4096*(w-1))`
+lifts. Right multiplication by an invertible route is a bijection on the
+whole group and on low classes, so it preserves this equal-fiber statement.
+The role factor `28425` is independent and cancels. These statements hold for
+**every eligible prime q and every w>=1**, not just the small test rings.
+
+Fix an odd prime `q>2^80` before choosing input widths, avoiding the fixed
+rational denominators and rank witnesses of the selected geometry, as required
+by the inherited cover contract. This is what **eligible** means here; the
+finite profile alone does not certify that prime-selection contract. Fix any
+invocation's ancestor prefix and any one of its edge occurrences. The source's
+bad-minor set then has fraction at most `b=2*64^3/q < 10^-16`.
+By the theorem, this remains its frequency at the invocation. Sum costs over
+edge occurrences and then ancestor prefixes. Linearity of a finite sum, not
+independence of bad events, gives the surcharge. There is no need to bound the
+probability that *some* edge fails, and no simultaneous union bound. Arbitrary
+correlation between the bad sets of two fixed edges is harmless.
+
+With selected histogram `H`, `E=sum_r H_r`, `L=28416` and exponent `a`, retain
+exactly the selected conservative charge
+
+```
+(1/L) * sum_r H_r*(r/64)^(1-a)
+  + (1/10^16) * (32*64^2) * E/L * (1/64)^(1-a).
+```
+
+Every good term stays charged; no displaced-good subtraction is taken. One
+outer factor `P/Q<2` is a volume constant, **not** a factor inserted into the
+characteristic moment at each level. This audit derives neither a new endpoint
+nor a new reserve coefficient. The first-stage fit envelope, H2 time bound,
+selected compiler, precision/tape and analytic-transfer obligations remain.
+
+## Two failures that row restoration cannot detect
+
+**Current-field adaptive edge choice.** Over `GL_2(F_q)`, index edge predicates
+by the `q+1` projective lines `[v]` and let `B_v={g : first_row(g)·v=0}`.
+Every fixed `B_v` has fraction `1/(q+1)`: each nonzero first row has exactly one
+kernel line, and invertible change of basis permutes the line fibers. Choose
+`v` to be the kernel of the **current** first row. The selected edge is then
+bad on every matrix. Identity routing and the identity final row map remain
+legal bijections; the sole missing hypothesis is that the edge choice be fixed
+before reading that invocation's current role. This is a linear-minor example,
+not an arbitrary rare-set oracle. It does not allege such a choice in PR589.
+
+**Skipping dummy rows.** Take `W=3`, `D=2`, `S=9`, `Q=10`, `P=18`. The complete
+padded slab `t=1` has three values of `r_0`, each with three values of `r_1`.
+In the genuine prefix `[10]`, the cylinder `(t,r_0)=(1,0)` contains only
+`r_1=0`. The event `r_1=0` has conditional frequency one rather than one third.
+All routes can be identity and the final row map can restore every row. Thus
+endpoint restoration justifies **unpadding**, not pruning intermediate
+invocations. The package checks these two failures separately.
+
+## Reproduction and evidence limits
+
+```
+uv run --python 3.12 --no-project python -I -B research/selected-cover-fresh-fibers/verify.py
+uv run --python 3.12 --no-project python -I -O -B research/selected-cover-fresh-fibers/verify.py
+uv run --python 3.12 --no-project python scripts/research_package.py --package research/selected-cover-fresh-fibers
+```
+
+Observed local Python 3.12 smoke and registered optimized replay:
+
+```
+PASS_SELECTED_COVER_FRESH_FIBERS cases=60 cuts=150 GL_rings=4 controls=9
+PASS_REGISTERED_RESEARCH_PACKAGE research/selected-cover-fresh-fibers outcome=completed
+```
+
+The 60 mixed-radix cases cover 14,120 padded rows and 2,370 conditional
+fibers. The four full small-ring enumerations are `GL_2` over moduli
+`3,9,5,25`; the adaptive-minor witnesses use primes `3,5,7`. These finite
+domains are explicitly separate from the universal written theorem.
+
+`RESULT.json` is required and compared with a fresh canonical JSON object.
+Explicit `--write-result PATH` creates a new external receipt without
+silently replacing an existing file. Exact finite checks exercise mixed-radix
+round trips, prefix-dependent bijections and stopping, all low-matrix fibers
+of the stated small prime-power rings, both counterexamples, and semantic
+mutations. Acceptance uses explicit exceptions, not Python assertions.
+Finite runs support the implementation; the all-depth and all-width statements
+come from the written proofs above. No whole supplier cold replay, formal
+kernel run, or hosted CI result is claimed.
+
+## Open next questions
+
+1. **Emit the selected all-size field-dependency certificate.** The concrete
+   remaining obligation is that every call guard/edge-list/weight read set is
+   contained in its ancestor fields and every route fixes unused descendant
+   fields. Start from the child-weight formula and the current chart route,
+   then annotate the selected emitter's all-size lowering. This is blocked by
+   that lowering remaining an inherited contract rather than an emitted
+   address-level artifact; stock magnitude and scalar endpoint checks cannot
+   substitute for it.
+2. **Admit a deliberately adaptive selector only with its new charge.** If a
+   changed controller chooses an edge after reading current low residues,
+   compute the fiberwise sum of its chosen bad indicators instead of reusing
+   the fixed-edge average. Start with a finite partition of low classes. The
+   obstacle is a favorable fully paid bound, not the mere existence of a
+   row-restoring permutation. This result supplies no such improved selector.
+
+## Attribution and provenance
+
+The source's GL chart, weighted child rule, fresh-role restrictions and per-edge
+polynomial bound belong to the retained three-stage-cover framework; its
+source527 packaging and finite accounting are credited to eumemic. Rohan Arun
+supplied the PR185/PR387 bootstrap lineage and selected PR1094 assembly;
+Jeremy Kothe supplied the pinned PR1087 assembler. PR589's tuned bit supplier
+retains its credited punctured-E8, nine-stage and hosting lineage. Josie
+Elliston's PR1956/1965 and ToikY's PR1990 isolate the stock-fit question; this
+package does not claim their cutoff results. `r480-sharp-charge535` and its
+PR461/464/465 predecessors already sharpen the numerical bad-class charge;
+no such numerical refinement is claimed here.
+
+Prepared for Adam Gall with substantial OpenAI Codex assistance in mathematics,
+code and writing. Apache-2.0. No independent human review is claimed. Selection
+nonce `cc5bf62436a3476502c7769e29c2990c`, adversarial-audit, priority revision 4;
+`SELECTION.json` preserves the one original draw. The checked upstream
+checkpoint `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` changes guidance only;
+scientific inputs are retained at the original base. Live/cached overlap
+coverage and its limitations are recorded in `TASK.json`.

research/selected-cover-fresh-fibers/RESULT.json

@@ -0,0 +1,143 @@
+{
+  "adaptive_minor_counterexamples": [
+    {
+      "adaptive_bad_fraction": "1",
+      "edges": 4,
+      "fixed_bad_fraction": "1/4",
+      "matrices": 48,
+      "prime": 3,
+      "row_map": "identity"
+    },
+    {
+      "adaptive_bad_fraction": "1",
+      "edges": 6,
+      "fixed_bad_fraction": "1/6",
+      "matrices": 480,
+      "prime": 5,
+      "row_map": "identity"
+    },
+    {
+      "adaptive_bad_fraction": "1",
+      "edges": 8,
+      "fixed_bad_fraction": "1/8",
+      "matrices": 2016,
+      "prime": 7,
+      "row_map": "identity"
+    }
+  ],
+  "address_audit": {
+    "cases": 60,
+    "conditional_fibers": 2370,
+    "cuts": 150,
+    "depths": [
+      1,
+      4
+    ],
+    "padded_rows": 14120,
+    "widths": [
+      2,
+      6
+    ]
+  },
+  "genuine_prefix_counterexample": {
+    "D": 2,
+    "W": 3,
+    "ancestor": [
+      1,
+      0
+    ],
+    "genuine": 10,
+    "genuine_bad_fraction": "1",
+    "genuine_fresh_values": [
+      0
+    ],
+    "padded": 18,
+    "padded_bad_fraction": "1/3",
+    "stock": 9
+  },
+  "gl2_low_fibers": [
+    {
+      "lifts_per_low_class": 1,
+      "low_classes": 48,
+      "matrices": 48,
+      "power": 1,
+      "prime": 3
+    },
+    {
+      "lifts_per_low_class": 81,
+      "low_classes": 48,
+      "matrices": 3888,
+      "power": 2,
+      "prime": 3
+    },
+    {
+      "lifts_per_low_class": 1,
+      "low_classes": 480,
+      "matrices": 480,
+      "power": 1,
+      "prime": 5
+    },
+    {
+      "lifts_per_low_class": 625,
+      "low_classes": 480,
+      "matrices": 300000,
+      "power": 2,
+      "prime": 5
+    }
+  ],
+  "limits": [
+    "All-depth theorem uses the written prefix/complete-domain hypotheses.",
+    "Selected all-size field dependency graph remains an inherited compiler obligation.",
+    "No stock coefficient, improved root, new supplier or multiplication theorem.",
+    "Finite matrices are GL2 controls, not enumeration of selected GL64."
+  ],
+  "negative_controls_rejected": [
+    "current_route_reads_future",
+    "nonbijective_current_route",
+    "ancestor_future_alias",
+    "pruned_padded_domain",
+    "adaptive_edge_at_fixed_edge_charge",
+    "omitted_selected_edge",
+    "live_stock_substituted_for_physical",
+    "source_byte_corruption",
+    "unrestored_row_at_unpadding"
+  ],
+  "selected": {
+    "bad_fraction_retained": "1/10000000000000000",
+    "complete_moment_at_a_zero": "2874298095721977/2890625000000000",
+    "deficit": 10272,
+    "edges": 904896,
+    "fallback_coefficient_before_rank_power": "4713/11291503906250",
+    "fallback_per_bad_edge": 131072,
+    "live_roles": 28416,
+    "m": 64,
+    "max_child": 42,
+    "physical_roles": 28425,
+    "profile": {
+      "1": 381024,
+      "2": 400416,
+      "3": 22752,
+      "4": 26880,
+      "42": 288,
+      "5": 29376,
+      "6": 17376,
+      "7": 26784
+    },
+    "rank_mass": 1808352,
+    "scope": "Existing selected bill only; no new moment root or stock coefficient."
+  },
+  "source_sha256": {
+    "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+    "research/bootstrap-depth-audit/sources/pr387/bootstrap-sources/research/community-round8-audit/pr185-proof-reviewed.md": "bbac6ec77f315dd76324f4595b8c7a9b0ec719f3903d0c56c61f23990326e8fa",
+    "research/community-frontier1094-audit/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045",
+    "research/complex-t16-rare-pattern-exchanges/SOURCE.json": "4cfd44cebfe88f4450294239fbea8feecb564338dc3027b76065227f5d19cb6f",
+    "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz": "d4acf04daef85d4514f80ec5fcd2492d0c60e5d6c49fa71b3e6523f8db2dea86",
+    "research/complex-t16-rare-pattern-exchanges/upstream1087.tar.gz:code/assemble.py": "15f6986a476bac76bcdc0bfcf51da115389b46f1950d2766b6822f757888b13a",
+    "research/e8-bit-p111-tuned/tune/EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4",
+    "research/five-stage-source527-banks/proof/three-stage-cover-bit.tex": "47123a756f823c83a0d48cca2bf5add6472cd88410b13aed345e70c8834fb511",
+    "research/five-stage-source527-banks/proof/three-stage-cover-rows.tex": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8",
+    "research/r480-sharp-charge535/README.md": "28355cfc614358eb482d018ba7b21addb0725520fbcd148a0f0f0faaabd03209",
+    "research/selected-bootstrap-stock-audit/README.md": "0f3cda98c8382d41dc4f5d905460a4b4ed2854d6f94f20035b150e14825827c6"
+  },
+  "status": "PASS_SELECTED_COVER_FRESH_FIBERS"
+}