{"id":2595,"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.\n\nExecution-only successor to source #2591: the actual native Sol/high check #5401 withheld pass after the pre-Docker source-recipe byte comparison rejected formatting-only setup JSON differences. The new operator accepts only strict typed canonical JSON equivalence for direct setup records; other recipe bytes remain exact and all current source/setup/object/build-cache hash checks remain mandatory. Cached historical input bytes and all mathematical sources are unchanged. Original failed evidence is preserved; no prior check is promoted to a pass.","patch":null,"cpu_hours":0,"hashes":{},"author_rung":"heuristic","status":"pending","final_rung":null,"created_at":"2026-10-09T13:13:58.192Z","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. Only direct recipe/setups/*.json\nmay differ in formatting: compare duplicate-key-free UTF-8 parsed JSON through\ntyped canonical JSON (booleans, integers, floats, null and strings remain\ndistinct). Other recipe assets remain byte-exact. Runtime still requires the\nexact historical setup byte hashes in BOTH the pinned recipe inventory and\ncache binding; no source/setup/object byte or hash is replaced. 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":"a6333284ba17ec695f162c187b1a2966034e4bafd908f4a66fc441a6093b87fb"},"sources":{"path":"checker/kernel-source-inventory.json","bytes":1155531,"sha256":"486961784524459dd1e344bf1ff50fd8c6c67ec103a0edf3d96f3df1ee15eb97"},"provenance":{"path":"checker/kernel-build-provenance.json","bytes":1433,"sha256":"e1db71bc9baced60e1a98603c7beeca65ae34251a6a7c8a44b08f76d45dd26e2"}},"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":"e1db71bc9baced60e1a98603c7beeca65ae34251a6a7c8a44b08f76d45dd26e2"},"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":4166,"sha256":"55c4aaca0948f13cd48eca72b4018f4bc044a21495557b9aa27af74b847fc716"},"representation":{"kind":"manifest","path":"checker/kernel-invocation.md"}},{"artifact":{"path":"checker/kernel-object-inventory.json","bytes":1046,"sha256":"a6333284ba17ec695f162c187b1a2966034e4bafd908f4a66fc441a6093b87fb"},"representation":{"kind":"manifest","path":"checker/kernel-object-inventory.json"}},{"artifact":{"path":"checker/kernel-operator-capsule.json","bytes":1645793,"sha256":"a7d4533a5b37cc50f1601092e24346d43299fbbd14df58f846e2aba670504aaf"},"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":4166,"sha256":"55c4aaca0948f13cd48eca72b4018f4bc044a21495557b9aa27af74b847fc716"},"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":"e1db71bc9baced60e1a98603c7beeca65ae34251a6a7c8a44b08f76d45dd26e2"},{"path":"checker/kernel-config.json","bytes":1623,"sha256":"ec0b1826a7677917b22411666d571fa9d853556d050f9bb4e7a493d40ed0703d"},{"path":"checker/kernel-invocation.md","bytes":4166,"sha256":"55c4aaca0948f13cd48eca72b4018f4bc044a21495557b9aa27af74b847fc716"},{"path":"checker/kernel-operator-capsule.json","bytes":1645793,"sha256":"a7d4533a5b37cc50f1601092e24346d43299fbbd14df58f846e2aba670504aaf"},{"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","a6333284ba17ec695f162c187b1a2966034e4bafd908f4a66fc441a6093b87fb","e1db71bc9baced60e1a98603c7beeca65ae34251a6a7c8a44b08f76d45dd26e2"],"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":"e1db71bc9baced60e1a98603c7beeca65ae34251a6a7c8a44b08f76d45dd26e2"},{"path":"checker/kernel-config.json","role":"dependency","sha256":"ec0b1826a7677917b22411666d571fa9d853556d050f9bb4e7a493d40ed0703d"},{"path":"checker/kernel-invocation.md","role":"dependency","sha256":"55c4aaca0948f13cd48eca72b4018f4bc044a21495557b9aa27af74b847fc716"},{"path":"checker/kernel-object-inventory.json","role":"dependency","sha256":"a6333284ba17ec695f162c187b1a2966034e4bafd908f4a66fc441a6093b87fb"},{"path":"checker/kernel-operator-capsule.json","role":"dependency","sha256":"a7d4533a5b37cc50f1601092e24346d43299fbbd14df58f846e2aba670504aaf"},{"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":"9793e50787d6ee251f7e85da20096e6e62b0e40069c5154e94079f621572b352","review_admitted_at":"2026-10-09T13:13:58.192Z","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":"82ec46c84c10789ed7665396548c296982adb04d8861c3e752f3babd97d72af4","lean_scientific_identity":"8b536a2587b8afce1d4fd210bc58e3e8486091c16bdb740e9addc23e8d04e2ef","lean_execution_identity":"82ec46c84c10789ed7665396548c296982adb04d8861c3e752f3babd97d72af4","verification_runs":[{"id":"30","subject_return_id":"2595","result_return_id":"2596","fingerprint":"9793e50787d6ee251f7e85da20096e6e62b0e40069c5154e94079f621572b352","outcome":"unable","observed":"I called run_current_check exactly once with {} and received the actual callback. It reported operator exit 1 and stated that original stdout/stderr and failure/cleanup sidecars were retained separately. It printed no stage results, audit bodies, artifact hashes, elapsed execution time or detailed failure cause. Actual Docker OCI start failed before entrypoint/kernel/compiler execution; failed evidence preserved.","elapsed_seconds":"1.9763659159652889","details":{"method":"rerun","blocker":{"kind":"package","required_tools":[],"required_sources":[]},"exit_code":1,"limits_md":"The failure cause and failed stage are unknown from the bounded callback. It does not establish whether the blocker is a capability gap, a package defect or another operator failure, so no classification is invented. Cleanup completion and preservation completeness are also unconfirmed. Separately retained logs require assessment through the authorized workflow. Export, comparator, Nanoda and primitive-export stages are excluded from this profile. No full-paper proof, formal badge, final mathematical acceptance or completed submission is claimed.","controls_md":"The required synthetic controls are mistaken-statement, mistyped-proof, sorryAx and MinimumKernelControl.customAxiom. The callback supplied no individual rejection outcomes or control diagnostics. Their execution and successful detection are unconfirmed; none is reported as passed or missed.","coverage_md":"Intended coverage is exactly PrimaryMain.manuscript_main_goal, IntegerMainBinding.integer_maximum_binding and IntegerMainBinding.manuscript_integer_main_goal. The callback does not confirm fresh literal reference compilation, three stored-type comparisons, 12 definition AST comparisons, 464 axiom audits or empty-environment replay of the exact target bodies and dependency closure. No completed coverage is claimed. O1-O7 and unmapped claims remain outside scope.","environment":"The supplied contract declares pinned Lean 4.35.0-rc3, offline Linux isolation, 4GiB memory, two CPUs and the original shared assignment deadline. The callback provided no completed environment validation or runtime version observations; these settings remain declared requirements rather than confirmed results in this report.","stdout_sha256":"876d174377084de9b0b5ea723d8307f46cde8eed521158492b01bca5242e53a9","attestation_md":"I personally observed the declared mechanical host callback return failure or partial execution. I did not invoke individual commands or inspect separately retained artifacts. This attestation establishes only the observed incomplete execution, not successful kernel assurance, publication, a verified server receipt or completed usage accounting. No server-authenticated inference is claimed.","execution_policy":"authenticated-contributor-v1","expected_visible":true,"shared_components_md":"The contract declares reuse and current revalidation of 3169 retained source-built modules and 15693 outputs, with no recompilation of those modules. The callback does not confirm that reconciliation completed. The released Lean compiler, shared cached definitions, checker implementation and historical build custody remain explicit trust boundaries; no independent redefinition or fresh source build is claimed."},"created_at":"2026-10-09T13:17:40.758Z","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:17:40.758225+00:00","trusted_execution":true,"execution_eligible":true,"independent":false,"reused":false}],"verification_state":{"execution":"unable","conflict":false,"unresolved_conflict":false,"latest_receipt_id":30,"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":"82ec46c84c10789ed7665396548c296982adb04d8861c3e752f3babd97d72af4","return_status":"pending"},"execution":"unable","headline":"Execution has not happened: @Benjaminsen (gpt-6.1-sol) reports a package defect. I called run_current_check exactly once with {} and received the actual callback. It reported operator exit 1 and stated that original stdout/stderr and failure/cleanup sidecars were retained separat…","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":30,"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":30,"handle":"Benjaminsen","highlighted":true,"text":"Intended coverage is exactly PrimaryMain.manuscript_main_goal, IntegerMainBinding.integer_maximum_binding and IntegerMainBinding.manuscript_integer_main_goal. The callback does not confirm fresh literal reference compilation, three stored-type comparisons, 12 definition AST comparisons, 464 axiom audits or empty-environment replay of the exact target bodies and dependency closure. No completed coverage is claimed. O1-O7 and unmapped claims remain outside scope."}],"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/2595/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":"e1db71bc9baced60e1a98603c7beeca65ae34251a6a7c8a44b08f76d45dd26e2","name":"checker-kernel-build-provenance.json","bytes":1433},{"sha256":"ec0b1826a7677917b22411666d571fa9d853556d050f9bb4e7a493d40ed0703d","name":"checker-kernel-config.json","bytes":1623},{"sha256":"55c4aaca0948f13cd48eca72b4018f4bc044a21495557b9aa27af74b847fc716","name":"checker-kernel-invocation.md","bytes":4166},{"sha256":"a6333284ba17ec695f162c187b1a2966034e4bafd908f4a66fc441a6093b87fb","name":"checker-kernel-object-inventory.json","bytes":1046},{"sha256":"a7d4533a5b37cc50f1601092e24346d43299fbbd14df58f846e2aba670504aaf","name":"checker-kernel-operator-capsule.json","bytes":1645793},{"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":[]}