{"id":2591,"job_id":null,"problem_id":1,"lane_id":null,"type":"paper","user_id":1,"model":"gpt-6.1-sol","provider":"openai","report_md":"The supplied source supports a defensible proposal for the three mapped claims. My judgment is based on reading the complete selected text and deriving its mathematical chain; it is not a compiler, kernel, authenticated execution, publication, or trusted-review verdict. Two mapped claims are eventual assertions over real y, proved through finite estimates; they are not merely checks of particular numerical instances. No tools, history retrieval, builds, external-source readings, or publication calls were performed.\n\nThe exact claims and domains are:\n\n1. `PrimaryMain.manuscript_main_goal`: there exist real c>0 and Y such that every real y≥Y satisfies c·mainShape(y)≤G2(mainPrimes(y)). The shape is y(log y)^3(log log log y)^2/(log log y)^4. The family is every natural prime whose real cast is ≤y, rather than the auxiliary family up to sqrt(y). The proof chooses c=1/chooseB(12).\n2. `IntegerMainBinding.integer_maximum_binding`: for `(S : Finset Nat)` and `(hS : PrimeFamily S)`, G2(S) is attained by an integer consecutive gap and bounds every such gap at every integer start. `PrimeFamily S` means ∀p∈S, Nat.Prime p. It is an explicit mathematical hypothesis, even though it supplies no analytic estimate. `assumptions: []` must mean no additional analytic inputs or custom axioms, not absence of this hypothesis.\n3. `IntegerMainBinding.manuscript_integer_main_goal`: the first assertion combined with the second, giving an attained maximum distance d and its lower bound for the full cutoff family. It uses the same c and eventual threshold, takes d=G2(mainPrimes(y)), and proves the required PrimeFamily condition.\n\nThese types match the revised manuscript's theorem and maximum characterization. Their full individual claim coverage does not imply full manuscript coverage.\n\nThe maximum definition is independent of covering. `Survivor S n` is gcd(n(n+2),period S)=1; its integer version uses Int.gcd. `Consecutive` and `IntConsecutive` require positive natural distance, surviving endpoints, and failure at precisely the offsets 0<i<d. `cyclicGapDistances` restricts the start to 0≤s<P and distance to 1≤d≤P, while allowing s+d≥P. G2 is its finite supremum. Primality gives P>0; the residue P−1 survives because its two factors are congruent to −1 and 1. Periodicity gives a survivor in every window of P positive offsets, bounding every consecutive distance by P. A least next survivor supplies nonemptiness and therefore attainment. Integer remainder normalization preserves the polynomial and every offset, including negative starts. This proves both directions of the integer maximum binding. For S empty, P=1, every integer survives, and the maximum is 1. The supremum's empty-set fallback is consequently not used on the theorem domain.\n\nThe covering bridge is also sound. The two classes are encoded as i≡a(p) or i+2≡a(p), avoiding truncated natural subtraction. Distinct primes admit a CRT phase s+a(p)≡0. At that phase, covering is exactly failure of survivor membership. An excluded block may start away from a surviving endpoint: the proof translates by P, chooses the greatest preceding survivor, and uses its least next survivor to obtain distance at least m+1. Conversely, an attained distance at least m+1 supplies m excluded interior positions. This includes m=0. Reserved completion only requires a finite injection and disjointness to preserve early choices; primality is required when converting the completed cover into the gap bound.\n\nThe incidence sieve uses the actual positive interval 1,…,X. Its weights are fiber cardinalities of the incidence product D(n), so nonnegativity, finite support, total mass X, divisor moments, and the sifted-count identity are derived. Under PrimeFamily, the period is squarefree and every divisor is the product of its selected prime subset. Canonical CRT residues give cardinality g(d)=∏p|d |Ωp|. Each residue-class count differs from X/d by at most 1, including d>X; summation gives |r_d|≤g(d). Canonical representatives and primality are real hypotheses in this derivation, discharged for the manuscript sets. Divisors of the positive period cannot be zero. The global definition sets g(0)=0 and g(1)=1; ν(d)=g(d)/d is coprime-multiplicative, with Lean's zero-preserving division convention. On supported divisors it is the required positive squarefree density.\n\nThe residue correspondence preserves the real cutoffs and the strict/closed band z0<p≤z1. Natural representatives are proved equal to the literal modular classes. With 3<z0, the cardinalities are 1 at 2, 2 at 3, and otherwise 4 in the middle band or 2 outside it. The four middle residues have nonzero pairwise differences of absolute values 1,2,3, so primes above 3 give no collisions. Thus 0<ν(p)<1 and ν(p)≤4/5, including the two small primes. These facts justify divisions, logarithms, positive Euler products, and the BoundingSieve instance; they are not assumed analytic inputs.\n\nThe Selberg reasoning is internally consistent. The denominator uses d²≤H, not d≤H. Finite squarefree Möbius inversion proves the constructed coefficients have λ1=1 and quadratic main term 1/J(H). Their support implies the expanded lcm error is supported at n≤H. The coefficient bound |λd|≤d and the 3^ω(n) ordered squarefree lcm pairs give n²3^ω(n); multiplying by g(n)≤4^ω(n) and using 12^ω(n)≤4n² gives error at most 4H^5. The exceptional correction factors at 2 and 3 multiply to 4.\n\nThe finite Euler first-moment argument retains half the mass below logarithmic cost log H/2 when ∑ν(p)log p≤log H/4. The supplied prime-log proof derives ∑p≤N log p/p≤log4(2+log N) from the primorial bound and finite summation. The restricted/full product ratio is bounded using −log(1−ν)≤5ν. With k=512log4, N=floor(exp(L/k)), H=exp(L/16), and L=log y, the source proves the scale, ratio, and error inequalities at a sufficient positive threshold. Its constants agree with the prose: E=20log4·k+80log4, Cs=2exp(E), C=4exp(10log4), K=Cs·128C², and B=1+6K·12^4. Ordinary finite Euler bounds and exact floor/log comparisons give the one-sided product bound. Substitution then yields the sieve budget y/(4L). No two-sided Mertens asymptotic is needed.\n\nEarly noncoverage has the required finite classification. If auxiliary avoidance fails, a prime p≤sqrt(y) divides k=i or i+2; extra middle hits would already cover i. Every prime factor of k is above z0. Any factor q>z1 must satisfy q≥y/2. Such p and q are distinct, and pq divides positive k≤m+2, whereas p>z0 and q≥y/2 contradict 2(m+2)/y≤z0. The Lean argument therefore proves a stronger smooth-or-auxiliary classification than the prose needs; retaining the short branch only enlarges the counting upper bound. Union cardinalities and the injection i↦i+2 give R≤S+floor(sqrt(y)+2)+2Ψ(m+2,z1).\n\nThe smooth budget avoids a hidden uniform-asymptotic assumption. Ψ counts positive integers, includes 1, excludes 0, and imposes prime divisors ≤real Z. The library adapter uses floor(Z)+1 to preserve its strict-bound convention. Rankin summability is over integers factored over a finite prime set, valid for every α>0; it does not require the all-natural series to converge at α≤1. For U=log X/log Z, U≥1, log Z≥1 and U≤sqrt Z imply δ=log U/(2log Z)∈[0,1/4]. The shifted product bound gives exponent −Ulog U/2+6log4·sqrt U·log U. The exact floor/+2 parameter lemmas discharge the range and prove ulog u/L2→12. Eventually sqrt u≥288log4 and ulog u≥(23/2)L2; hence the exponent is ≤−(529/96)L2≤−(11/2)L2. With Xlog Z≤2yL^4 and sqrt L≥96C this gives 2Ψ≤y/(24L). The short term is also ≤y/(24L), so the three budgets sum exactly to y/(3L).\n\nThe reserve supply has a separate elementary proof. The signed factorial wheel has period 30, values 0 or 1, and value 1 at arguments 1,…,5. Factorial-log bounds give |T(x)−ax|≤5(1+log(x+1)), including x<1. The von Mangoldt divisor identity gives the exact weighted wheel sum. Its strip comparison and strong induction yield aN−5LN≤ψ(N)≤(6/5)aN+5LN². Higher prime powers contribute at most 2sqrt N(log N)², using a covering image of base/exponent pairs without assuming injectivity. Rational logarithm bounds give a≥31/36, hence 2a/5≥31/90. At y≥max(300000^4,e), the explicit error is ≤y/90, so θ(y)−θ(y/2)≥y/3. The strict dyadic prime strip is contained in the inclusive reserved family, and each log p≤log y. Therefore its cardinality is ≥y/(3log y). This is a sufficient lower bound, not the coefficient-1/2 PNT asymptotic.\n\nCompletion now follows from the natural cardinality comparison, with all early residues preserved. The floor mass equals c·mainShape(y), and the strict floor inequality makes it <m+1≤G2. All intermediate positivity, geometry, smooth-range and supply conditions are discharged by finite maxima of eventual thresholds. The resulting theorem has no remaining Input S, M, H or P premise. It asserts neither an optimized onset nor infinitely many twin primes.\n\nAgainst the actual supplied prior-accepted manuscript, SHA256 cc0432e2b45ac88f478860fe2da61262047d55764837e80f8cae65d9b525ca5e, the visible revision adds the historical contribution paragraph, the explicit PrimeFamily/assumptions explanation in Section 1, and the expanded adapted-source/ledger attribution in Section 10. The mathematical exposition and O1–O7 blocks otherwise agree in the supplied texts. The current manuscript is declared as SHA256 6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80. I did not compute hashes or execute a byte diff. The earlier 4ed5 manuscript mentioned in the map is a different historical review target and must not replace this comparison baseline.\n\nThe attribution corrections are defensible as preservation of supplied provenance: historical Astra and DeepSeek credits remain historical, the present source-author attribution remains the issued gpt-6.1-sol/high designation, PNT+ and Arend Mellendijk notices remain, OpenAI math adaptations retain their revision credit, and PrimeLog retains the Mathlib theta contributors. No linked history, author date, original literature page, or license archive was independently retrieved. Job #3880 remains open for the named source expert; these additions do not reconstruct chronology or close that prerequisite. This is source-author self-review, not independent trusted acceptance.\n\nThe allowed standard axioms are propext, Classical.choice and Quot.sound. No custom analytic axiom is introduced in the displayed scientific source. `Target_*` definitions are propositions, not evidence of proof; the corresponding theorem bodies supply the arguments. Likewise, `#print axioms` commands are not observed audit output. Challenge `sorry` placeholders belong only to the trusted statement specification and must be rejected as solution evidence. Transitive axiom legality, exact critical-definition values, built-in primitives and proof typing still require actual checks.\n\nThe execution contract correctly separates inert reconstruction from proof validation. The ordered stream's declared 123032181 bytes plus the 1039-byte primitive appendix equal the declared 123033220-byte solution. Hashes, AST records and historical PASS fields are supplied evidence descriptors, not newly reproduced observations. Referenced capsule contents, dependency bodies and setup/object inventories are not all displayed as source here. One audit uncertainty is visible: the portable declaration scanner looks for `ax`, while the primitive scanner permits `axiom` records. Their grammar must be reconciled with the actual exporter before claiming axiom-scan coverage; neither scan establishes transitive legality or kernel acceptance.\n\nCurrent fresh reference/export generation, primitive comparison against that fresh reference, binding and axiom audits, both kernel stages, all mandatory controls, and authenticated formal proof acceptance are NOT RUN. Required gates are independent review of the exact current manuscript/map and operator/tool sources; verified source/setup/toolchain/object custody; current reference and exports; actual primitive and definition comparisons; transitive axiom checking; Lean and Nanoda positives and seven rejection controls; independently attested execution boundaries; and the authenticated receipt for this exact package. Inert preparation/custody is reported as passed by the supplied metadata, not performed by me.\n\nA mathematical falsifier is a counterexample within the exact stated domain or a genuine gap in the derived inequalities. A compiler failure, extra axiom, mismatched definition/primitive, accepting negative control, or broken source-to-object custody falsifies the proposed validation evidence without automatically refuting the theorem. My source reading found no mathematical counterexample or fatal logical gap. O1–O7 remain OPEN: Mertens prime-harmonic asymptotics, uniform smooth asymptotics, the arbitrary-A>4 smooth route, dyadic PNT asymptotics, external/general sieve statements, two-sided product comparisons, and the separate priced short construction. This is not a fully formalized original paper.\n\nThis is a source and statement proposal; current execution is pending. Native usage is allocated only to the accompanying issued planning return, so tokens here are intentionally deferred rather than claimed twice.\n\nSeparately labelled Lean-kernel source package. The exact manuscript, mathematical sources, scientific identity and independently reviewed statement mapping #695 are unchanged. The new profile checks pinned source-built objects with the Lean kernel and an axiom audit in an isolated external worker. It does not claim independent export comparison or Nanoda checking. Old exported artifacts retained for scientific identity are supplementary and are not checked by this profile. Current execution and its authenticated receipt remain pending. Seven original obligations O1–O7 remain open; coverage is only the three mapped finite main/integer declarations. This is a source/metadata derivation from actual Sol returns #2585 and #2588; no new inference or historical execution is claimed. Usage was credited once on the original native planning completions; this package has tokens:null.","patch":null,"cpu_hours":0,"hashes":{},"author_rung":"heuristic","status":"pending","final_rung":null,"created_at":"2026-10-09T12:47:07.305Z","repo_url":null,"commit":null,"cites":{"returns":[2585,2588]},"tokens":{"log":"custom","input":0,"models":{"gpt-6.1-sol":0},"output":0,"source":"none","entries":0,"cache_read":0,"cache_write":0,"observed_models":["gpt-6.1-sol"]},"paper_slug":"kk-lower-bound","revision_path":"paper/kk-lower-bound.md","revision_sha":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80","recipe_md":"# Minimum Lean-kernel assurance: lean-kernel-v1\n\nThe scientific and literal statement identities are unchanged. Old export chunks,\nappendix and comparator provenance are supplementary UNUSED historical artifacts;\nthis profile does not consume or validate them as proof representations.\n\nUse the pinned existing Linux aarch64 Lean 4.35.0-rc3 release, binary and source\narchive descriptor. The kernel executable is materialized from the released\nruntime, not a locally rebuilt compiler. Decode capsule_codec.py's exact bounded\nsource-recipe and kernel-operator capsules; use every exact source/setup/argv,\nasset, prefix and retained-output pin. Existing retained objects may be supplied\nread-only iff all3169 modules/15693 outputs and every companion file hash match.\nChanged/missing/shadowed inputs FAIL; no historical receipt is a current result.\nThe archives named by the retained dependency descriptor supply the pinned\nexternal module sources. Authored source files are direct manifested artifacts.\n\nIn a readonly-root, nonroot UID10001/GID10001, network-none Docker container,\ncapabilities NONE, no-new-privileges, IPC none, 4GiB memory and memory+swap ceiling,\n2 CPUs,256 pids,64MiB noexec/nosuid /tmp, read-only declared inputs and one owned\ndisk scratch, run the packaged outer+inner adapter. Before/after effective mount,\nnetwork namespace/interface/socket guards and exact image/process observations\nmust PASS. No secret/socket/home mounts. Existing four-hour assignment deadline\nis shared; each active container is limited1200s, cleanup reserved600s; logs8MiB\nper stream and workspace8GiB sampled with early rejection at7.5GiB are MONITORS,\nnot filesystem quota claims. Cleanup and owned-container absence are required.\n\nInvocation: python3 -I run_pilot.py --execute --candidate <package-root>\n--plan <selected-plan> --expected-plan-sha256 <actual-raw-plan-sha256>\n--expected-fingerprint <actual-fingerprint> --assignment-deadline-monotonic\n<actual-issued-deadline> --output <fresh-owned-output>. Host locations/observations\nare private receipts only, not scientific/execution identity values.\n\nActual stages: hash every exact source/setup/asset/released-prefix/cache output;\nparse current source headers and setup; compile fresh TrustedMainChallenge types\n(its three placeholder proofs are NOT solution proofs); compare stored literal\nthree theorem types/levels and12 critical definition type/value ASTs; check464\nmapped axiom closures against exact expected sets. Compile KernelReplay.lean,\nwhich imports the pinned objects, gathers target proof/type dependencies plus\nmutual/inductive blocks, rejects unsafe/partial and all unapproved axioms,\nreplays the full gathered closure into a fresh EMPTY Lean kernel environment,\nchecks generated quotient constants and compares all three checked proof bodies\nand types to the actual imported declarations. Never seed an imported kernel env.\n\nControls: a valid True theorem has the wrong literal target statement; an actual\ntarget body replaced by True.intro must be rejected by fresh kernel replay;\nsynthetic sorryAx/customAxiom proof alternatives are rejected by transitive axiom\npolicy, even though a kernel would accept an axiom assumption. These are clearly\nlabelled synthetic control constructions; they are not an independent Nanoda run.\nNo export/compiler dependency closure rebuild or primitive external stage occurs.\nAll current observations, source/object hashes, commands, failure logs and cleanup\nare retained. Current authenticated ordinary Sol/high callback must assess the\nactual completed evidence; no prior build can be renamed a current check. Final\nordinary independent correctness review follows execution, with no source-review\nor execution-review precondition for this distinct profile.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"high","also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":null,"research_route_id":null,"verification_plan":{"cost":{"ram_gb":4,"disk_gb":8,"minutes":20,"cpu_hours":1,"judgment_minutes":20},"lean":{"claims":[{"id":"integer_main_eq1","target":"IntegerMainBinding.lean","locator":"Revised manuscript Sections 1 and 8: Eq.(1) with the attained integer-gap definition and full prime cutoff.","coverage":"full","assumptions":[],"declaration":"IntegerMainBinding.manuscript_integer_main_goal"},{"id":"integer_maximum","target":"IntegerMainBinding.lean","locator":"Revised manuscript Section 1: attained largest gap over all integer starts, including negative starts and the period boundary.","coverage":"full","assumptions":[],"declaration":"IntegerMainBinding.integer_maximum_binding"},{"id":"main_eq1","target":"PrimaryMain.lean","locator":"Revised manuscript Sections 1 and 8, Eq.(1): eventual full-prime-cutoff cyclic two-residue survivor-gap bound.","coverage":"full","assumptions":[],"declaration":"PrimaryMain.manuscript_main_goal"}],"policy":"lean-kernel-v1","toolchain":"leanprover/lean4:v4.35.0-rc3","paper_slug":"kk-lower-bound","dependencies":[{"name":"Cli","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","revision":"843844fa601dd56767b1eb22b7ada5b64d5e567a"},{"name":"Lean","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","revision":"470d5ce1400764999581fd26d5d72b00d990b0f4"},{"name":"LeanSearchClient","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","revision":"50cd21bc62f2c8357c4f269d1185921cbfcdfc90"},{"name":"Qq","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","revision":"d93a8a0622807953d1e424f0fe2a5f5b5520c12e"},{"name":"aesop","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","revision":"36cb0105a76ff3de70add8ae91afb6cfc57fafe3"},{"name":"batteries","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","revision":"ec2288a9bf12ecc05a459c5db5aac77f4c73424c"},{"name":"importGraph","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","revision":"7ad9f2e325aa6cec3dacaa97c2653a98032750eb"},{"name":"mathlib","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","revision":"331d5244f0d3aad530d9ab00ded135b4c7691502"},{"name":"plausible","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","revision":"afc2695efcb6855264d85a45632db1ddc56c8774"},{"name":"proofwidgets","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","revision":"87dfe779d5dfd03142ee4fe158911b8eb553ec98"}],"artifact_roles":[{"kind":"scientific","path":"ActualBoundingSieve.lean"},{"kind":"scientific","path":"Arithmetic.lean"},{"kind":"scientific","path":"Bridges.lean"},{"kind":"scientific","path":"CRTMoments.lean"},{"kind":"scientific","path":"DivisorMoments.lean"},{"kind":"scientific","path":"EarlyCover.lean"},{"kind":"scientific","path":"EulerRatio.lean"},{"kind":"scientific","path":"FactorialLogBounds.lean"},{"kind":"scientific","path":"FactorialWheel.lean"},{"kind":"scientific","path":"FiniteCoreTargets.lean"},{"kind":"scientific","path":"Gaps.lean"},{"kind":"scientific","path":"IncidenceMoments.lean"},{"kind":"scientific","path":"IntegerMainBinding.lean"},{"kind":"scientific","path":"ManuscriptParameters.lean"},{"kind":"scientific","path":"ManuscriptResidues.lean"},{"kind":"scientific","path":"MertensBand.lean"},{"kind":"scientific","path":"Normalization.lean"},{"kind":"scientific","path":"PrimaryMain.lean"},{"kind":"scientific","path":"PrimeFactorial.lean"},{"kind":"scientific","path":"PrimeLog.lean"},{"kind":"scientific","path":"PrimePowerTail.lean"},{"kind":"scientific","path":"PrimePsiBounds.lean"},{"kind":"scientific","path":"PrimeReserveBudget.lean"},{"kind":"scientific","path":"RealBand.lean"},{"kind":"scientific","path":"ReserveBudget.lean"},{"kind":"scientific","path":"Reserved.lean"},{"kind":"scientific","path":"ResidueMoment.lean"},{"kind":"scientific","path":"SelbergError.lean"},{"kind":"scientific","path":"SelbergEuler.lean"},{"kind":"scientific","path":"SelbergFinite.lean"},{"kind":"scientific","path":"ShiftedRankin.lean"},{"kind":"scientific","path":"SieveCoarse.lean"},{"kind":"scientific","path":"SieveInterface.lean"},{"kind":"scientific","path":"SieveParameters.lean"},{"kind":"scientific","path":"SmoothBudget.lean"},{"kind":"scientific","path":"SmoothLogLimit.lean"},{"kind":"scientific","path":"SmoothParameters.lean"},{"kind":"scientific","path":"SmoothRankin.lean"},{"kind":"execution","path":"capsule_codec.py"},{"kind":"execution","path":"checker/KernelReplay.lean"},{"kind":"execution","path":"checker/kernel-build-provenance.json"},{"kind":"execution","path":"checker/kernel-config.json"},{"kind":"execution","path":"checker/kernel-invocation.md"},{"kind":"provenance","path":"checker/kernel-object-inventory.json"},{"kind":"execution","path":"checker/kernel-operator-capsule.json"},{"kind":"execution","path":"checker/kernel-source-inventory.json"},{"kind":"execution","path":"checker/lean_kernel_validator.py"},{"kind":"scientific","path":"dependencies/mathlib/lake-manifest.json"},{"kind":"scientific","path":"dependencies/mathlib/lakefile.lean"},{"kind":"provenance","path":"dependencies/tool-and-source-descriptor.json"},{"kind":"provenance","path":"evidence-and-tool-source-capsule.json"},{"kind":"scientific","path":"lean-toolchain.txt"},{"kind":"scientific","path":"mandatory-primitives-appendix.txt"},{"kind":"scientific","path":"manuscript.md"},{"kind":"scientific","path":"ordered-export-index.json"},{"kind":"provenance","path":"original-manuscript-verbatim.md"},{"kind":"scientific","path":"proof-export-00.xz.b64.txt"},{"kind":"scientific","path":"proof-export-01.xz.b64.txt"},{"kind":"scientific","path":"proof-export-02.xz.b64.txt"},{"kind":"scientific","path":"proof-export-03.xz.b64.txt"},{"kind":"scientific","path":"proof-to-exposition-map.json"},{"kind":"provenance","path":"source-recipe-capsule.json"},{"kind":"scientific","path":"statement-bundle.json"}],"kernel_custody":{"objects":{"path":"checker/kernel-object-inventory.json","bytes":1046,"sha256":"4d521d484b1dd8aa15b62c98f2df05521518b900b9ed8b53a5a8f25d2108522c"},"sources":{"path":"checker/kernel-source-inventory.json","bytes":1155531,"sha256":"486961784524459dd1e344bf1ff50fd8c6c67ec103a0edf3d96f3df1ee15eb97"},"provenance":{"path":"checker/kernel-build-provenance.json","bytes":1433,"sha256":"63f6c8c7421f08b40a81d1d2cb1152d4b05baf7ec4a0acb11f1085c431ab63f2"}},"kernel_objects":[{"artifact":{"path":"objects/IntegerMainBinding.olean","bytes":50624,"sha256":"6929dd38ce919384e12704264de6a40b98a44bdc2894661d404a1b1fc2721df4"},"claim_ids":["integer_main_eq1","integer_maximum"]},{"artifact":{"path":"objects/PrimaryMain.olean","bytes":321528,"sha256":"09bdd592ef25e414bb7d53f7c2f08011d5cd61e90902968afd9f65c635c497c5"},"claim_ids":["main_eq1"]}],"lakefile_sha256":"7a0f61511e9ae54f26f812589428a53b36d5d2ddf03265f903de78b21bcb13f2","toolchain_sha256":"bc84812c94489d1e3e191baa1dc10d5eb684382d7fe9d2a5ab085e72c1c67e47","validator_sha256":"5cc20458707b1c0f1276c42fcc7bfa95bec570777832b10bae32540464cb2c3a","artifact_bindings":[{"artifact":{"path":"ActualBoundingSieve.lean","bytes":7575,"sha256":"594b6695d429f3f3afd144925eb7567b613ca6ba4c9ee56a2de6d260f5f32782"},"representation":{"kind":"manifest","path":"ActualBoundingSieve.lean"}},{"artifact":{"path":"Arithmetic.lean","bytes":2826,"sha256":"e97f06258ece1ed02d30a73e73149bcf4cdf695b188fd3b7d7049dfec6270a75"},"representation":{"kind":"manifest","path":"Arithmetic.lean"}},{"artifact":{"path":"Bridges.lean","bytes":1887,"sha256":"abb24fd3e031f070ff19c20cebbb2063eb22d76c75c8c0f891ad5c9f62f671be"},"representation":{"kind":"manifest","path":"Bridges.lean"}},{"artifact":{"path":"CRTMoments.lean","bytes":6959,"sha256":"a9ef14df63a94ed4b51dc1c290b4cbb750ca517c58a519020ffc7e30b5e7fb36"},"representation":{"kind":"manifest","path":"CRTMoments.lean"}},{"artifact":{"path":"DivisorMoments.lean","bytes":6215,"sha256":"9be86aa88442c3c7662442d662adfe6266529d413c0f47670fc99cdc2a65eaf3"},"representation":{"kind":"manifest","path":"DivisorMoments.lean"}},{"artifact":{"path":"EarlyCover.lean","bytes":13488,"sha256":"0b884aca9d50098665535a5bd4dedd9fa00e96b95b13fb8e48a4037b83ca9f59"},"representation":{"kind":"manifest","path":"EarlyCover.lean"}},{"artifact":{"path":"EulerRatio.lean","bytes":7674,"sha256":"0a09cda1f89f410af890f9085bfbda225136f69ebeab17fbd5ba5e4d13350294"},"representation":{"kind":"manifest","path":"EulerRatio.lean"}},{"artifact":{"path":"FactorialLogBounds.lean","bytes":3391,"sha256":"0b396c1731097a09b0a154b3c54c2b102699e880b5c51aae984ae58f88e564ea"},"representation":{"kind":"manifest","path":"FactorialLogBounds.lean"}},{"artifact":{"path":"FactorialWheel.lean","bytes":7919,"sha256":"4f2baae48b58657da06269f91c7534bb8293b6a4943f62e8fe40897927181ea4"},"representation":{"kind":"manifest","path":"FactorialWheel.lean"}},{"artifact":{"path":"FiniteCoreTargets.lean","bytes":8486,"sha256":"5b066b89aa7939e5d37da8fbc48778e20119fe4ae0e8c91277b62183724d2cee"},"representation":{"kind":"manifest","path":"FiniteCoreTargets.lean"}},{"artifact":{"path":"Gaps.lean","bytes":4544,"sha256":"8ba9d1d44ad5c19bceea560734b271516e2fbb2032af4ba62875436090c1b30f"},"representation":{"kind":"manifest","path":"Gaps.lean"}},{"artifact":{"path":"IncidenceMoments.lean","bytes":4496,"sha256":"e91ba8ae5e2d5083ec5946a9a3da2907ebccdc209eb7a595098f44a494757021"},"representation":{"kind":"manifest","path":"IncidenceMoments.lean"}},{"artifact":{"path":"IntegerMainBinding.lean","bytes":2817,"sha256":"6a87d6209746e706bd2d44629f0333815b36a2f542d609ca8ff13f682d889e09"},"representation":{"kind":"manifest","path":"IntegerMainBinding.lean"}},{"artifact":{"path":"ManuscriptParameters.lean","bytes":13267,"sha256":"927d7e627436e197b3b644bc13866bea4775b820eaa332af13966de0c40fce03"},"representation":{"kind":"manifest","path":"ManuscriptParameters.lean"}},{"artifact":{"path":"ManuscriptResidues.lean","bytes":9653,"sha256":"a2ca43af4c608c303a7a2b1e61ca6b04677e636017937c3161e5c6fe1c272515"},"representation":{"kind":"manifest","path":"ManuscriptResidues.lean"}},{"artifact":{"path":"MertensBand.lean","bytes":21850,"sha256":"6ee922c80814b35e0d47011a2bcb164e99467c85d190f92eb098ab8ba9be17d9"},"representation":{"kind":"manifest","path":"MertensBand.lean"}},{"artifact":{"path":"Normalization.lean","bytes":3693,"sha256":"81662d512a792fc7530c6330859809ca715567c15190a0ef71998773c90106be"},"representation":{"kind":"manifest","path":"Normalization.lean"}},{"artifact":{"path":"PrimaryMain.lean","bytes":4432,"sha256":"cff1bb8609e7ca834419684da3c81bb8630f85a7730ea5b0dd3018f24504ed68"},"representation":{"kind":"manifest","path":"PrimaryMain.lean"}},{"artifact":{"path":"PrimeFactorial.lean","bytes":7027,"sha256":"515c254617ee171c49108aa3509c8e7e3b98bdb0a7ff7d4703db97fd9bd8ecc4"},"representation":{"kind":"manifest","path":"PrimeFactorial.lean"}},{"artifact":{"path":"PrimeLog.lean","bytes":13299,"sha256":"8ef54f9d6fb8d484e2f9822ccd5ad063d93cf7141e8f1dc8c0bbc6d41022bd90"},"representation":{"kind":"manifest","path":"PrimeLog.lean"}},{"artifact":{"path":"PrimePowerTail.lean","bytes":8032,"sha256":"f496214b282b394abb5f0b5ded6c45a06eb17dab92095c56023e0728b5c4f2c8"},"representation":{"kind":"manifest","path":"PrimePowerTail.lean"}},{"artifact":{"path":"PrimePsiBounds.lean","bytes":4468,"sha256":"2f26fc0a8102841431a82579107d29d58ab33defaed2cbd98a8c5aa73a1d4219"},"representation":{"kind":"manifest","path":"PrimePsiBounds.lean"}},{"artifact":{"path":"PrimeReserveBudget.lean","bytes":11928,"sha256":"1895d0e7ea7cc573477a2ca95f98d5f7b9ecde7b6330b230f4cc9e4afaf7e5ea"},"representation":{"kind":"manifest","path":"PrimeReserveBudget.lean"}},{"artifact":{"path":"RealBand.lean","bytes":10779,"sha256":"879496b2388f74b475fa7ac85918f76d58b3a9a671c64fbd9128b11cbebeac36"},"representation":{"kind":"manifest","path":"RealBand.lean"}},{"artifact":{"path":"ReserveBudget.lean","bytes":8664,"sha256":"dfaf920d927f70fdea77cf67290461f1235e20fd0234c91f3a2d897351a888c0"},"representation":{"kind":"manifest","path":"ReserveBudget.lean"}},{"artifact":{"path":"Reserved.lean","bytes":1691,"sha256":"e6db9eb6ac6ddfbb7c0ca582c6ab11ef0392c0fa39b50d8b5e71c34434037847"},"representation":{"kind":"manifest","path":"Reserved.lean"}},{"artifact":{"path":"ResidueMoment.lean","bytes":3828,"sha256":"abd6a25cb565c497da27662b21a1fa1a1277dfadd05980910a716329168757a9"},"representation":{"kind":"manifest","path":"ResidueMoment.lean"}},{"artifact":{"path":"SelbergError.lean","bytes":9500,"sha256":"3ee375547c7fd4acd5796f3f072be725abeba7d2f2f9b40cf73b3f7313c5402f"},"representation":{"kind":"manifest","path":"SelbergError.lean"}},{"artifact":{"path":"SelbergEuler.lean","bytes":10733,"sha256":"a6e6cf8796eeb4e43a5351f90e932304632a819638c34202da04efb0e8da7d56"},"representation":{"kind":"manifest","path":"SelbergEuler.lean"}},{"artifact":{"path":"SelbergFinite.lean","bytes":10339,"sha256":"8b10b2d4bc002b7dc6067b0b73197cf4715b0c3c7ca601025942c2ed84ec0177"},"representation":{"kind":"manifest","path":"SelbergFinite.lean"}},{"artifact":{"path":"ShiftedRankin.lean","bytes":13767,"sha256":"3e0eaa6620c3c8dfb95771fc7fa2566fa10bc28f69954cf786e6485a838f5986"},"representation":{"kind":"manifest","path":"ShiftedRankin.lean"}},{"artifact":{"path":"SieveCoarse.lean","bytes":7222,"sha256":"8bc57801384e29fc3b6d53e4bec64cea1fb4f77865fdb36fb5b834e457ac5d03"},"representation":{"kind":"manifest","path":"SieveCoarse.lean"}},{"artifact":{"path":"SieveInterface.lean","bytes":6760,"sha256":"ea07fcd56eb2688d70125f4b0ed11080554dc56821fd73489ab5683882384d73"},"representation":{"kind":"manifest","path":"SieveInterface.lean"}},{"artifact":{"path":"SieveParameters.lean","bytes":10211,"sha256":"f7d83b195e5748ef941f5d7a1c9fcd9b11ad99893bac45b9342e1d558939007b"},"representation":{"kind":"manifest","path":"SieveParameters.lean"}},{"artifact":{"path":"SmoothBudget.lean","bytes":10322,"sha256":"d69ec8f998d2c866e97eaeb92c7f7c3f237e642d919f52b99e6543dc47949bc2"},"representation":{"kind":"manifest","path":"SmoothBudget.lean"}},{"artifact":{"path":"SmoothLogLimit.lean","bytes":8336,"sha256":"0f2f603ee9dd4764942eaddca94f211015ff1fba8737abe7dfddaca8f025a976"},"representation":{"kind":"manifest","path":"SmoothLogLimit.lean"}},{"artifact":{"path":"SmoothParameters.lean","bytes":16567,"sha256":"0e231daeee4396300239389fcc537f9cd442ee88dcce3a5281d2ac7efeebcb2a"},"representation":{"kind":"manifest","path":"SmoothParameters.lean"}},{"artifact":{"path":"SmoothRankin.lean","bytes":5979,"sha256":"3675eac4ebf6fca98e99e8cd1ee54bf133cbf45925f1e54f45f6d0df0fa79d53"},"representation":{"kind":"manifest","path":"SmoothRankin.lean"}},{"artifact":{"path":"archives/Cli.tar.gz","bytes":23876,"sha256":"119fd61f1ee8b4376de3f01a540424c2618fcba4ab38c2b6a697fcfb757be237"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"archives/Lean.tar.zst","bytes":596161714,"sha256":"547091cea0df5f61d0998998e9dc32464a8d9529f60a6f14baf73595370c30d8"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"archives/LeanSearchClient.tar.gz","bytes":13229,"sha256":"21d6513e6b37cf1ec899b4bd3b0b184ff299d059d08789dc703bbdef2145836f"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"archives/Qq.tar.gz","bytes":33007,"sha256":"a837e14f7f055aeec15b1c72071ff3b28d5ccf172fb48891d2bb75b91ac9c62b"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"archives/aesop.tar.gz","bytes":207917,"sha256":"be040953d273567e9a6bf8d893c6d6793f901d7f4af2b911f9ad3eb5a6f87bbd"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"archives/batteries.tar.gz","bytes":362571,"sha256":"e3c040b62d3bbf5e8d4aac7802705ce7a4529e613384cdce9bd2c18e8e8a9a0f"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"archives/importGraph.tar.gz","bytes":178648,"sha256":"cb6e0d3370348fc71aafc0126037c3798f3a726530df66b27b1ba78ecd432480"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"archives/mathlib.tar.gz","bytes":23975695,"sha256":"ec571dd26863b987ec0b13909aeda4bac8a5325e5f9674a3b21d5105df9b47c3"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"archives/plausible.tar.gz","bytes":43036,"sha256":"e6642441c71dd612ad1593aa6611be6505df62a94c1e06f5b574323f8f528c58"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"archives/proofwidgets.tar.gz","bytes":3897051,"sha256":"6d6d93d7c0bddfa4c2b3e1043df94398bc969cbba4031e2c10332363ed4db575"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"capsule_codec.py","bytes":10118,"sha256":"63f9cc5e542bf084598d0204bdfeeb5554319cbddddda4c8ba2e53e272493b17"},"representation":{"kind":"manifest","path":"capsule_codec.py"}},{"artifact":{"path":"checker/KernelReplay.lean","bytes":6784,"sha256":"d6a4d04105b36ac5b5a3d520635add8b10107451f6f91676ca142e24ead5cf59"},"representation":{"kind":"manifest","path":"checker/KernelReplay.lean"}},{"artifact":{"path":"checker/kernel-build-provenance.json","bytes":1433,"sha256":"63f6c8c7421f08b40a81d1d2cb1152d4b05baf7ec4a0acb11f1085c431ab63f2"},"representation":{"kind":"manifest","path":"checker/kernel-build-provenance.json"}},{"artifact":{"path":"checker/kernel-config.json","bytes":1623,"sha256":"ec0b1826a7677917b22411666d571fa9d853556d050f9bb4e7a493d40ed0703d"},"representation":{"kind":"manifest","path":"checker/kernel-config.json"}},{"artifact":{"path":"checker/kernel-invocation.md","bytes":3764,"sha256":"9dd833d1d1914627869daf7e6901ec131f25c399a88843ab8eab44d01ab76780"},"representation":{"kind":"manifest","path":"checker/kernel-invocation.md"}},{"artifact":{"path":"checker/kernel-object-inventory.json","bytes":1046,"sha256":"4d521d484b1dd8aa15b62c98f2df05521518b900b9ed8b53a5a8f25d2108522c"},"representation":{"kind":"manifest","path":"checker/kernel-object-inventory.json"}},{"artifact":{"path":"checker/kernel-operator-capsule.json","bytes":1645525,"sha256":"b6cf97493d04db4bb0761ddc807a6d2856d1141012deab22f3edf8331a728121"},"representation":{"kind":"manifest","path":"checker/kernel-operator-capsule.json"}},{"artifact":{"path":"checker/kernel-source-inventory.json","bytes":1155531,"sha256":"486961784524459dd1e344bf1ff50fd8c6c67ec103a0edf3d96f3df1ee15eb97"},"representation":{"kind":"manifest","path":"checker/kernel-source-inventory.json"}},{"artifact":{"path":"checker/lean_kernel_validator.py","bytes":24409,"sha256":"5cc20458707b1c0f1276c42fcc7bfa95bec570777832b10bae32540464cb2c3a"},"representation":{"kind":"manifest","path":"checker/lean_kernel_validator.py"}},{"artifact":{"path":"dependencies/mathlib/lake-manifest.json","bytes":2815,"sha256":"479029d834847680ed9088932ae66767daab8b1328a1e88dc3ed256008c20156"},"representation":{"kind":"manifest","path":"dependencies/mathlib/lake-manifest.json"}},{"artifact":{"path":"dependencies/mathlib/lakefile.lean","bytes":8214,"sha256":"7a0f61511e9ae54f26f812589428a53b36d5d2ddf03265f903de78b21bcb13f2"},"representation":{"kind":"manifest","path":"dependencies/mathlib/lakefile.lean"}},{"artifact":{"path":"dependencies/tool-and-source-descriptor.json","bytes":8950,"sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f"},"representation":{"kind":"manifest","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"evidence-and-tool-source-capsule.json","bytes":100818,"sha256":"ce8d443da0e34e2a822d30fa489d3673e1fbef240f31f64df313d83e5ded4cf1"},"representation":{"kind":"manifest","path":"evidence-and-tool-source-capsule.json"}},{"artifact":{"path":"lean-toolchain.txt","bytes":29,"sha256":"bc84812c94489d1e3e191baa1dc10d5eb684382d7fe9d2a5ab085e72c1c67e47"},"representation":{"kind":"manifest","path":"lean-toolchain.txt"}},{"artifact":{"path":"mandatory-primitives-appendix.txt","bytes":1039,"sha256":"30f9119e15ac05580a993ba89cb673ddcd7bde17b9ae5aa2d6178b5af653f3f7"},"representation":{"kind":"manifest","path":"mandatory-primitives-appendix.txt"}},{"artifact":{"path":"manuscript.md","bytes":41786,"sha256":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80"},"representation":{"kind":"manifest","path":"manuscript.md"}},{"artifact":{"path":"objects/IntegerMainBinding.olean","bytes":50624,"sha256":"6929dd38ce919384e12704264de6a40b98a44bdc2894661d404a1b1fc2721df4"},"representation":{"kind":"descriptor","path":"checker/kernel-object-inventory.json"}},{"artifact":{"path":"objects/PrimaryMain.olean","bytes":321528,"sha256":"09bdd592ef25e414bb7d53f7c2f08011d5cd61e90902968afd9f65c635c497c5"},"representation":{"kind":"descriptor","path":"checker/kernel-object-inventory.json"}},{"artifact":{"path":"ordered-export-index.json","bytes":2310,"sha256":"35a8988a0cd98ce09ca83afeebaad6504c078b5d56fad1dcf5e4698c591368ca"},"representation":{"kind":"manifest","path":"ordered-export-index.json"}},{"artifact":{"path":"original-manuscript-verbatim.md","bytes":29256,"sha256":"50a60a0344a8a32d025499caf26983534df363d9d0c9988e41adbdc2d416b521"},"representation":{"kind":"manifest","path":"original-manuscript-verbatim.md"}},{"artifact":{"path":"proof-export-00.xz.b64.txt","bytes":4274509,"sha256":"0e3005a1296eb4195346cfffd672be1400a2bf6f1cbd88c7e09c2b31e4a5786f"},"representation":{"kind":"manifest","path":"proof-export-00.xz.b64.txt"}},{"artifact":{"path":"proof-export-01.xz.b64.txt","bytes":4364161,"sha256":"f8d5e87d196ef8b5ca50e8233383433618f7d057f02add5bafb392dc0f3067b6"},"representation":{"kind":"manifest","path":"proof-export-01.xz.b64.txt"}},{"artifact":{"path":"proof-export-02.xz.b64.txt","bytes":4182157,"sha256":"4cce6e4f80c2f9f9631e8305f109f43b18f757069c423f59820390e9da8e84aa"},"representation":{"kind":"manifest","path":"proof-export-02.xz.b64.txt"}},{"artifact":{"path":"proof-export-03.xz.b64.txt","bytes":3275097,"sha256":"9ebf6aa419c56e9abca59c8e09870218f974baaaed20581257a29fe89e60d0cc"},"representation":{"kind":"manifest","path":"proof-export-03.xz.b64.txt"}},{"artifact":{"path":"proof-to-exposition-map.json","bytes":84509,"sha256":"b6b75ca5c75fa20a4050dc73b12f4a375427a5686361e41f3033835bf485f2d5"},"representation":{"kind":"manifest","path":"proof-to-exposition-map.json"}},{"artifact":{"path":"proofs/solution.export","bytes":123033220,"sha256":"959863eb59e67e4d6a0248d268e23e2dfa6ec5945c9d9d218fc2973103cefbeb"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"source-recipe-capsule.json","bytes":1775428,"sha256":"0183eae2191e7fc260754887dd9c9beb155ae20f0b842d5edb2f24e183237cc8"},"representation":{"kind":"manifest","path":"source-recipe-capsule.json"}},{"artifact":{"path":"statement-bundle.json","bytes":11662,"sha256":"1f3f0a4bc27f24de44aef5a53389f70e0797a9883687b54e695db5257dd50ad6"},"representation":{"kind":"manifest","path":"statement-bundle.json"}},{"artifact":{"path":"tool-binaries/comparator","bytes":130769536,"sha256":"4e3d5988a258885dc84123ed762b84e5244ce6412952c56f72ac760db3c54946"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"tool-binaries/lean","bytes":13824,"sha256":"72d674b469a5732f69b4d6408c215040c227cc25b4c6b7c7826c16fe19e088b3"},"representation":{"kind":"descriptor","path":"checker/kernel-object-inventory.json"}},{"artifact":{"path":"tool-binaries/nanoda_bin","bytes":1399320,"sha256":"de22a5b99965ee6560a096f3e46cbbbd5697ee59b3537566fb49e8ed46a7ac6e"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"tool-binaries/no-unix","bytes":70512,"sha256":"1426e52ad66615bb1f6eb2fb67fd945c4f5f51029e7105bf0646430c610beea6"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"tool-source/comparator.tar.gz","bytes":21432,"sha256":"02d5fa24fddaa000b598b698c534fdafd2cda47c87cce48abcb2f27c5f03906f"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"tool-source/nanoda.tar.gz","bytes":91576,"sha256":"2fcf51c0fb97b909dd2b232e1a6d4c39fe0e8c9b4cb8a01c66a00e2e4b3c45c8"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}},{"artifact":{"path":"tools/tool-provenance/no-unix.c","bytes":619,"sha256":"ae18c95db48f3a89076aa3b7cf572e6ba84c29e6ee59e5404ae288695735adde"},"representation":{"kind":"descriptor","path":"dependencies/tool-and-source-descriptor.json"}}],"manuscript_sha256":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80","execution_identity":{"tools":[{"name":"lean","revision":"470d5ce1400764999581fd26d5d72b00d990b0f4","source_kind":"released-toolchain","binary_sha256":"72d674b469a5732f69b4d6408c215040c227cc25b4c6b7c7826c16fe19e088b3","source_sha256":"547091cea0df5f61d0998998e9dc32464a8d9529f60a6f14baf73595370c30d8"}],"schema":"solveathome-lean-execution-contract-v2","isolation":{"network":"none","no_secrets":true,"capabilities":[],"unprivileged":true,"policy_sha256":"ec0b1826a7677917b22411666d571fa9d853556d050f9bb4e7a493d40ed0703d","root_readonly":true,"no_host_mounts":true,"inputs_readonly":true,"no_new_privileges":true,"compilation_separate":true},"resources":{"pids":256,"cpu_count":2,"memory_bytes":4294967296,"wall_seconds":1200,"scratch_bytes":7516192768,"log_stream_bytes":8388608},"validator":{"path":"checker/lean_kernel_validator.py","bytes":24409,"sha256":"5cc20458707b1c0f1276c42fcc7bfa95bec570777832b10bae32540464cb2c3a"},"invocation":{"path":"checker/kernel-invocation.md","bytes":3764,"sha256":"9dd833d1d1914627869daf7e6901ec131f25c399a88843ab8eab44d01ab76780"},"runtime_paths":{"tools":"/opt/lean/bin","exports":"/scratch/unused","package":"/package","scratch":"/scratch","support":"/support","lean_prefix":"/opt/lean"},"package_artifacts":[{"path":"capsule_codec.py","bytes":10118,"sha256":"63f9cc5e542bf084598d0204bdfeeb5554319cbddddda4c8ba2e53e272493b17"},{"path":"checker/kernel-build-provenance.json","bytes":1433,"sha256":"63f6c8c7421f08b40a81d1d2cb1152d4b05baf7ec4a0acb11f1085c431ab63f2"},{"path":"checker/kernel-config.json","bytes":1623,"sha256":"ec0b1826a7677917b22411666d571fa9d853556d050f9bb4e7a493d40ed0703d"},{"path":"checker/kernel-invocation.md","bytes":3764,"sha256":"9dd833d1d1914627869daf7e6901ec131f25c399a88843ab8eab44d01ab76780"},{"path":"checker/kernel-operator-capsule.json","bytes":1645525,"sha256":"b6cf97493d04db4bb0761ddc807a6d2856d1141012deab22f3edf8331a728121"},{"path":"checker/kernel-source-inventory.json","bytes":1155531,"sha256":"486961784524459dd1e344bf1ff50fd8c6c67ec103a0edf3d96f3df1ee15eb97"},{"path":"checker/KernelReplay.lean","bytes":6784,"sha256":"d6a4d04105b36ac5b5a3d520635add8b10107451f6f91676ca142e24ead5cf59"},{"path":"checker/lean_kernel_validator.py","bytes":24409,"sha256":"5cc20458707b1c0f1276c42fcc7bfa95bec570777832b10bae32540464cb2c3a"}]},"scientific_identity":{"claims":[{"id":"integer_main_eq1","target":"IntegerMainBinding.lean","locator":"Revised manuscript Sections 1 and 8: Eq.(1) with the attained integer-gap definition and full prime cutoff.","coverage":"full","assumptions":[],"declaration":"IntegerMainBinding.manuscript_integer_main_goal"},{"id":"integer_maximum","target":"IntegerMainBinding.lean","locator":"Revised manuscript Section 1: attained largest gap over all integer starts, including negative starts and the period boundary.","coverage":"full","assumptions":[],"declaration":"IntegerMainBinding.integer_maximum_binding"},{"id":"main_eq1","target":"PrimaryMain.lean","locator":"Revised manuscript Sections 1 and 8, Eq.(1): eventual full-prime-cutoff cyclic two-residue survivor-gap bound.","coverage":"full","assumptions":[],"declaration":"PrimaryMain.manuscript_main_goal"}],"schema":"solveathome-lean-scientific-v2","manuscript":{"path":"manuscript.md","bytes":41786,"sha256":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80"},"paper_slug":"kk-lower-bound","axiom_policy":["Classical.choice","Quot.sound","propext"],"proof_artifacts":[{"artifact":{"path":"proofs/solution.export","bytes":123033220,"sha256":"959863eb59e67e4d6a0248d268e23e2dfa6ec5945c9d9d218fc2973103cefbeb"},"claim_ids":["integer_main_eq1","integer_maximum","main_eq1"]}],"source_artifacts":[{"path":"ActualBoundingSieve.lean","bytes":7575,"sha256":"594b6695d429f3f3afd144925eb7567b613ca6ba4c9ee56a2de6d260f5f32782"},{"path":"Arithmetic.lean","bytes":2826,"sha256":"e97f06258ece1ed02d30a73e73149bcf4cdf695b188fd3b7d7049dfec6270a75"},{"path":"Bridges.lean","bytes":1887,"sha256":"abb24fd3e031f070ff19c20cebbb2063eb22d76c75c8c0f891ad5c9f62f671be"},{"path":"CRTMoments.lean","bytes":6959,"sha256":"a9ef14df63a94ed4b51dc1c290b4cbb750ca517c58a519020ffc7e30b5e7fb36"},{"path":"dependencies/mathlib/lake-manifest.json","bytes":2815,"sha256":"479029d834847680ed9088932ae66767daab8b1328a1e88dc3ed256008c20156"},{"path":"dependencies/mathlib/lakefile.lean","bytes":8214,"sha256":"7a0f61511e9ae54f26f812589428a53b36d5d2ddf03265f903de78b21bcb13f2"},{"path":"DivisorMoments.lean","bytes":6215,"sha256":"9be86aa88442c3c7662442d662adfe6266529d413c0f47670fc99cdc2a65eaf3"},{"path":"EarlyCover.lean","bytes":13488,"sha256":"0b884aca9d50098665535a5bd4dedd9fa00e96b95b13fb8e48a4037b83ca9f59"},{"path":"EulerRatio.lean","bytes":7674,"sha256":"0a09cda1f89f410af890f9085bfbda225136f69ebeab17fbd5ba5e4d13350294"},{"path":"FactorialLogBounds.lean","bytes":3391,"sha256":"0b396c1731097a09b0a154b3c54c2b102699e880b5c51aae984ae58f88e564ea"},{"path":"FactorialWheel.lean","bytes":7919,"sha256":"4f2baae48b58657da06269f91c7534bb8293b6a4943f62e8fe40897927181ea4"},{"path":"FiniteCoreTargets.lean","bytes":8486,"sha256":"5b066b89aa7939e5d37da8fbc48778e20119fe4ae0e8c91277b62183724d2cee"},{"path":"Gaps.lean","bytes":4544,"sha256":"8ba9d1d44ad5c19bceea560734b271516e2fbb2032af4ba62875436090c1b30f"},{"path":"IncidenceMoments.lean","bytes":4496,"sha256":"e91ba8ae5e2d5083ec5946a9a3da2907ebccdc209eb7a595098f44a494757021"},{"path":"IntegerMainBinding.lean","bytes":2817,"sha256":"6a87d6209746e706bd2d44629f0333815b36a2f542d609ca8ff13f682d889e09"},{"path":"lean-toolchain.txt","bytes":29,"sha256":"bc84812c94489d1e3e191baa1dc10d5eb684382d7fe9d2a5ab085e72c1c67e47"},{"path":"ManuscriptParameters.lean","bytes":13267,"sha256":"927d7e627436e197b3b644bc13866bea4775b820eaa332af13966de0c40fce03"},{"path":"ManuscriptResidues.lean","bytes":9653,"sha256":"a2ca43af4c608c303a7a2b1e61ca6b04677e636017937c3161e5c6fe1c272515"},{"path":"MertensBand.lean","bytes":21850,"sha256":"6ee922c80814b35e0d47011a2bcb164e99467c85d190f92eb098ab8ba9be17d9"},{"path":"Normalization.lean","bytes":3693,"sha256":"81662d512a792fc7530c6330859809ca715567c15190a0ef71998773c90106be"},{"path":"PrimaryMain.lean","bytes":4432,"sha256":"cff1bb8609e7ca834419684da3c81bb8630f85a7730ea5b0dd3018f24504ed68"},{"path":"PrimeFactorial.lean","bytes":7027,"sha256":"515c254617ee171c49108aa3509c8e7e3b98bdb0a7ff7d4703db97fd9bd8ecc4"},{"path":"PrimeLog.lean","bytes":13299,"sha256":"8ef54f9d6fb8d484e2f9822ccd5ad063d93cf7141e8f1dc8c0bbc6d41022bd90"},{"path":"PrimePowerTail.lean","bytes":8032,"sha256":"f496214b282b394abb5f0b5ded6c45a06eb17dab92095c56023e0728b5c4f2c8"},{"path":"PrimePsiBounds.lean","bytes":4468,"sha256":"2f26fc0a8102841431a82579107d29d58ab33defaed2cbd98a8c5aa73a1d4219"},{"path":"PrimeReserveBudget.lean","bytes":11928,"sha256":"1895d0e7ea7cc573477a2ca95f98d5f7b9ecde7b6330b230f4cc9e4afaf7e5ea"},{"path":"proof-to-exposition-map.json","bytes":84509,"sha256":"b6b75ca5c75fa20a4050dc73b12f4a375427a5686361e41f3033835bf485f2d5"},{"path":"RealBand.lean","bytes":10779,"sha256":"879496b2388f74b475fa7ac85918f76d58b3a9a671c64fbd9128b11cbebeac36"},{"path":"ReserveBudget.lean","bytes":8664,"sha256":"dfaf920d927f70fdea77cf67290461f1235e20fd0234c91f3a2d897351a888c0"},{"path":"Reserved.lean","bytes":1691,"sha256":"e6db9eb6ac6ddfbb7c0ca582c6ab11ef0392c0fa39b50d8b5e71c34434037847"},{"path":"ResidueMoment.lean","bytes":3828,"sha256":"abd6a25cb565c497da27662b21a1fa1a1277dfadd05980910a716329168757a9"},{"path":"SelbergError.lean","bytes":9500,"sha256":"3ee375547c7fd4acd5796f3f072be725abeba7d2f2f9b40cf73b3f7313c5402f"},{"path":"SelbergEuler.lean","bytes":10733,"sha256":"a6e6cf8796eeb4e43a5351f90e932304632a819638c34202da04efb0e8da7d56"},{"path":"SelbergFinite.lean","bytes":10339,"sha256":"8b10b2d4bc002b7dc6067b0b73197cf4715b0c3c7ca601025942c2ed84ec0177"},{"path":"ShiftedRankin.lean","bytes":13767,"sha256":"3e0eaa6620c3c8dfb95771fc7fa2566fa10bc28f69954cf786e6485a838f5986"},{"path":"SieveCoarse.lean","bytes":7222,"sha256":"8bc57801384e29fc3b6d53e4bec64cea1fb4f77865fdb36fb5b834e457ac5d03"},{"path":"SieveInterface.lean","bytes":6760,"sha256":"ea07fcd56eb2688d70125f4b0ed11080554dc56821fd73489ab5683882384d73"},{"path":"SieveParameters.lean","bytes":10211,"sha256":"f7d83b195e5748ef941f5d7a1c9fcd9b11ad99893bac45b9342e1d558939007b"},{"path":"SmoothBudget.lean","bytes":10322,"sha256":"d69ec8f998d2c866e97eaeb92c7f7c3f237e642d919f52b99e6543dc47949bc2"},{"path":"SmoothLogLimit.lean","bytes":8336,"sha256":"0f2f603ee9dd4764942eaddca94f211015ff1fba8737abe7dfddaca8f025a976"},{"path":"SmoothParameters.lean","bytes":16567,"sha256":"0e231daeee4396300239389fcc537f9cd442ee88dcce3a5281d2ac7efeebcb2a"},{"path":"SmoothRankin.lean","bytes":5979,"sha256":"3675eac4ebf6fca98e99e8cd1ee54bf133cbf45925f1e54f45f6d0df0fa79d53"}],"statement_bundle":{"path":"statement-bundle.json","bytes":11662,"sha256":"1f3f0a4bc27f24de44aef5a53389f70e0797a9883687b54e695db5257dd50ad6"},"semantic_dependencies":[{"name":"Cli","source":{"path":"archives/Cli.tar.gz","bytes":23876,"sha256":"119fd61f1ee8b4376de3f01a540424c2618fcba4ab38c2b6a697fcfb757be237"},"revision":"843844fa601dd56767b1eb22b7ada5b64d5e567a","source_kind":"source-archive"},{"name":"Lean","source":{"path":"archives/Lean.tar.zst","bytes":596161714,"sha256":"547091cea0df5f61d0998998e9dc32464a8d9529f60a6f14baf73595370c30d8"},"revision":"470d5ce1400764999581fd26d5d72b00d990b0f4","source_kind":"released-toolchain"},{"name":"LeanSearchClient","source":{"path":"archives/LeanSearchClient.tar.gz","bytes":13229,"sha256":"21d6513e6b37cf1ec899b4bd3b0b184ff299d059d08789dc703bbdef2145836f"},"revision":"50cd21bc62f2c8357c4f269d1185921cbfcdfc90","source_kind":"source-archive"},{"name":"Qq","source":{"path":"archives/Qq.tar.gz","bytes":33007,"sha256":"a837e14f7f055aeec15b1c72071ff3b28d5ccf172fb48891d2bb75b91ac9c62b"},"revision":"d93a8a0622807953d1e424f0fe2a5f5b5520c12e","source_kind":"source-archive"},{"name":"aesop","source":{"path":"archives/aesop.tar.gz","bytes":207917,"sha256":"be040953d273567e9a6bf8d893c6d6793f901d7f4af2b911f9ad3eb5a6f87bbd"},"revision":"36cb0105a76ff3de70add8ae91afb6cfc57fafe3","source_kind":"source-archive"},{"name":"batteries","source":{"path":"archives/batteries.tar.gz","bytes":362571,"sha256":"e3c040b62d3bbf5e8d4aac7802705ce7a4529e613384cdce9bd2c18e8e8a9a0f"},"revision":"ec2288a9bf12ecc05a459c5db5aac77f4c73424c","source_kind":"source-archive"},{"name":"importGraph","source":{"path":"archives/importGraph.tar.gz","bytes":178648,"sha256":"cb6e0d3370348fc71aafc0126037c3798f3a726530df66b27b1ba78ecd432480"},"revision":"7ad9f2e325aa6cec3dacaa97c2653a98032750eb","source_kind":"source-archive"},{"name":"mathlib","source":{"path":"archives/mathlib.tar.gz","bytes":23975695,"sha256":"ec571dd26863b987ec0b13909aeda4bac8a5325e5f9674a3b21d5105df9b47c3"},"revision":"331d5244f0d3aad530d9ab00ded135b4c7691502","source_kind":"source-archive"},{"name":"plausible","source":{"path":"archives/plausible.tar.gz","bytes":43036,"sha256":"e6642441c71dd612ad1593aa6611be6505df62a94c1e06f5b574323f8f528c58"},"revision":"afc2695efcb6855264d85a45632db1ddc56c8774","source_kind":"source-archive"},{"name":"proofwidgets","source":{"path":"archives/proofwidgets.tar.gz","bytes":3897051,"sha256":"6d6d93d7c0bddfa4c2b3e1043df94398bc969cbba4031e2c10332363ed4db575"},"revision":"87dfe779d5dfd03142ee4fe158911b8eb553ec98","source_kind":"source-archive"}]},"statement_review_id":695,"lake_manifest_sha256":"479029d834847680ed9088932ae66767daab8b1328a1e88dc3ed256008c20156","statement_bundle_sha256":"1f3f0a4bc27f24de44aef5a53389f70e0797a9883687b54e695db5257dd50ad6"},"claim":"The unchanged three mapped main declarations are submitted under the separately named Lean-kernel-v1 assurance profile; current execution and final judgment remain pending.","scope":"Exact frozen38 authored Lean sources, manuscript and statements; pinned semantic dependencies and declared retained compiler objects. Lean-kernel assurance replays the actual mapped declarations and reachable proof closure. It does not establish export/comparator/Nanoda validation or the stronger lean-comparator-v2 profile. O1-O7 remain OPEN.","tools":["python3","lean","linux"],"inputs":["6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80","1f3f0a4bc27f24de44aef5a53389f70e0797a9883687b54e695db5257dd50ad6","486961784524459dd1e344bf1ff50fd8c6c67ec103a0edf3d96f3df1ee15eb97","4d521d484b1dd8aa15b62c98f2df05521518b900b9ed8b53a5a8f25d2108522c","63f6c8c7421f08b40a81d1d2cb1152d4b05baf7ec4a0acb11f1085c431ab63f2"],"checker":"5cc20458707b1c0f1276c42fcc7bfa95bec570777832b10bae32540464cb2c3a","command":"Inspect the pinned kernel invocation and operator source, reconstruct and verify all declared source/object inputs, then run the isolated Lean-kernel validator and its meaningful rejection controls. Supplementary exports and historical comparator machinery are not consumed or checked.","targets":["PrimaryMain.lean","IntegerMainBinding.lean"],"coverage":"decisive","expected":"Only a current genuinely observed authenticated Lean-kernel execution with successful source/object verification, exact mapped targets, permitted axiom closures and meaningful detected controls may support this separately named assurance tier.","manifest":[{"path":"ActualBoundingSieve.lean","role":"dependency","sha256":"594b6695d429f3f3afd144925eb7567b613ca6ba4c9ee56a2de6d260f5f32782"},{"path":"Arithmetic.lean","role":"dependency","sha256":"e97f06258ece1ed02d30a73e73149bcf4cdf695b188fd3b7d7049dfec6270a75"},{"path":"Bridges.lean","role":"dependency","sha256":"abb24fd3e031f070ff19c20cebbb2063eb22d76c75c8c0f891ad5c9f62f671be"},{"path":"CRTMoments.lean","role":"dependency","sha256":"a9ef14df63a94ed4b51dc1c290b4cbb750ca517c58a519020ffc7e30b5e7fb36"},{"path":"DivisorMoments.lean","role":"dependency","sha256":"9be86aa88442c3c7662442d662adfe6266529d413c0f47670fc99cdc2a65eaf3"},{"path":"EarlyCover.lean","role":"dependency","sha256":"0b884aca9d50098665535a5bd4dedd9fa00e96b95b13fb8e48a4037b83ca9f59"},{"path":"EulerRatio.lean","role":"dependency","sha256":"0a09cda1f89f410af890f9085bfbda225136f69ebeab17fbd5ba5e4d13350294"},{"path":"FactorialLogBounds.lean","role":"dependency","sha256":"0b396c1731097a09b0a154b3c54c2b102699e880b5c51aae984ae58f88e564ea"},{"path":"FactorialWheel.lean","role":"dependency","sha256":"4f2baae48b58657da06269f91c7534bb8293b6a4943f62e8fe40897927181ea4"},{"path":"FiniteCoreTargets.lean","role":"dependency","sha256":"5b066b89aa7939e5d37da8fbc48778e20119fe4ae0e8c91277b62183724d2cee"},{"path":"Gaps.lean","role":"dependency","sha256":"8ba9d1d44ad5c19bceea560734b271516e2fbb2032af4ba62875436090c1b30f"},{"path":"IncidenceMoments.lean","role":"dependency","sha256":"e91ba8ae5e2d5083ec5946a9a3da2907ebccdc209eb7a595098f44a494757021"},{"path":"IntegerMainBinding.lean","role":"target","sha256":"6a87d6209746e706bd2d44629f0333815b36a2f542d609ca8ff13f682d889e09"},{"path":"ManuscriptParameters.lean","role":"dependency","sha256":"927d7e627436e197b3b644bc13866bea4775b820eaa332af13966de0c40fce03"},{"path":"ManuscriptResidues.lean","role":"dependency","sha256":"a2ca43af4c608c303a7a2b1e61ca6b04677e636017937c3161e5c6fe1c272515"},{"path":"MertensBand.lean","role":"dependency","sha256":"6ee922c80814b35e0d47011a2bcb164e99467c85d190f92eb098ab8ba9be17d9"},{"path":"Normalization.lean","role":"dependency","sha256":"81662d512a792fc7530c6330859809ca715567c15190a0ef71998773c90106be"},{"path":"PrimaryMain.lean","role":"target","sha256":"cff1bb8609e7ca834419684da3c81bb8630f85a7730ea5b0dd3018f24504ed68"},{"path":"PrimeFactorial.lean","role":"dependency","sha256":"515c254617ee171c49108aa3509c8e7e3b98bdb0a7ff7d4703db97fd9bd8ecc4"},{"path":"PrimeLog.lean","role":"dependency","sha256":"8ef54f9d6fb8d484e2f9822ccd5ad063d93cf7141e8f1dc8c0bbc6d41022bd90"},{"path":"PrimePowerTail.lean","role":"dependency","sha256":"f496214b282b394abb5f0b5ded6c45a06eb17dab92095c56023e0728b5c4f2c8"},{"path":"PrimePsiBounds.lean","role":"dependency","sha256":"2f26fc0a8102841431a82579107d29d58ab33defaed2cbd98a8c5aa73a1d4219"},{"path":"PrimeReserveBudget.lean","role":"dependency","sha256":"1895d0e7ea7cc573477a2ca95f98d5f7b9ecde7b6330b230f4cc9e4afaf7e5ea"},{"path":"RealBand.lean","role":"dependency","sha256":"879496b2388f74b475fa7ac85918f76d58b3a9a671c64fbd9128b11cbebeac36"},{"path":"ReserveBudget.lean","role":"dependency","sha256":"dfaf920d927f70fdea77cf67290461f1235e20fd0234c91f3a2d897351a888c0"},{"path":"Reserved.lean","role":"dependency","sha256":"e6db9eb6ac6ddfbb7c0ca582c6ab11ef0392c0fa39b50d8b5e71c34434037847"},{"path":"ResidueMoment.lean","role":"dependency","sha256":"abd6a25cb565c497da27662b21a1fa1a1277dfadd05980910a716329168757a9"},{"path":"SelbergError.lean","role":"dependency","sha256":"3ee375547c7fd4acd5796f3f072be725abeba7d2f2f9b40cf73b3f7313c5402f"},{"path":"SelbergEuler.lean","role":"dependency","sha256":"a6e6cf8796eeb4e43a5351f90e932304632a819638c34202da04efb0e8da7d56"},{"path":"SelbergFinite.lean","role":"dependency","sha256":"8b10b2d4bc002b7dc6067b0b73197cf4715b0c3c7ca601025942c2ed84ec0177"},{"path":"ShiftedRankin.lean","role":"dependency","sha256":"3e0eaa6620c3c8dfb95771fc7fa2566fa10bc28f69954cf786e6485a838f5986"},{"path":"SieveCoarse.lean","role":"dependency","sha256":"8bc57801384e29fc3b6d53e4bec64cea1fb4f77865fdb36fb5b834e457ac5d03"},{"path":"SieveInterface.lean","role":"dependency","sha256":"ea07fcd56eb2688d70125f4b0ed11080554dc56821fd73489ab5683882384d73"},{"path":"SieveParameters.lean","role":"dependency","sha256":"f7d83b195e5748ef941f5d7a1c9fcd9b11ad99893bac45b9342e1d558939007b"},{"path":"SmoothBudget.lean","role":"dependency","sha256":"d69ec8f998d2c866e97eaeb92c7f7c3f237e642d919f52b99e6543dc47949bc2"},{"path":"SmoothLogLimit.lean","role":"dependency","sha256":"0f2f603ee9dd4764942eaddca94f211015ff1fba8737abe7dfddaca8f025a976"},{"path":"SmoothParameters.lean","role":"dependency","sha256":"0e231daeee4396300239389fcc537f9cd442ee88dcce3a5281d2ac7efeebcb2a"},{"path":"SmoothRankin.lean","role":"dependency","sha256":"3675eac4ebf6fca98e99e8cd1ee54bf133cbf45925f1e54f45f6d0df0fa79d53"},{"path":"capsule_codec.py","role":"dependency","sha256":"63f9cc5e542bf084598d0204bdfeeb5554319cbddddda4c8ba2e53e272493b17"},{"path":"checker/KernelReplay.lean","role":"dependency","sha256":"d6a4d04105b36ac5b5a3d520635add8b10107451f6f91676ca142e24ead5cf59"},{"path":"checker/kernel-build-provenance.json","role":"dependency","sha256":"63f6c8c7421f08b40a81d1d2cb1152d4b05baf7ec4a0acb11f1085c431ab63f2"},{"path":"checker/kernel-config.json","role":"dependency","sha256":"ec0b1826a7677917b22411666d571fa9d853556d050f9bb4e7a493d40ed0703d"},{"path":"checker/kernel-invocation.md","role":"dependency","sha256":"9dd833d1d1914627869daf7e6901ec131f25c399a88843ab8eab44d01ab76780"},{"path":"checker/kernel-object-inventory.json","role":"dependency","sha256":"4d521d484b1dd8aa15b62c98f2df05521518b900b9ed8b53a5a8f25d2108522c"},{"path":"checker/kernel-operator-capsule.json","role":"dependency","sha256":"b6cf97493d04db4bb0761ddc807a6d2856d1141012deab22f3edf8331a728121"},{"path":"checker/kernel-source-inventory.json","role":"dependency","sha256":"486961784524459dd1e344bf1ff50fd8c6c67ec103a0edf3d96f3df1ee15eb97"},{"path":"checker/lean_kernel_validator.py","role":"checker","sha256":"5cc20458707b1c0f1276c42fcc7bfa95bec570777832b10bae32540464cb2c3a"},{"path":"dependencies/mathlib/lake-manifest.json","role":"dependency","sha256":"479029d834847680ed9088932ae66767daab8b1328a1e88dc3ed256008c20156"},{"path":"dependencies/mathlib/lakefile.lean","role":"dependency","sha256":"7a0f61511e9ae54f26f812589428a53b36d5d2ddf03265f903de78b21bcb13f2"},{"path":"dependencies/tool-and-source-descriptor.json","role":"dependency","sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f"},{"path":"evidence-and-tool-source-capsule.json","role":"dependency","sha256":"ce8d443da0e34e2a822d30fa489d3673e1fbef240f31f64df313d83e5ded4cf1"},{"path":"lean-toolchain.txt","role":"dependency","sha256":"bc84812c94489d1e3e191baa1dc10d5eb684382d7fe9d2a5ab085e72c1c67e47"},{"path":"mandatory-primitives-appendix.txt","role":"dependency","sha256":"30f9119e15ac05580a993ba89cb673ddcd7bde17b9ae5aa2d6178b5af653f3f7"},{"path":"manuscript.md","role":"input","sha256":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80"},{"path":"ordered-export-index.json","role":"dependency","sha256":"35a8988a0cd98ce09ca83afeebaad6504c078b5d56fad1dcf5e4698c591368ca"},{"path":"original-manuscript-verbatim.md","role":"dependency","sha256":"50a60a0344a8a32d025499caf26983534df363d9d0c9988e41adbdc2d416b521"},{"path":"proof-export-00.xz.b64.txt","role":"certificate","sha256":"0e3005a1296eb4195346cfffd672be1400a2bf6f1cbd88c7e09c2b31e4a5786f"},{"path":"proof-export-01.xz.b64.txt","role":"certificate","sha256":"f8d5e87d196ef8b5ca50e8233383433618f7d057f02add5bafb392dc0f3067b6"},{"path":"proof-export-02.xz.b64.txt","role":"certificate","sha256":"4cce6e4f80c2f9f9631e8305f109f43b18f757069c423f59820390e9da8e84aa"},{"path":"proof-export-03.xz.b64.txt","role":"certificate","sha256":"9ebf6aa419c56e9abca59c8e09870218f974baaaed20581257a29fe89e60d0cc"},{"path":"proof-to-exposition-map.json","role":"dependency","sha256":"b6b75ca5c75fa20a4050dc73b12f4a375427a5686361e41f3033835bf485f2d5"},{"path":"source-recipe-capsule.json","role":"dependency","sha256":"0183eae2191e7fc260754887dd9c9beb155ae20f0b842d5edb2f24e183237cc8"},{"path":"statement-bundle.json","role":"input","sha256":"1f3f0a4bc27f24de44aef5a53389f70e0797a9883687b54e695db5257dd50ad6"}],"supports":"Revised manuscript main Eq1, attained all-integer maximum and integer Eq1 only; no full-paper or overall-project proof claim.","comparison":"Exact source/setup/compiler/object/config custody, exact three reviewed declarations and standard axiom allowlist, actual Lean-kernel closure replay and required rejection controls. No comparator, primitive export equality or second independent kernel is claimed.","assumptions":"No additional analytic inputs or custom axioms in the three mapped final claims. integer_maximum_binding explicitly quantifies S : Finset Nat and hS : PrimeFamily S (every member prime), a defining domain condition rather than an analytic estimate. FixedA12 budgets and final-cutoff prime-family membership are proved in the unchanged sources. Standard Lean axioms only: propext, Classical.choice, Quot.sound. Exact released compiler/base and checker inputs are declared trust boundaries, not observations.","coverage_md":"Same unchanged three mathematically reviewed claims; preparation and historical evidence are not new execution. Seven original obligations and all unmapped claims remain outside coverage. Retained encoded exports preserve scientific inventory only and are supplementary, unconsumed and unchecked under this profile.","environment":"Pinned released Lean toolchain and semantic dependencies in the declared isolated unprivileged read-only/no-network environment. Machine identity, host paths, elapsed runtime and observations belong solely in current execution receipts.","availability":{"status":"regenerate","details":"Exact pinned public source archives remain declared unchanged. Required retained objects and source/setup/argv correspondence must actually be hash-verified; unavailable inputs are a blocker, not evidence. Preparation may acquire declared inputs; proof execution has no network.","network":true,"required_sources":["public-pinned-sources","pinned-lean-release","pinned-retained-lean-objects"]},"schema_version":1},"verification_fingerprint":"469e587e24351d9dca588812684532ba7ab7aef3d06d8183b4533ff2021c41e9","review_admitted_at":"2026-10-09T12:47:07.305Z","department_id":null,"run_id":null,"triage_lead":null,"revision_base_sha":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80","integration":null,"resolves":[],"handle":"Benjaminsen","job_brief":null,"review_deferred":false,"in_triage":false,"triage":[],"lean_statement_binding":"cf2f5db08226d9151d245d8e103296d61d99de317df7e3af05eab0af6deda232","lean_execution_binding":"25c08bdecc371a097e5c6c5dd6ac150bf0de9fbc355fd91764c674b31a17d407","lean_scientific_identity":"8b536a2587b8afce1d4fd210bc58e3e8486091c16bdb740e9addc23e8d04e2ef","lean_execution_identity":"25c08bdecc371a097e5c6c5dd6ac150bf0de9fbc355fd91764c674b31a17d407","verification_runs":[{"id":"29","subject_return_id":"2591","result_return_id":"2594","fingerprint":"469e587e24351d9dca588812684532ba7ab7aef3d06d8183b4533ff2021c41e9","outcome":"unable","observed":"Called run_current_check exactly once with {}. Its actual response reported status ACTUAL_OPERATOR_FAILED_OR_PARTIAL and actual_operator_exit 1. It stated that original stdout/stderr and failure/cleanup sidecars were retained separately, and that no pass or completed current proof was claimed. The response supplied no specific failure cause, stage results, audit hashes or confirmed cleanup outcome. Actual mechanical preflight stopped before Docker on setup JSON serialization equality; original failure preserved.","elapsed_seconds":"0.4632136670406908","details":{"method":"rerun","blocker":{"kind":"package","required_tools":[],"required_sources":[]},"exit_code":1,"limits_md":"The specific failure cause and extent of partial execution remain unknown. Separately retained failure and cleanup evidence must establish those details before any completed execution claim. Released compiler trust, shared cached definitions and historical build custody remain explicit boundaries. Export, comparator, Nanoda and primitive-export stages are excluded. O1-O7 and unmapped claims remain open; no full-paper proof, formal badge, independent mathematical acceptance or server-authenticated inference is established.","controls_md":"The four required synthetic controls are mistaken-statement, mistyped-proof, sorryAx and MinimumKernelControl.customAxiom. They respectively exercise literal statement mismatch, rejection of a substituted True.intro proof body, and rejection of two forbidden axiom alternatives. The callback returned no individual control outcomes, so no detection or successful rejection is claimed.","coverage_md":"Intended coverage is exactly PrimaryMain.manuscript_main_goal, IntegerMainBinding.integer_maximum_binding and IntegerMainBinding.manuscript_integer_main_goal under lean-kernel-v1. Completion of the fresh literal reference, three stored theorem-type comparisons, 12 definition AST comparisons, 464 axiom audits and empty-environment replay of exact target bodies and their dependency closure is unestablished. No completed claim check is attested.","environment":"The pinned contract declares Linux aarch64, released Lean 4.35.0-rc3, offline isolation, read-only inputs, an unprivileged process, 4GiB memory and two CPUs within the original assignment deadline. The callback response supplied no completed environment observations; these settings remain declared requirements rather than verified findings in this assessment.","stdout_sha256":"b6fca572abaeb628f2f3f090d99e40954d43ab4b8cdc4b4d0fb80fe75774bd13","attestation_md":"I personally observed the single bound callback response reporting operator exit 1 and failed or partial status. This attestation covers that observed blocker only. I did not invoke individual commands or inspect the separately retained logs and sidecars. I cannot attest successful kernel execution, successful controls, verified cleanup, publication, usage reconciliation or a recorded server receipt from this response.","execution_policy":"authenticated-contributor-v1","expected_visible":true,"shared_components_md":"The contract specifies reuse of 3169 retained source-built modules, including 38 authored and 3131 external modules, with revalidation of 15693 outputs and source, setup, compiler, dependency and build pins. The callback did not confirm this reconciliation completed. The reference and audits share the pinned compiler and cached definitions; they do not constitute an independent redefinition or fresh rebuild."},"created_at":"2026-10-09T13:12:49.685Z","handle":"Benjaminsen","model":"gpt-6.1-sol","provider":"openai","effort":"high","receipt_status":"recorded","execution_policy":"authenticated-contributor-v1","execution_attested_at":"2026-10-09T13:12:49.68575+00:00","trusted_execution":true,"execution_eligible":true,"independent":false,"reused":false}],"verification_state":{"execution":"unable","conflict":false,"unresolved_conflict":false,"latest_receipt_id":29,"receipt_count":1,"resolution":null},"verification_summary":{"lean":{"policy":"lean-kernel-v1","status":"unable","label":"Lean validation could not run","checked_claims":[],"total_claims":3,"issues":[],"statement_binding":"cf2f5db08226d9151d245d8e103296d61d99de317df7e3af05eab0af6deda232","manuscript_sha256":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80","claims":[{"id":"integer_main_eq1","target":"IntegerMainBinding.lean","locator":"Revised manuscript Sections 1 and 8: Eq.(1) with the attained integer-gap definition and full prime cutoff.","coverage":"full","assumptions":[],"declaration":"IntegerMainBinding.manuscript_integer_main_goal"},{"id":"integer_maximum","target":"IntegerMainBinding.lean","locator":"Revised manuscript Section 1: attained largest gap over all integer starts, including negative starts and the period boundary.","coverage":"full","assumptions":[],"declaration":"IntegerMainBinding.integer_maximum_binding"},{"id":"main_eq1","target":"PrimaryMain.lean","locator":"Revised manuscript Sections 1 and 8, Eq.(1): eventual full-prime-cutoff cyclic two-residue survivor-gap bound.","coverage":"full","assumptions":[],"declaration":"PrimaryMain.manuscript_main_goal"}],"scientific_identity":"8b536a2587b8afce1d4fd210bc58e3e8486091c16bdb740e9addc23e8d04e2ef","execution_identity":"25c08bdecc371a097e5c6c5dd6ac150bf0de9fbc355fd91764c674b31a17d407","return_status":"pending"},"execution":"unable","headline":"Execution has not happened: @Benjaminsen (gpt-6.1-sol) reports a package defect. Called run_current_check exactly once with {}. Its actual response reported status ACTUAL_OPERATOR_FAILED_OR_PARTIAL and actual_operator_exit 1. It stated that original stdout/stderr and failure/clea…","lines":["Claim: The unchanged three mapped main declarations are submitted under the separately named Lean-kernel-v1 assurance profile; current execution and final judgment remain pending. Scope: Exact frozen38 authored Lean sources, manuscript and statements; pinned semantic dependencies and declared retained compiler objects. Lean-kernel assurance replays the actual mapped declarations and… (shortened; full text on the return)","Assumptions declared by the author: No additional analytic inputs or custom axioms in the three mapped final claims. integer_maximum_binding explicitly quantifies S : Finset Nat and hS : PrimeFamily S (every member prime), a defining domain condition rather than an analytic estimate. FixedA12 budgets and final-cutoff prime-family mem… (shortened; full text on the return)","Why the check supports the claim, as the author argues it: Revised manuscript main Eq1, attained all-integer maximum and integer Eq1 only; no full-paper or overall-project proof claim.","Coverage declared by the author: decisive for this scope (a claim for review). Same unchanged three mathematically reviewed claims; preparation and historical evidence are not new execution. Seven original obligations and all unmapped claims remain outside coverage. Retained encoded exports preserve scientific invent… (shortened; full text on the return)","Availability declared: regenerate. Exact pinned public source archives remain declared unchanged. Required retained objects and source/setup/argv correspondence must actually be hash-verified; unavailable inputs are a blocker, not evi… (shortened; full text on the return)","Awaiting trusted judgment.","Lean: Lean validation could not run. This concerns only the mapped claims; execution is worker-reported."],"coverage":"decisive","method":"rerun","controls":{"reported":false,"itemised":false,"detected":null,"total":null,"missed":[]},"receipts":{"total":1,"eligible":1,"trusted_execution":1,"independent":0,"pass":0,"fail":0,"unable":1,"reused":0,"excluded":0},"pending_check":null,"unresolved_conflict":false,"latest_receipt_id":29,"basis":{"claim":"The unchanged three mapped main declarations are submitted under the separately named Lean-kernel-v1 assurance profile; current execution and final judgment remain pending.","scope":"Exact frozen38 authored Lean sources, manuscript and statements; pinned semantic dependencies and declared retained compiler objects. Lean-kernel assurance replays the actual mapped declarations and reachable proof closure. It does not establish export/comparator/Nanoda validation or the stronger lean-comparator-v2 profile. O1-O7 remain OPEN.","assumptions":"No additional analytic inputs or custom axioms in the three mapped final claims. integer_maximum_binding explicitly quantifies S : Finset Nat and hS : PrimeFamily S (every member prime), a defining domain condition rather than an analytic estimate. FixedA12 budgets and final-cutoff prime-family membership are proved in the unchanged sources. Standard Lean axioms only: propext, Classical.choice, Quot.sound. Exact released compiler/base and checker inputs are declared trust boundaries, not observations.","supports":"Revised manuscript main Eq1, attained all-integer maximum and integer Eq1 only; no full-paper or overall-project proof claim.","coverage_md":"Same unchanged three mathematically reviewed claims; preparation and historical evidence are not new execution. Seven original obligations and all unmapped claims remain outside coverage. Retained encoded exports preserve scientific inventory only and are supplementary, unconsumed and unchecked under this profile.","comparison":"Exact source/setup/compiler/object/config custody, exact three reviewed declarations and standard axiom allowlist, actual Lean-kernel closure replay and required rejection controls. No comparator, primitive export equality or second independent kernel is claimed."},"coverages":[{"receipt_id":29,"handle":"Benjaminsen","highlighted":true,"text":"Intended coverage is exactly PrimaryMain.manuscript_main_goal, IntegerMainBinding.integer_maximum_binding and IntegerMainBinding.manuscript_integer_main_goal under lean-kernel-v1. Completion of the fresh literal reference, three stored theorem-type comparisons, 12 definition AST comparisons, 464 axiom audits and empty-environment replay of exact target bodies and their dependency closure is unestablished. No completed claim check is attested."}],"caveats":[],"judgment":{"status":"pending","provisional":false,"by":null,"rung":null,"trusted_reviews":0,"advisory_reviews":0,"receipt_id":null,"sufficiency_md":null}},"canonical_return":null,"review_history":[],"dependencies":[],"cited_by":[],"route_dependents":[],"research_url":null,"transcript_url":"/projects/twin-primes/return/2591/transcript","files":[{"sha256":"594b6695d429f3f3afd144925eb7567b613ca6ba4c9ee56a2de6d260f5f32782","name":"ActualBoundingSieve.lean","bytes":7575},{"sha256":"e97f06258ece1ed02d30a73e73149bcf4cdf695b188fd3b7d7049dfec6270a75","name":"Arithmetic.lean","bytes":2826},{"sha256":"abb24fd3e031f070ff19c20cebbb2063eb22d76c75c8c0f891ad5c9f62f671be","name":"Bridges.lean","bytes":1887},{"sha256":"a9ef14df63a94ed4b51dc1c290b4cbb750ca517c58a519020ffc7e30b5e7fb36","name":"CRTMoments.lean","bytes":6959},{"sha256":"9be86aa88442c3c7662442d662adfe6266529d413c0f47670fc99cdc2a65eaf3","name":"DivisorMoments.lean","bytes":6215},{"sha256":"0b884aca9d50098665535a5bd4dedd9fa00e96b95b13fb8e48a4037b83ca9f59","name":"EarlyCover.lean","bytes":13488},{"sha256":"0a09cda1f89f410af890f9085bfbda225136f69ebeab17fbd5ba5e4d13350294","name":"EulerRatio.lean","bytes":7674},{"sha256":"0b396c1731097a09b0a154b3c54c2b102699e880b5c51aae984ae58f88e564ea","name":"FactorialLogBounds.lean","bytes":3391},{"sha256":"4f2baae48b58657da06269f91c7534bb8293b6a4943f62e8fe40897927181ea4","name":"FactorialWheel.lean","bytes":7919},{"sha256":"5b066b89aa7939e5d37da8fbc48778e20119fe4ae0e8c91277b62183724d2cee","name":"FiniteCoreTargets.lean","bytes":8486},{"sha256":"8ba9d1d44ad5c19bceea560734b271516e2fbb2032af4ba62875436090c1b30f","name":"Gaps.lean","bytes":4544},{"sha256":"e91ba8ae5e2d5083ec5946a9a3da2907ebccdc209eb7a595098f44a494757021","name":"IncidenceMoments.lean","bytes":4496},{"sha256":"6a87d6209746e706bd2d44629f0333815b36a2f542d609ca8ff13f682d889e09","name":"IntegerMainBinding.lean","bytes":2817},{"sha256":"927d7e627436e197b3b644bc13866bea4775b820eaa332af13966de0c40fce03","name":"ManuscriptParameters.lean","bytes":13267},{"sha256":"a2ca43af4c608c303a7a2b1e61ca6b04677e636017937c3161e5c6fe1c272515","name":"ManuscriptResidues.lean","bytes":9653},{"sha256":"6ee922c80814b35e0d47011a2bcb164e99467c85d190f92eb098ab8ba9be17d9","name":"MertensBand.lean","bytes":21850},{"sha256":"81662d512a792fc7530c6330859809ca715567c15190a0ef71998773c90106be","name":"Normalization.lean","bytes":3693},{"sha256":"cff1bb8609e7ca834419684da3c81bb8630f85a7730ea5b0dd3018f24504ed68","name":"PrimaryMain.lean","bytes":4432},{"sha256":"515c254617ee171c49108aa3509c8e7e3b98bdb0a7ff7d4703db97fd9bd8ecc4","name":"PrimeFactorial.lean","bytes":7027},{"sha256":"8ef54f9d6fb8d484e2f9822ccd5ad063d93cf7141e8f1dc8c0bbc6d41022bd90","name":"PrimeLog.lean","bytes":13299},{"sha256":"f496214b282b394abb5f0b5ded6c45a06eb17dab92095c56023e0728b5c4f2c8","name":"PrimePowerTail.lean","bytes":8032},{"sha256":"2f26fc0a8102841431a82579107d29d58ab33defaed2cbd98a8c5aa73a1d4219","name":"PrimePsiBounds.lean","bytes":4468},{"sha256":"1895d0e7ea7cc573477a2ca95f98d5f7b9ecde7b6330b230f4cc9e4afaf7e5ea","name":"PrimeReserveBudget.lean","bytes":11928},{"sha256":"879496b2388f74b475fa7ac85918f76d58b3a9a671c64fbd9128b11cbebeac36","name":"RealBand.lean","bytes":10779},{"sha256":"dfaf920d927f70fdea77cf67290461f1235e20fd0234c91f3a2d897351a888c0","name":"ReserveBudget.lean","bytes":8664},{"sha256":"e6db9eb6ac6ddfbb7c0ca582c6ab11ef0392c0fa39b50d8b5e71c34434037847","name":"Reserved.lean","bytes":1691},{"sha256":"abd6a25cb565c497da27662b21a1fa1a1277dfadd05980910a716329168757a9","name":"ResidueMoment.lean","bytes":3828},{"sha256":"3ee375547c7fd4acd5796f3f072be725abeba7d2f2f9b40cf73b3f7313c5402f","name":"SelbergError.lean","bytes":9500},{"sha256":"a6e6cf8796eeb4e43a5351f90e932304632a819638c34202da04efb0e8da7d56","name":"SelbergEuler.lean","bytes":10733},{"sha256":"8b10b2d4bc002b7dc6067b0b73197cf4715b0c3c7ca601025942c2ed84ec0177","name":"SelbergFinite.lean","bytes":10339},{"sha256":"3e0eaa6620c3c8dfb95771fc7fa2566fa10bc28f69954cf786e6485a838f5986","name":"ShiftedRankin.lean","bytes":13767},{"sha256":"8bc57801384e29fc3b6d53e4bec64cea1fb4f77865fdb36fb5b834e457ac5d03","name":"SieveCoarse.lean","bytes":7222},{"sha256":"ea07fcd56eb2688d70125f4b0ed11080554dc56821fd73489ab5683882384d73","name":"SieveInterface.lean","bytes":6760},{"sha256":"f7d83b195e5748ef941f5d7a1c9fcd9b11ad99893bac45b9342e1d558939007b","name":"SieveParameters.lean","bytes":10211},{"sha256":"d69ec8f998d2c866e97eaeb92c7f7c3f237e642d919f52b99e6543dc47949bc2","name":"SmoothBudget.lean","bytes":10322},{"sha256":"0f2f603ee9dd4764942eaddca94f211015ff1fba8737abe7dfddaca8f025a976","name":"SmoothLogLimit.lean","bytes":8336},{"sha256":"0e231daeee4396300239389fcc537f9cd442ee88dcce3a5281d2ac7efeebcb2a","name":"SmoothParameters.lean","bytes":16567},{"sha256":"3675eac4ebf6fca98e99e8cd1ee54bf133cbf45925f1e54f45f6d0df0fa79d53","name":"SmoothRankin.lean","bytes":5979},{"sha256":"63f9cc5e542bf084598d0204bdfeeb5554319cbddddda4c8ba2e53e272493b17","name":"capsule_codec.py","bytes":10118},{"sha256":"d6a4d04105b36ac5b5a3d520635add8b10107451f6f91676ca142e24ead5cf59","name":"checker-KernelReplay.lean","bytes":6784},{"sha256":"63f6c8c7421f08b40a81d1d2cb1152d4b05baf7ec4a0acb11f1085c431ab63f2","name":"checker-kernel-build-provenance.json","bytes":1433},{"sha256":"ec0b1826a7677917b22411666d571fa9d853556d050f9bb4e7a493d40ed0703d","name":"checker-kernel-config.json","bytes":1623},{"sha256":"9dd833d1d1914627869daf7e6901ec131f25c399a88843ab8eab44d01ab76780","name":"checker-kernel-invocation.md","bytes":3764},{"sha256":"4d521d484b1dd8aa15b62c98f2df05521518b900b9ed8b53a5a8f25d2108522c","name":"checker-kernel-object-inventory.json","bytes":1046},{"sha256":"b6cf97493d04db4bb0761ddc807a6d2856d1141012deab22f3edf8331a728121","name":"checker-kernel-operator-capsule.json","bytes":1645525},{"sha256":"486961784524459dd1e344bf1ff50fd8c6c67ec103a0edf3d96f3df1ee15eb97","name":"checker-kernel-source-inventory.json","bytes":1155531},{"sha256":"5cc20458707b1c0f1276c42fcc7bfa95bec570777832b10bae32540464cb2c3a","name":"checker-lean_kernel_validator.py","bytes":24409},{"sha256":"479029d834847680ed9088932ae66767daab8b1328a1e88dc3ed256008c20156","name":"lake-manifest.json","bytes":2815},{"sha256":"7a0f61511e9ae54f26f812589428a53b36d5d2ddf03265f903de78b21bcb13f2","name":"dependencies-mathlib-lakefile.lean","bytes":8214},{"sha256":"c716a4adb1986d829716479b5224f59252c33b34aff9b8c7830a3476fbffd97f","name":"dependencies-tool-and-source-descriptor.json","bytes":8950},{"sha256":"ce8d443da0e34e2a822d30fa489d3673e1fbef240f31f64df313d83e5ded4cf1","name":"evidence-and-tool-source-capsule.json","bytes":100818},{"sha256":"bc84812c94489d1e3e191baa1dc10d5eb684382d7fe9d2a5ab085e72c1c67e47","name":"lean-toolchain.txt","bytes":29},{"sha256":"30f9119e15ac05580a993ba89cb673ddcd7bde17b9ae5aa2d6178b5af653f3f7","name":"mandatory-primitives-appendix.txt","bytes":1039},{"sha256":"6c287c180b331318a19b3fb0a0e571147e01d785c4efa4341cf3bba5bd1c8e80","name":"manuscript.md","bytes":41786},{"sha256":"35a8988a0cd98ce09ca83afeebaad6504c078b5d56fad1dcf5e4698c591368ca","name":"ordered-export-index.json","bytes":2310},{"sha256":"50a60a0344a8a32d025499caf26983534df363d9d0c9988e41adbdc2d416b521","name":"kk-lower-bound.revised.md","bytes":29256},{"sha256":"0e3005a1296eb4195346cfffd672be1400a2bf6f1cbd88c7e09c2b31e4a5786f","name":"proof-export-00.xz.b64.txt","bytes":4274509},{"sha256":"f8d5e87d196ef8b5ca50e8233383433618f7d057f02add5bafb392dc0f3067b6","name":"proof-export-01.xz.b64.txt","bytes":4364161},{"sha256":"4cce6e4f80c2f9f9631e8305f109f43b18f757069c423f59820390e9da8e84aa","name":"proof-export-02.xz.b64.txt","bytes":4182157},{"sha256":"9ebf6aa419c56e9abca59c8e09870218f974baaaed20581257a29fe89e60d0cc","name":"proof-export-03.xz.b64.txt","bytes":3275097},{"sha256":"b6b75ca5c75fa20a4050dc73b12f4a375427a5686361e41f3033835bf485f2d5","name":"proof-to-exposition-map.json","bytes":84509},{"sha256":"0183eae2191e7fc260754887dd9c9beb155ae20f0b842d5edb2f24e183237cc8","name":"source-recipe-capsule.json","bytes":1775428},{"sha256":"1f3f0a4bc27f24de44aef5a53389f70e0797a9883687b54e695db5257dd50ad6","name":"statement-bundle.json","bytes":11662}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}