5458360578283d9c9afab1d0a88ac2a94ef9bf757f9f0012d4e1b715a875dcc2  Makefile
9c21ecd15d0081254396f1d3ec195e4047cdab7cb4f14002f7020d524e29847c  README.md
9d1cfa519d5873017590badb7c7306436cd8300ab6f685ab832fc1db555f0004  RIGHTS.md
bef968de9d6862112cbee3e8b0c0eb30ae275ac781c36f9c0c49048ae9dd363c  companion/code/audit_reference.py
c4b341f2fd59e7f627d693533f23e7518c8b082d580122ffabc9c920ce786afb  companion/code/dense278.py
b1a3729f10ef82acba303b1bd62447907ee4094dcce8f2220e6bdc83845ec6e5  companion/code/distinct278.py
7c682dfc946cd395d5e45a63b967e033653a33be241e626a0d4b2d781506c8a8  companion/code/exact278.py
e3f9e44f9fa85eeea0e4bdfd3bfaed9eaae42dabdc8b0cbf38316107f2a1268e  companion/code/graph278.py
1daaa910bd3913b5e600103da84763893a2f1037a93377135d8ca4cfb97091f4  companion/code/prime_pool.py
4bccc615d1aac2d8a15948907ee285850f186c8ce08e7c3c7f820eef85c57d93  companion/code/rational_lp.py
86e22bbfa852bc9f9484eeb467bf0cdad6a8079be4f4ec7be2a6841d810549ff  companion/code/star278.py
38fee64dc950455466fc313da161dc00bdf8b66a64a45996d7a5e00900341d85  companion/code/verify_certificates.py
3bc84d8f7596388138e209cbab11eeb682ab51eaddfa92ff6c69f2591d9e6115  companion/results/clean_build_record.json
a17bcac04dbfbe5c0e3ea4164bf41a959e9e8f6bb663a4d143c90abd1ab9360b  companion/results/clean_lean_build.log
69e210d5902092ded0794d017427fdf90cdfae669ab9cf160320b9f83b8d4c90  companion/results/clean_lean_replay.log
4eb408d5e7bedbb09e70f6c5e467f5d3422da2ca633cd617e74a981a331a7bd7  companion/results/clean_lean_scope_audit.log
5918d4c26f7d58580f9775a0a48eb92806e23013f4763f8a94518064d5f4ec23  companion/results/companion_hardening_record.json
8ab9e9d721f110ec642affbb4ccae443854909272c4630a147d6a6daf2e1423d  companion/results/concise_title_record.json
eed70922e12704d3a99507c5c4246cc1a08af97325289672f212b38d33e20f1d  companion/results/doi_update_record.json
49cb0d1a560e50e2a9f9e48732a0cf7ced24a4dc7ac167bdb9bebb89319d66ed  companion/results/editorial_alignment_record.json
81502dc80460e0e702e2e953788a8229c4a64b25afb32fd41ee9598c04c719fb  companion/results/exposition_examples.json
0e435d25c65fd959647b8df5889caf7d808c5f54c072fe75690bd490bfc2f139  companion/results/exposition_record.json
c0951c203dac73a225909596f9344608a5cdade994bf753b18a8f75a28a5c3a3  companion/results/final_clean_graph_tests.log
f888c2b03e08f5071b8ea6fc16de671c15936a94841bd8c517daa9e9363a3600  companion/results/final_clean_reference_tests.log
d1c307304eca549313595e4a278b39225d84f1d64c8a9cf06486ca42b61f003d  companion/results/final_clean_revision_tests.log
c796d4b5f3f697cb0e60c107d3ce609869480c3b6d271be89764551677834f1b  companion/results/final_clean_upgrade_tests.log
8ab4a7a53ed291c42be79797308317e7627a282f2824201ee3d45a69f386eeb7  companion/results/final_graph_tests.json
7055ea11dacfa28839fc7bdf6e69ab4e6254f2970bd0707b32d2c7e910e999be  companion/results/final_graph_tests.log
6bec260a3edf0fc6815d7db7f2337416a555122b881b52b885f35431b3b024de  companion/results/final_lean_build.log
4eb408d5e7bedbb09e70f6c5e467f5d3422da2ca633cd617e74a981a331a7bd7  companion/results/final_lean_publication.log
69e210d5902092ded0794d017427fdf90cdfae669ab9cf160320b9f83b8d4c90  companion/results/final_lean_replay.log
51b1bdf52a106401f34de603e7f6e6f60762756215e1cd6fb328202b60270bcb  companion/results/final_reference_tests.json
da907f19016ed08dd028c13da5b1198f4c9680df64fe8a26e94e635082613808  companion/results/final_reference_tests.log
8cf1c41d9ba38afcc17311bdc5afabf422ef7f662f483b1656b61b4d42ff2b1c  companion/results/final_revision_tests.json
8cf1c41d9ba38afcc17311bdc5afabf422ef7f662f483b1656b61b4d42ff2b1c  companion/results/final_revision_tests.log
aaf287455a2bb30db1be0c0e353ff79df2d4985e1cfcb564e9962582c828fc55  companion/results/final_upgrade_tests.json
eba78f87198928dc320bc70e0cf918ab1c7b904308e2ea0f27f0271d8cc8b7c5  companion/results/final_upgrade_tests.log
f85343d82463c352b7d57d3c309e8eb9e5c67c954142dd33c72194b2dbebe2ec  companion/results/final_v1_record.json
4eb408d5e7bedbb09e70f6c5e467f5d3422da2ca633cd617e74a981a331a7bd7  companion/results/focused_lean_scope_audit.log
4c4b57489027c5d605fc1b86ed5c653d6420c27a24bb90af603a95610a405a38  companion/results/focused_revision_record.json
325a7fcae82aa1a1137b5e6376c7b0a0b99599559a2a6205dccaead9fb6e3562  companion/results/frontier_certificates.json
a064701423d07c26e903c420a17049af5c07185a01733e5a8ffe7f45cae62ce3  companion/results/graph_tests.json
9b185f44b5811dff24be718210a84e52b805f22ccd641b83b0dbccef72c913d6  companion/results/graph_tests.log
6626db9e2dd732a8ea1d2329b3917d23fc472d761555ff5c1c047ea0dc1eca75  companion/results/hardening_clean_graph_tests.log
79ebe8aabc9b15f03886fdcb3415adc1227091b4dae4b39cbb11d7154f1336f7  companion/results/hardening_clean_reference_tests.log
ae2f0fcdfcc96d80da47646b0504f822daa498d96cbfbb3499b51e028c135ecc  companion/results/hardening_clean_review_tests.log
0f3276df416fe86d483f34024c4075ff3a1b526419942466ff70d7be88fb4bc2  companion/results/hardening_clean_revision_tests.log
90c3159af7688db92451227b0566b136e6a09c9ecc453c45c452630b6f930f0f  companion/results/hardening_clean_upgrade_tests.log
68e69520d8bd2f756e2279d83d7dbd05bacdc2724d1e472bc14ae399a4a86c1a  companion/results/hardening_graph_tests.json
c92584cc202afce30d726fd432696e939925fdb2c1a0bc406b43c1f1f84bf53b  companion/results/hardening_graph_tests.log
d6b870a8b7bf4bce80bd74eb2d0d0345e76b3ef1e8bc8957599cbd9df5e433e0  companion/results/hardening_lean_build.log
4101570136ca0b769d2d3e0d9eac2a634c6b3faeb699afa88f21520b98b30637  companion/results/hardening_lean_publication.log
752dd97b2b8806df7c2a9a0a6cd905ef681c0250f746e2ba7f0dcb335f8e2962  companion/results/hardening_lean_replay.log
70aa5ea7b6180aba1e21982b92f10e2f0051c834927438508575a22179ee85cc  companion/results/hardening_reference_tests.json
35eb4d5396cead2f61ee9c0bf62a8ab0fa1d0b8bdaff093a7a36b1294b38a062  companion/results/hardening_reference_tests.log
5315a8020bbffcb878c80422e2962f001dece904fdf9f0e8bc56cc5b561afc16  companion/results/hardening_review_tests.json
d91bbf119ec2cf36c1f820292b71d1f389b04d256b4ddea05e5c624fb0256ddf  companion/results/hardening_review_tests.log
6a52555f96523745706aba506dc686d0d747a36a13f1bb8738ab9a197ac2d23d  companion/results/hardening_revision_tests.json
f0db5eb27bd7991e36cf1e4d2d07f3588a114309a67a1a394bda6b09129664d1  companion/results/hardening_revision_tests.log
730ff57ac4e2c30c16a7f21f956d3a4d950a36477ef2406c65f4aefd02868183  companion/results/hardening_upgrade_tests.json
ddb3b883362d2aedab0cdff204d3e2d33fe0f74e555285a72d66aefb229ef685  companion/results/hardening_upgrade_tests.log
edafb9ca783613323f41fbaf49c0affa2cdd2c138fbc337177b401d29106e4d9  companion/results/keyword_update_record.json
4eb408d5e7bedbb09e70f6c5e467f5d3422da2ca633cd617e74a981a331a7bd7  companion/results/lean_scope_audit.log
8ab9e9d721f110ec642affbb4ccae443854909272c4630a147d6a6daf2e1423d  companion/results/mechanical_audit.json
139c7e61c8f03f734ab9d01dd646c8046888fc1b621ced408c7e0bd2c45331aa  companion/results/narrative_alignment_record.json
636018265f880678fcb443c13eec2ef13b7308e8e8c48fa176560378e6a7b2db  companion/results/onishi_comparison_record.json
44e03871039ca4e4e309d13cab07b104535746a0185cd04656b6ae00ad9312af  companion/results/priority_editorial_record.json
f234eb672546e28da4ccdcd0bcccbe84356ce39291031bdd9c4c5136295612fa  companion/results/reference_tests.json
2dbb7baeafa7841db5b6621eb38ab645d3a0e0e0650b71b8caff222277173975  companion/results/reference_tests.log
d941637e34c80b139f624a78890f1a87c7e3b81cdc02231ec49f8141d792db72  companion/results/research_upgrade_record.json
dea67f765886dcab55b7d6e2c25a144ae6e75583a449656b74475ad7161a9aa7  companion/results/review_clean_graph_tests.log
95b1be695fc328b39a6c904ee732e65d91e7e0f028cffc0e83901d8c8630d4f9  companion/results/review_clean_reference_tests.log
5f6bc2d81d5cd6c1dc7bf903a28f046869df5c48ad5b3b106dac111acd2370d8  companion/results/review_clean_review_tests.log
c77711dd4f7efb6a1fdcc4319440b2abfffe623869a33360ce298f3b56db1fa8  companion/results/review_clean_revision_tests.log
337fd98eb99958bcf66a740800fa0be77ce5b7e58027adbd4c24ecb75cbf9d7a  companion/results/review_clean_upgrade_tests.log
6818636da4d6390a6ab0802c043f9919e3a38fdd0fa79169d657545618b1dc7c  companion/results/review_graph_tests.json
303b1c9331a06eef9538daf54cf09cc2f4390b6d1b3c4686752fd8ff8b8e81e3  companion/results/review_graph_tests.log
e7e6691e8b463a15a36264b15c70b18a23d2c6af8ce04e6c285e4b5aa9f07a72  companion/results/review_lean_build.log
4eb408d5e7bedbb09e70f6c5e467f5d3422da2ca633cd617e74a981a331a7bd7  companion/results/review_lean_publication.log
69e210d5902092ded0794d017427fdf90cdfae669ab9cf160320b9f83b8d4c90  companion/results/review_lean_replay.log
be808894859c870782b1d02e588bb9ea2dd1a6c121c74296964702efb5bde0ef  companion/results/review_reference_tests.json
90764007672bc75302f13fb5a1810aec6a9bd1cf42cb6b3d6525cbc289a5599a  companion/results/review_reference_tests.log
32ebce2ed1ae10833cd057cc221556df90ee699f7b2f8f865479bf8d4758ca31  companion/results/review_review_tests.log
a6bf8a7b7dfc5da8d9e83cebe72b9f00c8886efc0ae73950b919430c76f7bc81  companion/results/review_revision_record.json
bd8f8f0d06632d3f2253b159999d93ac7830557aeab47767836219920127abb8  companion/results/review_revision_tests.json
bd8f8f0d06632d3f2253b159999d93ac7830557aeab47767836219920127abb8  companion/results/review_revision_tests.log
ee1484f6e4a7a8f56e5732d0d53b25a7725c80bd8e2a7912a5e34031eef32ffb  companion/results/review_tests.json
71ffd9272d594c99f8d760784751c6ffcb2de4c606b609bda16dca79767cc7f0  companion/results/review_upgrade_tests.json
25c0ed46b09e2eec362958d9f0b1bd132e079f2c094713d879803d96e891b37b  companion/results/review_upgrade_tests.log
b6b5264f0219b6c6d8aa3abfd99b73b1b8d8b37be33f27070228a03e3b310a36  companion/results/revision_tests.json
f7906dce0f4b8452f87d9705e8095376396ef75737f4eac4e2dbe65e5c61a876  companion/results/revision_tests.log
8cdb9d872787675cd3fdc3bd93e7b955bdafea6f0347785f74295359857e83bb  companion/results/title_revision_record.json
ee2943fc4ef2485f3aaa66a97d5f7c7c8a08f71765ba5b357875a1aaccaf7215  companion/results/upgrade_graph_tests.log
4eb408d5e7bedbb09e70f6c5e467f5d3422da2ca633cd617e74a981a331a7bd7  companion/results/upgrade_lean_scope_audit.log
784d542cc673cf31e20bbb8edca201c5e91eded036c3cfb06701baf5c43d2db5  companion/results/upgrade_reference_tests.log
b6b5264f0219b6c6d8aa3abfd99b73b1b8d8b37be33f27070228a03e3b310a36  companion/results/upgrade_revision_tests.log
6f879c4829bce6d49a5268786b4c13c0e7412657a2d0277fbca4e792e998d153  companion/results/upgrade_tests.json
8c0a570c405c3bf22650b8247459bebdd8354d3e36c1d6f85a86be4708453c65  companion/results/upgrade_upgrade_tests.log
0953677719c1587b266f6a266497461ff33adef3097bb7fb175545fd7b846cf6  companion/tests/run_graph_tests.py
8bd025dde705474d07852dc56ffe7a554061eec221614d035f1f689c263aa84f  companion/tests/run_reference_tests.py
9471acf5cb0f0b67a2e899b62fead82a2644488129e6d300991884a8f9ef6a79  companion/tests/run_review_tests.py
49e9f383b51bcf30e3f487890f573ec498e2b07bac7cd445a3b2102223e878e0  companion/tests/run_revision_tests.py
ccaf46b430e19cec143867504c85b5d9af719bd120362b28a9f7fc3c70ae8cbc  companion/tests/run_upgrade_tests.py
20710469635af5b8fe212af66b607491a1bb043798f08e714f0d32d6b10c2508  lean/ANALYTIC_DEPENDENCY.md
eff4a209c9bea0857d881629b755b4f9b93ba735f6773bea2cf62a65acf238d3  lean/Erdos278/AffineInvariance.lean
f5ac0daa75080d6c54d24790c2c5a057ce11df8473f821fcdfc9c6d54cd7e044  lean/Erdos278/ArithmeticBridge.lean
c769f1ec9bbcd88ccb90eb477727904a4992260466937f852e1334ebdca9e2b6  lean/Erdos278/ArithmeticFusion.lean
f1d49c366de442591e53ed11540a5ededbeebf1435db5e82127518b7d7d7e892  lean/Erdos278/ArithmeticIndependence.lean
797fd36ab9252e8b26a793b1312b61bc58d269d9b140dd4f6c5e745257be8033  lean/Erdos278/ArithmeticIntegerFactors.lean
f8224caf03840cbd4ee4ba0645a762bf15d7faa007a3ecb730bd3d5217e3a4c6  lean/Erdos278/ArithmeticMessageBounds.lean
dd8e6ba8dfe1f0197eabe1409eed18356480baa3b3cb393e38ac5c5762822633  lean/Erdos278/ArithmeticNecessity.lean
361768b4725be939cb2ec2ee7a3d546dd9c73dcd0ce48961db38ca7762ae2e24  lean/Erdos278/ArithmeticShearer.lean
5e7900406d494726e7bd84e4496c30e969219d2e46b4c7b32ded2ca53a5e94ca  lean/Erdos278/ArithmeticTableBounds.lean
1a19218ef2f0e52caf62e07956334edd4cca339ea1a521d17c980c8d2009c954  lean/Erdos278/ArithmeticTensor.lean
3cc6c8a85f97bf909684f4c2542c03ea302059e6fa9936d44cb212fa8f8ef8b0  lean/Erdos278/BasicBounds.lean
106d18a12a08f48484a2f048ddf48f7025283d595caefbfc67ca1c6b964f45a6  lean/Erdos278/BernsteinThinning.lean
825c697475bef71e2fa86d13bde49b2ac9a495708622124a1c7cbeb5f68cd33b  lean/Erdos278/BinarySize.lean
f1b03684e9f07adfa734642fbc2ecb79cc58f3001b667fb9c5d00b6e1e162e76  lean/Erdos278/BoundedCountingQueries.lean
d3800c5740028e8c4a69745c432e3c12985873ebac0deeba3f9e14aef33ef5f4  lean/Erdos278/BoundedCountingRecovery.lean
f8771fecf0a54e91c30d2b6f8c27d335093da59cb57541ff89d56cab8d9fd2fd  lean/Erdos278/BoundedCountingSize.lean
65169cdd69f67f3b8dc667ff12e883f4172fa1f3906276abd29fdbdf72c31f01  lean/Erdos278/BoundedPadding.lean
c6bc4cd581436a4aa291fc3f14595705e7b6b4c09bfcbebaac486b61470ab9b7  lean/Erdos278/BucketElimination.lean
1b3a3282214c9647020d28cdf33c08100c199c93995b64ead89868bba4234b5f  lean/Erdos278/BucketTableBounds.lean
a0006e122c682cd885bdc49620ca7f43eaa794fc552c17b1d163e69bb0c21313  lean/Erdos278/CDDensity.lean
64dc7d8a66d527360e75a33629bce9ef7e64eff29a937a0089ebcf09a8e5b046  lean/Erdos278/CDExactness.lean
bde3205aa5f2b616c45fb679b8b56ee09b2f2866856d7e7df7d436206cf77d27  lean/Erdos278/CDStrictness.lean
074f0f056cdf5ee09de4d653a159e9def901d57d2bf493c22f838ee257006cd3  lean/Erdos278/CachedSparseCounts.lean
021bf35da11c488640be7c6cd63f9398534f1d6116309e370816914263f4bcb1  lean/Erdos278/CanonicalFrontier.lean
106b77ae2f0d2b5d91207055546b0900834ef62fb553b2ee5dacc1ef91c05df6  lean/Erdos278/CertifiedProductGap.lean
941fa6a569455b5c07940f948a4978fb5c984217c0644c761a58e6163a65e686  lean/Erdos278/CertifiedPruning.lean
75f09ebb5bcf383a1fbe51eb4dc776664082b5d616b037a589b6a43f9a958be5  lean/Erdos278/CliqueWidth.lean
17f728ad2487bdee88d730f178d88b98b16ae18817ed1d7dc9c908f6b8587fde  lean/Erdos278/CompatibilityExpansion.lean
aaff65fc76727ad23e1866feddcf9293b4029d5a4251fe3a652d1d1174c57e49  lean/Erdos278/CompleteGraphShearer.lean
8c40a2819709db8236f986d9fb683354394e4579eb3e4d96b0bd7bf94133f4ff  lean/Erdos278/CompletionLaw.lean
c617e2aef4cc423d31699bcd526c74771e810e346040633fd0374521a4f94eb9  lean/Erdos278/CompletionScope.lean
98594d8ae92c3dec26d470bf8552fe9eaefff8337f573e3c67efea0e2420ee6a  lean/Erdos278/ComputableFrontier.lean
a016318499aaa0bf6b76a83c2d60208a1cac4a946d8f10ed2680da603fb190e0  lean/Erdos278/ComputableTree.lean
314b0a11a1bddd2422c91556aead2551e2df74184a6f2db6e1c9844231bb6984  lean/Erdos278/ComputedFrontierCorrespondence.lean
4bcb26ffca84033bf5d8d2ba04fb475cdf1737bca992c76a1eba61240596dbd5  lean/Erdos278/ConvexDomination.lean
803e4ec86a919e6f8d54d495b7ac77d6262ad32a39a378d061fb6c2f0715abf3  lean/Erdos278/ConvexFeasibility.lean
9f136c99a8e1e270657b95776cc240e12e032a0e0fcdbf140e09f2f9b1015f10  lean/Erdos278/CoprimeBasisCoordinates.lean
91c4fb1386f3b778d2db79dca9d33b61267bf7ccaca6b25d9ef26f07d4ddaaa5  lean/Erdos278/CountingGraphDegrees.lean
d2f786377b9c8bb2a94e9097698f09d2ef3268e53244847dcb7a8cb38558a158  lean/Erdos278/CountingGraphEncoding.lean
3f99e9b62a9998b149679477e8470aa8266cc2dfe76d83b9ec200d84523117c8  lean/Erdos278/CountingGraphPromises.lean
0665ab80fee28575ecc06974ea2abb52571cbfe51af212b619222ef8a92bde42  lean/Erdos278/CountingInterpolation.lean
71376934df35737a05f84afff807aeef7f11aa8593869bdfea7815cbc1535557  lean/Erdos278/CountingOracleReduction.lean
b4f7ac6e4b146c066cf886a5dee6cda65f700853ec3021c8bc90b5831781321a  lean/Erdos278/CylinderLaws.lean
891cc55f900485a0ad303492e913a721ac94461407e4d74d39eedac01094b5f5  lean/Erdos278/CylinderMove.lean
b0b3aba20f0f756dbfadd5ab79ebbc64f3ce652971560ead4d934e67728230ad  lean/Erdos278/DecompositionOrder.lean
075e80646de6dcacc2c74ac04f442fdad926dd4b9d4db7b5fc9308c09d23b169  lean/Erdos278/DecompositionSelection.lean
697caae061696eaee3b1d677991a6c8f948a8b15195f2f7e9cda55a45c99a4a1  lean/Erdos278/DecompositionSolver.lean
32ad1e0f72687f15941a6ee9db98cf9c5fc1c52c52563e70ff958aa687058387  lean/Erdos278/DenseArithmeticSolver.lean
c8171a4b443a31d5e9d79c2114326c9cf5c6c665816722783fd2dd1954cf64a6  lean/Erdos278/DenseElimination.lean
159dc36fa34fdf22de88153616fe71788ad293f82eaf92773138bb223842808a  lean/Erdos278/DenseFactor.lean
5aaec85a2ef0bbf6213d10895d2344f71a5376a43d27c8deaca95e15506c948e  lean/Erdos278/DensePrimeCounting.lean
666ca9591af47c428c106f7d593e00edd948ec52104a5137e03a60c520fb372b  lean/Erdos278/DenseTableTrace.lean
a41c4d853ccbe7ded9c161593456a9c64b70c89309962166c17d5fb853dfa08b  lean/Erdos278/DigitCongruence.lean
e93be7091008eb7701cb741393531b2a74557853cba6e4a947c6e1bfd92ab8a2  lean/Erdos278/DigitModel.lean
3b288307e4b40846d941ad9fc270f48eb9d00ba0e3254af91e2765acf7e12753  lean/Erdos278/DirectTreeRealization.lean
db9e9a2fc73ee9fca9ccfde155cae9b9435abcb965944feb96ab6982bccdee8c  lean/Erdos278/Disjointness.lean
31d317234d7969020d8d87805ee33c6ea1c038f43f27281db5887cba994d6871  lean/Erdos278/EventLaws.lean
7a6ed90dba34630aecda3f5887423e81f501840ee430998cd3b1308030b43856  lean/Erdos278/ExecutableDecompositionOrder.lean
3b6b1317cb46eb78ef6104b5688f1cc9d2f885cc8e7614b508054a70df3b0919  lean/Erdos278/ExecutableMasterFormula.lean
daaa3e594c0d1c9b13ac39e51fdcffa46f513ff02ebb5275ece740ef4a7999cf  lean/Erdos278/ExecutablePruning.lean
6d311743a35f541d415dd76718e006c78ba6efb4f13fc748ae0da16f2c9ad788  lean/Erdos278/ExtremalValue.lean
6b66dbdfd6d3b7aeac8b2c16e97deac494332aec43b0c5b7f034fa39b2ccc9a1  lean/Erdos278/FactorTables.lean
74debb80479187f8d51d2bb1c43aaa2567aad217b5b5ebdada400f7dc6253c5c  lean/Erdos278/FiniteCRT.lean
f98c8e9fdaf3fdd4a685f26bd420a5bc7043e08a4afbd3603c92483c18bc0b7c  lean/Erdos278/FiniteDensity.lean
f76d6b27bee5af20c6c04b6614f68c00d149efb2721e6d350a441d8d6bbc7131  lean/Erdos278/FiniteKeySelection.lean
b0a1dd7f6635a603f86eec79589057b11b1924148c71ef3fec70a96d88e22003  lean/Erdos278/FiniteMinimization.lean
2bdce85ff110ebc6b950a23410062d1359c6a4e1c571192b3dc34759464c1e99  lean/Erdos278/FinitePushforward.lean
972f938cb0273ad4186fcab1270a4ccb403c35f36a27c4b6e01f38539cb904fe  lean/Erdos278/FiniteStateFrontier.lean
b754bcfbec88619bcc47f38159a605e60b137a2ec2577e9afbba817728334b78  lean/Erdos278/FiniteVariableSum.lean
ffa928875b19ac2bb8de83df890ba54275a644a2e62150e663416a2e663d683f  lean/Erdos278/FiniteVectorCache.lean
89c9ccb6d82580e40c0c2d3f377351aea535a4b1b246985125677c295a427c7d  lean/Erdos278/FourthPowerSampling.lean
3c53c65ebb0b0d9774122e5ad431254699342ac6eeb703ac31de219b0312314a  lean/Erdos278/FrontierPreservation.lean
492c7c108be9245a8eb5573bc7610d6b863a565d535e009875d001174026f303  lean/Erdos278/FrontierPruning.lean
57152012173e5e581d0b0d0b57798d857968dec315385e470f30585846577f5a  lean/Erdos278/FrontierSeparation.lean
8b3619b9a774cac836fde34a753cc95b96e74ba1103617930a7b5650a054ccab  lean/Erdos278/FullStarBalance.lean
de5ba7c450b783bd59040877a1bb119b5ff77f197f923c0bb7f08824d5786419  lean/Erdos278/FullStarCoordinates.lean
b54adb3823ae1a53bd2d076f9816fec6009b5a1220f05f8d1dedc990c5ca4b5d  lean/Erdos278/FullStarMinimum.lean
5366cfd56c59c95f534464df9416219d335306c3deef8a3af2ee10aab1c476c8  lean/Erdos278/GeneralizedCRT.lean
8abb32b5ade1b60cceaca61efc69ebcfb06a7e7d63b9884c2ff4e20ecf1c54fe  lean/Erdos278/GlobalSaturation.lean
e4504d1616d99dca0ca08bd1946d7551cd0d350f5edf4a2827a5f7a9aa8d46c5  lean/Erdos278/GraphElimination.lean
09a31b78430b7ff4ee4e70f1733f793d343e4fd23ce854e087c55f4b0d603c29  lean/Erdos278/GraphPackingConstruction.lean
4c1b8c5f181886e5b1a3af047fadb7d39fb6b9d9ef5d0a993fabb7a0839f68c9  lean/Erdos278/GraphPackingEncoding.lean
596aa6373babeb36f1322dff5c93a99c1cdcfb6cc0d8d0e5c59d7aa7b22b9076  lean/Erdos278/GraphPackingPromises.lean
9caaa3b90eef64a20457beb8d29b3f528c78c83e65b661d25f1419af090ffca3  lean/Erdos278/GraphPackingReduction.lean
093a6d4dd6b7c9b2e08d4a661756999a3a6ed8bcec55a9adb1bf9cd706873b37  lean/Erdos278/HeavyPrimeResidues.lean
66f8ceda123dbc6c1307c628b2b857b29fc9d8f4e763e632951c3ac4f4cc00ef  lean/Erdos278/HoleCountCertificate.lean
4d9fc4a8fa5b165de3de63e3a8da4bcf28bf6a510276c9b8c4950fa8134bb82e  lean/Erdos278/IndependencePolynomial.lean
dfdbd6c870f6a8b8c1f6d7a88bb32897f80a5aa826a6bf9f6547ecab70d9f926  lean/Erdos278/IndependencePolynomialMap.lean
c281beb6103edf1dcac42021955fe4af50aa8a1ce235bc89a79ff9c09597fa41  lean/Erdos278/IntegerCounting.lean
0f377ab17e5717e9a4aa30f492fb5efce811d8a89bb7611133ffd576f07a0360  lean/Erdos278/IntegerMaskTensor.lean
359303ddd26c10ac6c31bca7b669ae38e1b94fe85d4ac085018ba274ed379716  lean/Erdos278/InterpolationTable.lean
94dcd040f6aa2993a2a4a4805882a8bbb2d2b615cc895398579cbecf40ede5b8  lean/Erdos278/LabelInvariance.lean
e8517b4a16dcd5d3af41db9b21841b328264aa8e5b421c553da73efc49799830  lean/Erdos278/LeafConnectivity.lean
553d059bfe41541bc5caad4faac1246bc33150426f8d83be6fc107b02f810fb7  lean/Erdos278/LinearElimination.lean
76f6eb9194ead26bc5c88774429f37d2de6492339b88e3fcf681f95306d5a554  lean/Erdos278/LinearInequality.lean
9235913cbf070a458f16b6f5d23fc745ccc020eee67c2887051ccc23cb86c9be  lean/Erdos278/LocalMaskLaw.lean
0f1255a4daa7efbe112183bb825a1a5fb5507bc29ff2de5ab909bfbe093d0f37  lean/Erdos278/LopsidedEvents.lean
5b72802e480e17a78235d27397c2db372e81951d22fe824d3e82f2dffee05ed1  lean/Erdos278/MaskTensor.lean
029325bf1c5a450300143125a27bf500cc268c687ce14d0d2ad32c8d9887ed35  lean/Erdos278/MasterTheorem.lean
20b637964ae5e0db2a0cd5f3e165a292b7c5242062affe804a617ac3460bcdf8  lean/Erdos278/NaturalFactor.lean
3e9da1c2a3d85c5088baf70202f056f21e59095d56b1077bdb58be1242a694f4  lean/Erdos278/OracleEncoding.lean
19ff4dbae5782a3b8a2cc732121dd8215d879589e624960b4763f610fdc0c279  lean/Erdos278/PairPartitionCount.lean
a52a79bc6e448b7855453e5d92108f35748aac4e9efc4fb76776059190cbb064  lean/Erdos278/PartitionExposure.lean
b8e8e49ca951b56cf3d5ad7b4dd5388e5a7bf7bd4559fde13da83f58c5ca8f43  lean/Erdos278/PartitionGap.lean
fcc2834ea84230a480aaa6f5a62f11edd10dba9a7c0554f89e2fde66d0c5cee6  lean/Erdos278/PartitionPairCode.lean
b4121d6286f1f223a2952faa6b9d173d205ce35a48490de7b7732e4b2261e8b5  lean/Erdos278/PartitionPairRecovery.lean
7b0de6bfb72b182a1ce38c7ead5cb59601a166c6216b125b66c1b66f72277ee4  lean/Erdos278/PartitionProducts.lean
d90caff5c929adbc473e6f3da6235c900f1f53ad7bd605aadd2f74c7744df755  lean/Erdos278/PartitionProfileCount.lean
52a295e36d7c769f50a889a0c716210aaea072c6066e6a36daaba26e7572a651  lean/Erdos278/PartitionProfiles.lean
22c6427c1397e519f75f4ada86e967c357d6269d67f303a801f947ee0c72cb16  lean/Erdos278/PartitionStateBound.lean
bf603dce3cfcb869f367795c784a71baac56253dde35f45019bd4ed558f626f5  lean/Erdos278/PartitionTransport.lean
c00d57d35454e7e8db0e1fa51349775f409a86e609c9b38afca7d4a158a69601  lean/Erdos278/PartitionTree.lean
55be19a7ab569d5530dad2fb81df5db0f8cf5269b3716031524e580010ded62f  lean/Erdos278/PartitionTreeDepth.lean
f5585f468832ecb8bce88647492b47f8695c59d509906c9512e22d9e51f062bb  lean/Erdos278/PartitionTreeExtraction.lean
ff24e4cda5db97cc35b05acddaff77ad5c0f14d153e946ad2612e9f49caa8aaa  lean/Erdos278/PartitionTreeLaws.lean
0cc1ab58a01cdef986080b73e24541d6bc64134368251b1a401fb0cb06f4e0eb  lean/Erdos278/PeriodicDensity.lean
cdccc9e798ba0bb908048a715b399955ad37933607667ce809b608dbb1c7defa  lean/Erdos278/PopulatedFourthPowerSamples.lean
f3ca417cd775b942cf90898d586b0f126a21976603bcf1f54f580aa2a1294fe3  lean/Erdos278/PrefixCounting.lean
582017d3537876e6890cbacd0c93a3194dcf4cddcadfbabc52260127f07375d2  lean/Erdos278/PrimeCoordinates.lean
3a24a0bab442d2272484b9c71597b07addb1ef0b12116e43463059ad6e3348e9  lean/Erdos278/PrimeDistribution.lean
230b768be39b2aefa2569f6cc81f0eb77f249e3b180b8c942c1a1087299171e7  lean/Erdos278/PrimeGraphTables.lean
2113bc0011ef01a83e4fc71f6bacb3f72590a472d82a37512faf560e63f06c6e  lean/Erdos278/PrimeLocalKernel.lean
6c16d641717edc6c22327aedfb15f66d889c1cc0b27ba1297d49cbb067faf270  lean/Erdos278/PrimeSelection.lean
19347f9cf07eee5faae742e623a5581dda1fb6d80edf1fb70c9c39b0538f16f3  lean/Erdos278/PrimeSetEncoding.lean
04750a3c3326f7b682ffe015ec41e1804831189be2fdeb59c060315b49332c23  lean/Erdos278/PrimeSupplyInterface.lean
f95a4a12a936379168ad1e360ba6ac9702ecf4158b8994bba55e0c451cac059c  lean/Erdos278/PrimeWindowConstruction.lean
9a58192ed711558f623dbcd68f780cbd370e7b16ade66e279598a237cd62550c  lean/Erdos278/PrivatePadding.lean
f315b1d3dcf484c44e2b7d8713fa418a1238fdae4404d2f55fe7e04a6365d324  lean/Erdos278/ProductApproximation.lean
fd5ba8a80c0b1fd9baf8bdf1d03855e79dac2afcce4b8b6e59c695a3d4d1caa5  lean/Erdos278/ProfileCoordinates.lean
b18dc6f1eda3778adeae6c3e2878b8def789f56a26481ec1d474c4a4ac5c3e83  lean/Erdos278/QuadraticGap.lean
0e5ae492555da1f89fe27148ae929b237e4aaf7c736aa0a63885d4e69b4e4f93  lean/Erdos278/RationalConvexHull.lean
a317a88df6cc344360f4de5fcaa6ded32d7cca46b50e39fae524d8d47a193e10  lean/Erdos278/RationalFeasibility.lean
c437e8719e7f5185f4a45fbc92b96c42ffd50d84d546ebecdab62154bb43180c  lean/Erdos278/RationalFrontier.lean
551dba88436f5aac2a9431453f40efc305f6176d8800ca6c6c868f42edd74922  lean/Erdos278/RationalInterval.lean
af2ae89b9fa6d60729814a2c3e0825854040a941ff8a82ee78e16375dfba82bf  lean/Erdos278/RationalReduction.lean
61c87caed7f21c038b9b1faa7925f15e20329c9604e4d95526beb696a29f44f5  lean/Erdos278/RecursiveArithmeticKernel.lean
207ee619affb4832c7ee82998bb026912dec75acfdb0e3de2603cbcdf902c24f  lean/Erdos278/RecursiveFusion.lean
e4d67857e41f34f51b60ea22a15277be8f5ed09de2d1a90ada7d628f88d4875d  lean/Erdos278/RecursiveTensor.lean
d989c64fb77c57295e5baf4705de53e738bec6189212dad31abff7d3548bbafd  lean/Erdos278/ResidueClassCapacity.lean
af0d5ab77083dd80cf6407ed404c14dab5b6c5c3500ac5c8419a86f5294527ac  lean/Erdos278/ResidueModel.lean
49abb632c5272f48fbb0e9bf6a3521f0c76459dff4b19f47a099aae01b1f7cf8  lean/Erdos278/SampledPolynomialRecovery.lean
e210ced2f27da1bac180acf4cc940bab2b24ef04e1dd3b869a87f3073a692232  lean/Erdos278/SaturatedKernel.lean
6f2735dc87ccbe89434294e62e1a8db7948cf6bf142bebd76a6abc7326f00b0e  lean/Erdos278/ScopeEnumeration.lean
d33781cc8ab04ccd1fba39d15c1fd41f249e5d25d145b5509d52ab881b4d0e73  lean/Erdos278/ScopeFusion.lean
9b4b7f9b740794ce8822c77b16963f6adab68a9cf17b2f94680ed1087e7c4a66  lean/Erdos278/ScopeIndex.lean
bf32c3f1d644fe519179bc891784277953b5f6bde67d3c21a72745f964ffd84a  lean/Erdos278/SequentialMinimum.lean
5084ef3add6d007260a56b576f6899500ef00ae7562a71aa7fbf586cd8006a32  lean/Erdos278/ShearerBoundary.lean
7a9bc8746b48d8e360026232a30001760f78d93e622de4efb7b926f97c6afe82  lean/Erdos278/ShearerRatio.lean
81ce45f60fc9e24fa43dfc0ffbb5a4e87f23fee3cfea2bb214d3a8cc7373f37f  lean/Erdos278/SmallPrimeSupply.lean
ac6ddffde9468fa62f7dd9da3fccf8759f4b0ddf220d575a8ef61465a3e5236a  lean/Erdos278/SparseAtoms.lean
7efedc0a33030520b4bdbd6a8850f2e4456dc1b5583df98f2968f03982d29225  lean/Erdos278/SparseBucketSolver.lean
f42539f7563577223ebb7da2644011acea451113689469c48adf82beb786d075  lean/Erdos278/SparseCounts.lean
4053e0b753e50e936a6763a3133be692e449dfed0da206fc8ac6e4c4a58b4bc1  lean/Erdos278/SparseIntegerTensor.lean
7a63630f678741339cb8d1d3f6a131f97a60973c3d8c22b3a43a941d0a3dd351  lean/Erdos278/StarCoordinates.lean
8b62db25cde6769c054ab79d7fa2426117fecd3b652802b8d93d7f0e4658aed2  lean/Erdos278/StarDensity.lean
d71e89b3fcc5ac701c73db2ac139e40801861ca044a8ffad81b3587234edf542  lean/Erdos278/StateProductBound.lean
bb00d92ab50e5fb91b3159035ff1cbddd7f3355ea4a7178f6c640db493a2aa74  lean/Erdos278/TensorReindex.lean
31d965053a68237c2109b034834d5e43ea61f13f47d33bbbf434cc313a90d0be  lean/Erdos278/TernaryWeights.lean
bcb7f14b980189a96e8986b512f3cdca7de4785e0d2f933bb7976e5baba96027  lean/Erdos278/TrackedElimination.lean
dbf447b958609c9565c4f26e33855cbaa59cccbee1d1e951d1091fc7b8aecb52  lean/Erdos278/TrackedFactors.lean
8074b432b8a6aa5e839e0e7b31c52bc282651cd4b8038bd092cae9b3e4cf7a27  lean/Erdos278/TreeBagPruning.lean
cc5d7b26df817d3f9c209ecd603c3f70e30eefcd499609b9d68745d5cf1d1a56  lean/Erdos278/TreeDecomposition.lean
062c19c8fd41aad3df045cd93ce9fd33ab795fde082113dfbd1f77e36e8d3873  lean/Erdos278/TreeStateKeys.lean
7e7731b4ffb37573cdc23a3dada57c83edae7e1d2605c47d3718c08b50284c93  lean/Erdos278/UpperHull.lean
ef02766f1084e3a08f85f942467056f09eb60731ed30f2b83d6abe7f43ff555d  lean/Erdos278/WeightEnvelope.lean
38d5269851067cc281203b391329afa7f43a9e4c76d82727601695a57c331fa3  lean/Erdos278/ZeroOverload.lean
11278d3fef627ae1e944a2b5888bd1481dd44e011ef8c94db9eda94d76f9080d  lean/Erdos278/ZeroOverloadKernel.lean
ddc1a479d80bfd24b64432dd4a48d6636dcbdfde2700bfe4ee33c72f1caf706f  lean/Erdos278.lean
8939046df6bb30169c487dbc879def7cce707709341b509a3aa985f21c7890ab  lean/PUBLICATION_SCOPE.md
0a0c9460f9ab30d46156f6a24cfed581be2be604ed58ab816b8c0ba12f5a443c  lean/PublicationScope.lean
e1823f4891c39aae2c7be6bb1b7e7260e323ac4d4eeeb1e298414619c5ca0f7d  lean/lake-manifest.json
624f598c4ad0d6fbb61a1df765239e7bfd924467f7bcdc4ece1f6f1c88f4cc69  lean/lakefile.toml
2bdc48adfa58d0017e538a0ad117c5d73d35deec879978f909406a80c8037273  lean/lean-toolchain
7a2043c3ebec9442954a74735a33d24e2b2d37e94be6549b32fb7f8fe2cff63e  lean/vendor/README.md
a77081ee7470d0d2dc25114572fafe24f341cff0b27fa85961b69e8abe053181  lean/vendor/SOURCE_SHA256.txt
1bce2337ed4de0e6e735819e89b4d35ad81c7e996e6cade79e8a9ef781dba314  lean/vendor/lean-architect/Architect/Attribute.lean
92ed89acca564cdfb0cb696a3c2e3b62a7ccca82cb6fca85d0f994ffd2b2cb60  lean/vendor/lean-architect/Architect/Basic.lean
921633f79fef58cf0d8540477785c4d9213608642685c21733dd3c61855d154d  lean/vendor/lean-architect/Architect/CollectUsed.lean
8497d574c12414908829e8b25a96e0ce52c643bd48da66b678d1623db395696a  lean/vendor/lean-architect/Architect/Command.lean
73de49bb499fc140dce470251e3f657368b788dca1659317e902f476ebb9556b  lean/vendor/lean-architect/Architect/Content.lean
6ae5e51b0f041d4cba8da31e0d8ff96ffa8ae89bf6dc33d84d7c0349dc92bd34  lean/vendor/lean-architect/Architect/Load.lean
ef52349573a02ff0714638fb47dfaf335c8c8a8c8b98192d3fc4d190ef4923d3  lean/vendor/lean-architect/Architect/Output.lean
cd152524b774c063cb382171e00c3b7913c5757063f560b10f9009e79f37f08d  lean/vendor/lean-architect/Architect/Tactic.lean
68748939e82259728644095b343599593f38abe65c971c14f910445a44f4ecf6  lean/vendor/lean-architect/Architect.lean
c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4  lean/vendor/lean-architect/LICENSE
c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4  lean/vendor/prime-number-theorem/LICENSE
b6c3ce0377e08884af9ead61b19c028635a0226c375af55460f6e41143657c6a  lean/vendor/prime-number-theorem/PrimeNumberTheoremAnd/Consequences.lean
64137811210c81187151a3d48ef170195cf36d58ea07a67ee61d1dc3212c82d0  lean/vendor/prime-number-theorem/PrimeNumberTheoremAnd/Defs.lean
e9db3c235cabf356d2b4aed528d0ceca6ad3e23c7a150d7049fd9ac796315823  lean/vendor/prime-number-theorem/PrimeNumberTheoremAnd/Fourier.lean
e688bf925c2130b291c536d3b93b72c20e41ae95d530c90915921d75a6f52504  lean/vendor/prime-number-theorem/PrimeNumberTheoremAnd/Mathlib/Algebra/Notation/Support.lean
c1cdb6bb509c6178bf17868c57e5b53721b87fb2774ef8562bc5945ffe5b11ae  lean/vendor/prime-number-theorem/PrimeNumberTheoremAnd/Mathlib/Analysis/Asymptotics/Asymptotics.lean
7e3e2b8f84e6c170051a6474272455bed2432e6fddac5660072318b9b4eda7ec  lean/vendor/prime-number-theorem/PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
e689045a2d7f92c71c68fda6aa69a89d4a8692187475ba432ed010f453110ea0  lean/vendor/prime-number-theorem/PrimeNumberTheoremAnd/SmoothExistence.lean
fe06e13fad5b47dbd324307ba246110515c4cb50f4c41d6cb15764fd53b1b8ef  lean/vendor/prime-number-theorem/PrimeNumberTheoremAnd/Sobolev.lean
99fcbcfaee33277e6ce6d1a1603c98d2fd7329dd7c57de88f4953786b9bc7823  lean/vendor/prime-number-theorem/PrimeNumberTheoremAnd/Wiener.lean
52be86f3f2711bf4c0af98959e1ebb9ec98cfcfe937e0566d897b1d3853875c7  output/latex/erdos-278-publication-v1.tex
2fc971c63abbf5c699d52a8e12aae49bbb87ce843bcc65a999db47bfea7764e0  output/pdf/erdos-278-publication-v1.pdf
814ff16b86de4ac794be3974e8efcbde4314a6c95eecd01f0aa2eb46c1420e91  reports/2026-09-16-focused-v1-audit.md
11e24fe61fd089e4de758d032b2419d96f982f2a3960ff1d1a1902b7e10dc988  reports/2026-09-16-title-v1-audit.md
18e3a069df022feeea2857bfa39b08604f9ad60de36067109e320fa3f68e3684  reports/2026-09-20-final-v1-audit.md
c7f06711f0e56cef193e46f7c86582ec5824be37560fb906dc4636c578f745e5  reports/2026-09-20-research-upgrade-audit.md
109794fc97d564a5298145cee9070facc138a2e16e45fbe29d4e03a8ee4e35b4  reports/2026-09-21-companion-hardening-audit.md
e125f34ce2e176264cd360e6cf913bdb34b41271c94936120fec0c9de5d6d74e  reports/2026-09-21-doi-update.md
0d626659d1dc72fee111f4e8c1fbd572f021e2521ebd212f21fd80548c25ffa4  reports/2026-09-21-editorial-alignment-audit.md
7b4b2ae1b726ed596e02d10190a809db2d67c0726b41613ffb4e591aabecbdc7  reports/2026-09-21-exposition-audit.md
17514c993a04e1d3cbc05206cfc7943aeabfff24ecf12dcc0265c1bc0317f078  reports/2026-09-21-narrative-alignment-audit.md
fd178b241201a5fc6623e095eb74e1ed37cb6f16135dfbaeda4e3e2d2cc042f2  reports/2026-09-21-priority-editorial-audit.md
b7ee88dd6ce51d28f96f13766a57ab67f4097eaa54195d3dd1f4e8eae55d55a6  reports/2026-09-21-review-revision-audit.md
e15b939472136ca4cd8ab73e2f41f443995c8479c2cadec64d5e894f3d09d5cf  reports/2026-09-22-concise-title-update.md
e9ca6fec77deddc3e9cd3d9030a6212a5182aff0fd74392feedf6443d0c53164  reports/2026-09-22-keyword-update.md
769fb03a3385ef8d239b5d5829d8824ff134165279c69b1c8aab131b165cea64  reports/2026-09-22-onishi-literature-update.md
6d282920660ec0204071dc560898df5da91f2d13f77b47a10bb79182dbba9000  reports/exposition_examples.py
