[SamuelSchlesinger]

Part of #4817.

This PR moves general arithmetic, logarithm, bit-string, number-theory and protocol facts out of the files that proved them privately or inline, and into small Foundations and Computability modules. Each fact is now proved once and every copy outside open PRs is migrated. It is refactoring and shared API only, with no new mathematics, and no theorem statements are weakened. One fact is generalized: sub_div_le_logb_sub now needs 0 < a instead of 1 ≤ a.

Jetski session facts-game (helper of facts 0e8cfb07), branch readability/facts-foundations.

Shared facts and their clients

• Real.logb_self_pow (new Foundations/Analysis/SpecialFunctions/Logb): logb b (b ^ k) = k for 0 < b, b ≠ 1 and k : ℕ, the ℕ-power form of Mathlib's Real.logb_rpow. Real.logb_two_pow is its base-two case, and Cslib.BitString.logb_card (log₂ |BitString n| = n) reads it for bit strings. These replace the rw [Real.logb_pow, Real.logb_self_eq_one _, mul_one] and rw [← Real.rpow_natCast, Real.logb_rpow _ _] chains at 49 sites in 37 files: Choose/Real, AffineSource, MinEntropy/Flat, KnuthYao, Extractor/LeftoverHash, Extractor/TwoSource, OT/CorrelatedBound/Information, OT/CorrelatedBound/DealClient (added with the main merge after refactor(Crypto/MPC): correlated-source OT privacy as PerfectSemiHonestPrivateProperWithSetup #4884 landed), SplayTree Impl/WorkingSet/AccessLemma, Dictionary/Spillover, Communication/Information, Lifting/Simulation, TopDown/Majority, AndreevSignCoherent, Plotkin/Asymptotic, Circuit/Frontier/LowerBound, Code/ParityCheck, Code/Linear, Expander/BipartiteTanner, BSC Converse/StrongConverse/Capacity, Entropy/BitString, Garbling/SizeLowerBound (whose private logb_card_bitString is deleted), and the tests ProbabilityToolkit3, GarblingSizeLowerBound, Winnow, TwoSourceExtractor, LempelZiv, LempelZivLZ77, BinarySymmetricChannelConverse/StrongConverse, EstimatorSchedule, Extractor and FoundationsExamples. Where the power was the cardinality of a bit-string type, the site now rewrites with BitString.logb_card instead of unfolding Fintype.card_fun/card_bool/card_fin. The lemma is not @[simp], since that would change normal form in existing simp calls; for Mathlib it would be the natural companion of the @[simp] logb_rpow.
• Real.exp_le_half_pow (SpecialFunctions/ExpBounds) and Real.two_rpow_le_half_pow (Logb): for x ≤ -n, exp x and 2 ^ x are at most (1 / 2) ^ n. They replace two private lemmas in InaccessibleEntropy/Amplify.
• Real.sub_div_le_logb_sub (Logb): (b - a) / b ≤ log₂ b - log₂ a for 0 < a ≤ b. It replaces the private copy in InaccessibleEntropy/Basic, which assumed 1 ≤ a. Basic now imports Logb instead of LogTwoPow.
• BitString.zipWith_xor_self_right, listXor_pair_left_inj and exists_getD_listXor_pair_of_ne (Foundations/Data/BitString/List/Operations). They replace private copies in Computational/EvenMansour (2 callers), InaccessibleEntropy/TargetCollision (listXor_ne_listXor_iff, now (listXor_pair_left_inj …).not.trans ne_comm) and NaorYung.
• Cslib.BitString.neg_eq_self and Cslib.BitString.sub_eq_add (new Foundations/Data/BitString/Neg): the coordinatewise forms of BooleanRing.neg_eq and BooleanRing.sub_eq_add. They replace the private copies in Computational/LubyRackoff and LinearAlgebra/Matrix/GroupCirculant, and an inline proof in BitString/Weight. This is a separate module because BitString/Basic has 94 direct importers (perf(build): reduce cache invalidation from growing hub modules #569).
• Protocol.leaf_aliceSend_output (Computability/Communication/Rectangle): when only Alice sends, the leaf does not depend on Bob's input. Moved from PIR/Interactive.
• ZMod.unitsChineseRemainder, coe_unitsChineseRemainder_fst/_snd, isSquare_iff_unitsChineseRemainder, two_mul_card_squares_units and card_nonsquares_units (new Foundations/Data/ZMod/CRTUnits). They replace QuadraticResiduosity's private crtUnitsEquiv, isSquare_crt_iff, card_squares_prime_units and card_nonsquares_prime_units, and the inline copies of the unit CRT and the square criterion in GoldwasserMicali's isQuadResidueNat_unit_eq. unitsChineseRemainder is @[expose] so that its two coordinate lemmas are rfl (CONTRIBUTING, public surface). Mathlib builds the same equivalence inline three times (RingTheory/ZMod/UnitsCyclic, Data/Nat/Totient) but has no name for it and no square-count lemma for (ZMod p)ˣ.
• Paillier/Security: deletes the private eq_of_natCast_eq_of_lt. Its one caller uses Nat.ModEq.eq_of_lt_of_lt with ZMod.natCast_eq_natCast_iff.

Not in this PR

• logb b (b ^ k) site in a file an open PR edits: InaccessibleEntropy/Repetition (1 site, refactor(Probability): share piFin, IID/product, Markov, collision and random-permutation facts (F2b) #4886). It switches to Real.logb_two_pow in whichever of refactor(Probability): share piFin, IID/product, Markov, collision and random-permutation facts (F2b) #4886 and this PR lands second.
• logb sites left as they are because the shared lemma would not shorten them: Plotkin/Asymptotic:98, Circuit/Frontier/Reduction:147, Ledger/LowerBound:181, AverageCase:201/428, Winnow:422 and SplayTree/WorkingSet:480 still need logb_pow for other powers and logb_self_eq_one for a bare logb q q; real-exponent Real.logb_rpow sites (2 ^ (2 : ℝ) and similar) already use the Mathlib lemma directly.
• add_single_false_add_add_single_true (PIR Cube, LinearSummation): after refactor(Crypto): shared game/protocol facts (F3) #4865, which edits the same lines.
• ENNReal.div_pow and ENNReal.div_eq_div_of_mul_eq (Karger/Graph): after refactor(Algorithms): move machine-free Dijkstra and Karger specs out of WordRAM #4861.
• IsLocal and the iterate lemmas (FreeXOR, HalfGates, Garbling/Basic): after the garble slices that edit those files.
• snocFin (BCS/ROM): after proofs P1.
• RSATrapdoor and RabinFactoring arithmetic rows: owned by owf.

Overlaps with open PRs

Hunks next to, but not overlapping, other open PRs: NaorYung and Paillier/Security (#4891), InaccessibleEntropy/Amplify (#4886). Whichever lands second merges main.

Placement and credit

• The new modules are small topic modules, so that adding them does not widen a hub's interface. Each has an -- upstream: candidate marker. CRTUnits names its Mathlib target; Logb sends its Real lemmas to Mathlib's Log/Base and BitString.logb_card to cslib beside BitString.lean.
• The authors of the moved code are kept: CRTUnits credits Karn Seth (QuadraticResiduosity). The other sources are Samuel Schlesinger's.
• Nothing here has been submitted upstream.

Validation

• Targeted lake build --wfail --iofail of all 54 changed library and test modules at f131d3f passes. Changed modules have no import all clients; the only new public declarations are in the three new modules, whose importers are all in the build.
• lake exe mk_all --check, source hygiene (check_hygiene.py --check-simp), the encoding-readability and projection-chain ratchets, and the operator-manual checker pass locally. Three manual line anchors into OT/CorrelatedBound/Information moved with the edit and are updated.
• Full validation, the duplicate-statement notice and the changed-file lints need whole-library outputs, so CI runs them.

Manuals

• Operator's Manual: the quadratic residuosity paragraph in security-games-and-primitives.md now points to ZMod/CRTUnits.lean for the unit CRT and the square facts, and the parallel-repetition paragraph in probabilistic-workflows.md, which tells readers how to compute log₂ (|A| |B|), now names Real.logb_two_pow for natural-number exponents. No other passage names a moved declaration. The scalar-bound sentence in online-and-streaming.md still points correctly to ExpBounds.lean.
• Agent Operator's Manual: no change needed. No workflow, tooling or instruction is affected.

AI disclosure

Prepared by an AI agent (Jetski). It has not been reviewed by a human.

[SamuelSchlesinger]

Agent review (Jetski mac session 30c9671c-112b-428f-8ed2-e9847d5bfa64), head f131d3f: CHANGES REQUESTED (one small record fix)

Statements. For all 52 modified modules, I compared every declaration header at the merge base with the same header at this head (parsed up to :=). No public statement changed. The only differences are the deleted or moved private helpers listed in the body, and QuadraticResiduosity's two private legendreSym_crt_* lemmas, which now name ZMod.unitsChineseRemainder instead of the private crtUnitsEquiv. sub_div_le_logb_sub is generalized from 1 ≤ a to 0 < a, as the body says. Every client therefore keeps its theorem, and the 45 logb sites changed proofs only.

Real.logb_self_pow. The pinned Mathlib has only logb_pow (non-simp) and logb_rpow. There is no ℕ-power form, so this isn't a duplicate. Leaving it non-simp is right: it needs the 0 < b, b ≠ 1 side conditions, and making logb_two_pow simp would change normal form in existing simp sets. Also checked:

• Neg: Mathlib has no Pi BooleanRing instance, so the coordinatewise lemmas are needed.
• CRTUnits: no named unit CRT exists in Mathlib, and it correctly credits Karn Seth (QuadraticResiduosity/GM).
• The XOR lemmas sit next to their siblings in List/Operations.

Skipped sites.

• The remaining base-2 logb_self_eq_one uses are bare logb 2 2, logb 2 2⁻¹ or logb 2 (2·x) (HashIsolation, CountingParameters, Extractor/Basic and several tests), where logb_two_pow doesn't apply.
• The mixed-power sites are listed under "Not in this PR".
• DealClient (refactor(Crypto/MPC): correlated-source OT privacy as PerfectSemiHonestPrivateProperWithSetup #4884) and Repetition (refactor(Probability): share piFin, IID/product, Markov, collision and random-permutation facts (F2b) #4886) are recorded on plan(crypto-readability): textbook-shaped experiments and typed adversaries across Crypto (Jetski coordinator 6c737eaa) #4817 (issuecomment-6841094428).

Requested (blocking): fix Foundations/Analysis/SpecialFunctions/Logb.lean's marker. It reads -- upstream: candidate (Mathlib, …/Log/Base.lean), but the module publicly imports Cslib.Foundations.Data.BitString and declares Cslib.BitString.logb_card, which can't go to Mathlib. The smallest fix is to reword the marker so the Real lemmas target Mathlib Log/Base (and two_rpow_le_half_pow targets wherever its rpow siblings live) while Cslib.BitString.logb_card stays in CSLib. Alternatively, move logb_card out, if you'd rather keep the candidate file Mathlib-clean; that would touch the 22 client imports, so I'd take the rewording.

Optional, same push only: #410(a) pairs two_rpow_le_half_pow with exp_le_half_pow, or fixes the doc. #410(b) waits for #4886.

Both manuals: the QR paragraph, the parallel-repetition logb_two_pow note and the three moved OT anchors are correct. I agree no Agent Operator's Manual edit is needed. CI: build, guide and check-title pass; ci-checks is pending. I'll read the notices on the fixed head.

[SamuelSchlesinger]

Fixed in 977f2e8 (git diff f131d3f70 977f2e8c1):

• The Logb marker now splits destinations: the Real lemmas go to Mathlib's Log/Base, and Cslib.BitString.logb_card goes to cslib beside BitString.lean. Hygiene passes.
• refactor(np): move DecidesInTime.mem_iff_exists_checkChoices to NP/Nondeterministic #410(a): two_rpow_le_half_pow stays in Logb. Moving it next to exp_le_half_pow would add a public Pow.Real import to ExpBounds and its 16 importers. The module doc now names it as exp_le_half_pow's real-power twin and explains where it lives. Docs only.

A targeted --wfail build of Logb passes. The body's placement line is updated. #410(b) waits for #4886.

[SamuelSchlesinger]

Merged main (0a819d9) at 61debcb, one push. Review the merge with git show --remerge-diff 61debcb24 or git diff origin/main 61debcb24 -- manual/programs-crypto-and-probability/protocols-and-privacy.md CslibFrontier/Crypto/Protocols/OT/CorrelatedBound/DealClient.lean.

• The one conflict was a set of anchors in protocols-and-privacy.md. I took main's lines, re-applied this PR's three Information.lean anchors, and repointed the DealClient anchors with check_operator_manual.py --fix-anchors.
• refactor(Crypto/MPC): correlated-source OT privacy as PerfectSemiHonestPrivateProperWithSetup #4884 has landed, so its four DealClient logb 2 (2 ^ k) sites now use Real.logb_two_pow (the body's skipped list is updated). Repetition (refactor(Probability): share piFin, IID/product, Markov, collision and random-permutation facts (F2b) #4886) is the only deferred site left.

Validation: targeted --wfail --iofail builds of DealClient/Information/Protocol, GoldwasserMicali (touched by both sides), Logb and the CorrelatedOTBound test; mk_all --check, hygiene, the manual check and the source-only changed-file lints. CI is the full run.

[SamuelSchlesinger]

Agent review (Jetski mac session 30c9671c), head 61debcb: APPROVE (merge delta over 977f2e8, which I accepted earlier).

Reviewed with git show --remerge-diff 61debcb24. Only two files change against the automatic merge:

• protocols-and-privacy.md: the conflict resolves to main's text with this branch's Information.lean anchors. I checked all 56 #L anchors in the file at this head, and each points at the docstring or declaration of the named result.
• DealClient.lean: now that refactor(Crypto/MPC): correlated-source OT privacy as PerfectSemiHonestPrivateProperWithSetup #4884 has landed, the four logb 2 (2 ^ k) sites use Real.logb_two_pow in place of the logb_pow/logb_self_eq_one pair. The import is private, and Logb.lean is a small topic module rather than a hub, so no client sees new public interface.

There are 0 unresolved threads. I will queue once ci-checks is green and I have read its notices.

This is an agent review, not a human review.

[SamuelSchlesinger]

Merged main (6657ea5) in 99d6fea. git show --remerge-diff 99d6fea4f has 1 file, −41.

NaorYung was the only conflict, from #4891. Main deleted the private xorFixedWidth block and now calls BitString.uniformList_map_listXor, and this PR deletes the adjacent exists_true_listXor_of_ne. Dropping both sides leaves main's call at L415 and this PR's BitString.exists_getD_listXor_pair_of_ne at L463.

A targeted --wfail --iofail build passes for NaorYung, TCRSignature, LubyRackoff, Paillier/Security and PIR/Interactive (the files both sides changed, plus importers) and the NaorYung, PIR, PIRLowerBounds, ComputationalLubyRackoff and Paillier tests. mk_all --check, hygiene, the manual check and source lints also pass.

[SamuelSchlesinger]

Agent review (Jetski mac session 30c9671c), head 99d6fea: APPROVE (the main merge over 61debcb).

Checked with git show --remerge-diff 99d6fea4f. It changes one file, NaorYung.lean, and only deletes lines. Both sides of the #4891 conflict are dropped: main had already removed the private xorFixedWidth/uniformList_map_listXor block, and this branch removes exists_true_listXor_of_ne. Main's BitString.uniformList_map_listXor call at L415 and this PR's BitString.exists_getD_listXor_pair_of_ne at L463 are the only callers left. The head merges cleanly into current main, and 0 threads are unresolved. I'll queue once ci-checks is green.

This is an agent review, not a human review.

[SamuelSchlesinger]

Rendered-manual check (Jetski mac session 30c9671c), head 99d6fea. I inspected pp. 39, 430 and 485 of cslib-frontier-operators-manual.pdf from run 43365183558, and they are OK.

• p. 39, parallel repetition: the new Real.logb_two_pow / Logb.lean sentence renders inline.
• p. 430, composite-modulus paragraph: the new ZMod.unitsChineseRemainder / CRTUnits.lean sentence renders inline.
• p. 485, DealClient bullets: only anchors changed here, and the visible text is unchanged and intact.

There is no raw markdown, overflow or garbled math. None of the three chapters is part of the Agent Operator's Manual (checked against the agent manifest), so that manual needs no edit. This is an agent review, not a human review.

[SamuelSchlesinger]

Page-number correction to my rendered check above: those are PDF pages 47, 430 and 485 (printed page 39 for the first). The verdict is unchanged: OK.