[chris-ai1]

Proves strict containment between arbitrary exact-advice classes when the upper bound is pointwise larger and eventually at most the n-bit truth-table capacity. Neither bound nor advice must be computable. A fixed native polynomial-time decoder reads a binary-indexed advice bit using an advice-length cap; finite counting and countability diagonalization supply the separating language. Includes the positive one-bit predecessor hierarchy, every constant-advice hierarchy and strict P/1 versus P/poly.

Maps Goldreich’s official tighter Theorem4.1 addendum and the positive-gap, upper-capacity versions of draft Exercise3.3/Theorem4.1 (Exercise3.3 places upper capacity in its guideline). The complete-pair polynomial clock, exact/no-exception convention, eventual capacity, zero-based indexing and positivity are explicit. The unqualified nonnegative-gap draft reading remains subject to #4890’s counterexample; no arbitrary-time or finite-error separation is claimed. Advances #4772, stacked on #4890 at317d18039296ecb68bd038facb7f71feb3392ee6; the book-wide objective remains open.

Validation: strict hierarchy modules, AdviceHierarchy clients and Entries build pass; aggregate generation/check, manual checker/72 tests, hygiene, both readability ratchets and whitespace pass. Clients extract two-bit and five-bit separating languages and check P/0, zero predecessor and exponential-capacity boundaries. Local statement comparison found no duplicate among four theorems but omitted4355 modules without outputs; the four-proof source-copy scan found no repeats. Changed-file lints could not complete because an unrelated root ilean was missing. Hosted full CI and actual advisories remain required. Independent source/API/client/manual-source review approved at the current head; final outside readiness/rendered review is still required.

Manual impact: Operator chapter documents imports, hypotheses, decoder/resource conventions and complete checked clients/build command. Goldreich audit and result registry map exact source endpoints and limitations. Agent Operator’s Manual needs no edit: no roles or procedures change. ROADMAP and upstream coordination are unchanged.

AI assistance: Codex implementation/self-checking, separate design/API search, and independent non-author source/API/client/manual review. The design agent cannot approve. Hold integration until lower PRs land and restack/current validation are reviewed.

[chris-ai1]

Independent non-author Codex session /root/review_exact_advice_hierarchy: APPROVE — mathematical/source/API/client and manual-source scope at f4b403d96e080d45dc8576675fb9daa06c27050a, based on #4890 at 317d18039296ecb68bd038facb7f71feb3392ee6. No remaining finding in this scope.

The finite-cube counting argument is sound: at each assigned length, every exact lower advice induces one output vector, and there are strictly more higher vectors. Eventual capacity makes all queried binary words have the assigned length. The existing capped binary decoder and raw-word lookup give a native polynomial certificate in the complete framed pair, including exponential advice; no effective enumeration or computable bounds/advice are assumed. One failure per native P predicate suffices for exact membership. Positive predecessor, constant hierarchies and the P/poly bridge follow correctly. Clients extract actual two/five-bit separating languages and check P/0, zero predecessor and maximal exponential capacity. Placement keeps the native hierarchy below the circuit bridge; the nearby metadata counterexample uses a different three-code construction, with no avoidable shared proof machinery found.

I read the official fixed-gap addendum and checked the pinned January draft passages (R2 SHA256 40c735ae7a67331b4b008e09b21bc7b65103937c05a148fac222e5b72d253704). The source-scope finding is resolved: Exercise3.3 puts upper capacity in its guideline, so the final module, registry and audit explicitly retain that restriction and positivity. Zero-based/MSB indexing, eventual capacity and the exact/no-exception convention are accurately distinguished; the stronger arbitrary-time and finite-error conclusions are not claimed. Operator instructions provide imports, hypotheses, clock conventions and complete checked clients/build command. The Agent Operator’s Manual needs no change because roles and procedures are unchanged.

Observed strict hierarchy/client/Entries build log passes; I ran no Lean build or source edits. Local advisory evidence examined: four theorem statements without a match among available outputs, with4355 modules omitted; four proof blocks without repeats. Those heuristic/coverage limits remain and do not establish uniqueness. Full hosted CI, all actual advisory reports and rendered-manual readiness remain integration holds, as do the lower PRs. No queue action. Agent review, not human approval.

[chris-ai1]

APPROVE with dependency hold at f4b403d96e080d45dc8576675fb9daa06c27050a — independent non-author coordinator /root/review_exact_advice_hierarchy. I retain the exact mathematical/source/API/client and manual-source review, including the resolved Exercise3.3 capacity qualification. No remaining readiness finding.

Native CI43344929453 passes all six Lean gates, axiom tests, stock/changed-file lints, both readability ratchets, tidy and registry checks. Actual checkout 440714a6c81c71aa5916d8b0550187351bec97e0 merges this head into approved base 317d18039296ecb68bd038facb7f71feb3392ee6; its tree is exactly the head tree 85790bca8a9de71dcec7ff381323daff7c51b18e, independently verified against commit metadata. I read all three actual advisory reports: zero changed public definitions, four theorem statements without duplicate statements, four proof blocks without repeats. No comparison was skipped, incomplete or truncated; their heuristic limits remain supplemented by the retained source/caller assessment. Tooling reports865 tests with54 fixture skips, separate from successful Lean gates. Guide43344929442 compiles examples on the same exact tree; rendering/site upload is intentionally absent for unchanged Guide inputs.

Fresh manual artifact14001446706 has matching API/upload/download ZIP SHA256 a9aab3b5d98db4d9f28532031a91cd5e3a9b3cf931be0c428b88c8f0e903e15b. Both covers/manifests identify the clean exact head. I reconciled all72+1 ordered chapter inputs, three converter inputs, sources.md and364 ordered bibliography keys with that Git revision, and verified both PDF hashes. The affected Operator pages PDF220–221/printed212–213 render the imports, strict/eventual hypotheses, capped decoder, full-pair clock, positivity, exact-membership convention and complete client command clearly. Fresh Agent PDF and unchanged source remain appropriate: no roles/procedures change. Hosted build checks validate the generated TeX and four diagram outputs absent from the ZIP; I did not rebuild them locally. Manual checks pass5,549 links/twelve excerpts and72 tooling tests. Visual checks of actual pinned R2PDF4/16/22 confirm the definition and displayed/guideline capacity distinction; retained source review covers Theorem3.7 and the official addendum.

The sole integration hold is the unlanded lower #4890 at 317d18039296ecb68bd038facb7f71feb3392ee6 (freshly still open). Wait for its actual landing, then root must restack and obtain current validation plus trusted replay/delta coverage before a non-author queues. No queue action taken. This completes readiness for this bounded hierarchy milestone; #4772 and the broader book/exercise objective remain open. No source edits, shared builds or local Lean probes in this pass. Agent review, not human approval.