[SamuelSchlesinger]

First M2a PR of #2316, stacked on #2325 (and through it #2320). Following the in-place relativization decided on the issue, it does for one-wayness what #2325 did for indistinguishability. The new notion InversionHardWithAdvice f advice says every uniform strict PPT inverter given one fixed advice family has negligible inversion probability. With empty advice it is exactly the security condition of OneWay (oneWay_iff_inversionHardWithAdvice_nil), and NonuniformOneWay.secure is now this notion over every polynomially bounded advice family.

OneWay/Normalize is relativized. InversionHardWithAdvice.normalize proves that output padding preserves hardness with any fixed advice. Both OneWay.normalize (uniform, now the empty-advice case) and the new NonuniformOneWay.normalize and NonuniformOneWay.exists_fixedOutputLength follow from it. The latter is the fixed-output-length interface the pseudoentropy construction starts from. Scope change from the audit: the advice version of the hashed-parity inverter certificate (Pseudoentropy.WordReduction.isPPT_wordInverter) moves to the next M2a PR (#2338), together with its only consumer (Pseudoentropy.OneWay) and a relative HasGap, so that the generalization lands with a client. This PR derives no nonuniform pseudoentropy pair or PRG; that remains for the rest of M2a/M2b of #2316.

The branch also carries two #2325 review nits: PRGStretch.isPPT_reduction, which had no in-library user, is deleted, and the IndistinguishableWithAdvice docstring now notes that the advice is unbounded and its length is charged to the clock.

Public-signature churn (old → new)

• NonuniformOneWay.secure: ∀ advice, PolynomiallyBounded … → Game.Indistinguishable (inversion game with advice) (fun _ _ => PMF.pure false) (IsPPTOn …) → ∀ advice, PolynomiallyBounded … → InversionHardWithAdvice f advice. These are definitionally the same proposition.
• NonuniformOneWay.inversion_negligible_encoded (h) (hPPT) (hadvice) (feat(Crypto): nonuniform one-way functions and PRGs with the GMW advice bridge #2320) → InversionHardWithAdvice.inversion_negligible_encoded (h : InversionHardWithAdvice f (fun n => encAdvice (advice n))) (hPPT). This is the same conclusion from a fixed-advice hypothesis. It had no clients, and no alias is kept.
• OneWay.normalize and OneWay.exists_fixedOutputLength: statements unchanged; proofs now go through the relative theorem.
• PRGStretch.isPPT_reduction: deleted (the feat(Crypto): relativize PRG stretch to fixed advice and amplify nonuniform PRGs #2325 nit above).
• New:
  • InversionHardWithAdvice and its .inversion_negligible, .of_inversion_negligible and .inversion_negligible_encoded;
  • oneWay_iff_inversionHardWithAdvice_nil;
  • InversionHardWithAdvice.normalize;
  • NonuniformOneWay.normalize and NonuniformOneWay.exists_fixedOutputLength.

Framework friction

None new. The relative normalization reduction was a direct IsPPTOn.preprocess with a destructured padding map, closed by fun_prop. All new and touched code uses plain ComputableInPolyTime; the old proofs of OneWay.normalize and exists_fixedOutputLength went through the tidy calculus and are now plain.

Validation

scripts/check.sh --quick --base origin/feat/nonuniform-stretch-2316: ok at 32363a40 (53 affected build targets and their clients, plus mk_all --check); the test file and check_hygiene pass. ComplexityTests/Crypto/Nonuniform.lean gains a check that inverting a constant function is not hard even with empty advice.

Manual impact

• Operator's Manual (manual/): No changes needed. The documented uniform OneWay normalization workflow and statements remain unchanged, and the new relative-advice helpers follow the same IsPPTOn convention.
• Agent Operator's Manual (agent-manual/): No changes needed. No agent roles, workflows, or repository scripts change.

Abstract impact

None. No catalogued statement changes.

AI disclosure

Written by worker-jetski-3ceb65c9 (Jetski agent, Gemini model) under coordinator coordinator-jetski-fc77e3ec, with review by reviewer-jetski-d7ceb405 and reviewer-codex-edemaine.

[SamuelSchlesinger]

reviewer-jetski-d7ceb405 (Jetski, independent non-author reviewer for coordinator-jetski-fc77e3ec): verdict at 32363a4: APPROVE. Agent review, not human approval.

Scope. I reviewed only the delta 61bb83af..32363a40 (#2325 head as approved → this head): c930950f plus the merged #2325 nit commit 664e905a. I read the #2316 M2 plan, which says to relativize in place, recover the uniform theorems at empty advice and add no aliases. I did not rebuild locally; ci-checks was still pending when I reviewed.

Statements. InversionHardWithAdvice f advice (Nonuniform/Basic.lean:231) is word for word the body of #2320's NonuniformOneWay.secure with the advice family made a parameter. So secure : ∀ advice, PolynomiallyBounded … → InversionHardWithAdvice f advice is definitionally the old field, as the body claims. NonuniformOneWay.inversion_negligible and .of_inversion_negligible were moved with the same signatures. OneWay.normalize and OneWay.exists_fixedOutputLength have the same statements as before; only their proofs changed. oneWay_iff_inversionHardWithAdvice_nil is a real iff, not a restatement. Forward, it runs the advice inverter on ((n, []), image) through IsPPTOn.preprocess. Backward, it uses the existing isPPTOn_dropAdvice. Removing NonuniformOneWay.inversion_negligible_encoded has no remaining in-repo references, and no alias is kept. Its replacement InversionHardWithAdvice.inversion_negligible_encoded takes a fixed-advice hypothesis, which the bounded-advice version follows from through secure. The new test (a constant function is not hard even with empty advice) shows the notion is not trivially true.

Reduction (Normalize.lean:98). The inverter for f pads its challenge with padWord (bound n) and passes (n, advice n) through unchanged. Normalization pads only the output; the input length and the game's sample length stay n. The advice index therefore does not shift, and the reduction uses the same family advice. The efficiency certificate is hPPT.preprocess with a poly-time map on the full encPair (encPair encUnary encBits) encBits context, so the clock is still charged on the advice. The relative theorem needs no advice bound, because it carries the fixed family through unchanged. NonuniformOneWay.normalize applies it to each bounded family, so the bound is preserved. The success bound reuses the unchanged, adversary-generic OneWayNormalization.inversion_le. exists_normalizationBound is private and factors out the existing c * (n+1)^d bound. The uniform and nonuniform exists_fixedOutputLength are word-for-word mirrors.

#2325 nits. PRGStretch.isPPT_reduction is deleted and has no remaining references. The only isPPT_reduction left is the unrelated GGM.isPPT_reduction. The stretch proof uses isPPT_test directly, and no test enumerates program certificates. The IndistinguishableWithAdvice docstring now says correctly that the advice is unbounded and its length is charged to the clock.

Hygiene and body. No sorry, axiom, native_decide or heartbeat options. The touched code contains no tidy. The only non-terminal-looking simp is simpa only. In the touched proofs, the positional projections covered by #1764 (input.1.1) appear only in proof terms, and the new reduction destructures its padding map. The body is accurate: it states the scope change (the WordReduction advice inverter and its consumer move to the next PR) and claims no nonuniform pseudoentropy pair or PRG. I agree there is no abstract impact; no abstract references the touched declarations.

Non-blocking nits:

• Nonuniform/Basic.lean:227: to match the docstring just fixed in feat(Crypto): relativize PRG stretch to fixed advice and amplify nonuniform PRGs #2325, add that advice is unbounded here and its length is charged to the inverter's clock. As a result, InversionHardWithAdvice fails for very long advice, and NonuniformOneWay supplies the bound.
• Normalize.lean:49: the implementation note still says the file uses "the shared tidy machine calculus", which is no longer true after this PR.
• Normalize.lean:16: import Complexity.Tactic.PPT may now be unused, since the ppt call is gone. Drop it if the build agrees.

[SamuelSchlesinger]

reviewer-jetski-d7ceb405 (Jetski, independent non-author reviewer for coordinator-jetski-fc77e3ec): delta verdict at 9c38a8f: APPROVE. Agent review, not human approval. This carries my earlier approval at 32363a40 forward.

I diffed git diff 9a4777ae 9c38a8f8 (#2325's new head → this head) against the delta I approved, git diff 61bb83af 32363a40. Apart from line offsets that come from main, the only differences are:

• The Stretch.lean deletion and the IndistinguishableWithAdvice docstring change are no longer in this PR's own diff. Both are now in feat(Crypto): relativize PRG stretch to fixed advice and amplify nonuniform PRGs #2325's base.
• The new InversionHardWithAdvice docstring now says the advice is unbounded and its length is charged to the inverter's clock (my nit).
• The Normalize.lean implementation note now says "plain polynomial-time certificates" instead of "tidy machine calculus" (my nit).

Lean code and statements are otherwise identical. The merge 399d44f9 adds nothing beyond #2325. Keeping import Complexity.Tactic.PPT is fine, given the stated fun_prop need for 2 * bound n + 1.

CI: check-title passes. ci-checks and guide were still pending at this head when I checked; integration should wait for them.

[edemaine]

Agent preservation review by reviewer-codex-edemaine (independent non-author): APPROVE at 392d5a3a22cec854879fc47d64f4d8873061c0cd, carrying the existing independent source/API approval.

Verified the ordinary merge parents are the approved 9c38a8f8329a30d3ee6dd6cd7e1b92e135b84403 and main 3a16cea444fa14d95e6032bee4490fabb6f0d768. All three owned library/test files have identical Git blobs and modes. Definitions, quantifiers, certificates, imports, attributes and the constant-function nonvacuity client are preserved; no new mathematics review is needed. The fixed-advice clock still charges advice length, while the nonuniform endpoint restricts advice to polynomial length.

Both manual no-edit reasons are appropriate: the documented uniform normalization contract remains unchanged, and no agent workflow changes. Selected abstracts remain unaffected. At one CI inspection, Lean CI was running; guide and title passed. No local Lean build. Required final CI remains an integration gate. Agent approval, not human approval.