adf1d54bd1046d35fd224cc55c839b09305a6492bb8f2c079187c4245aa05250  anc/COMPANION.md
5693364954015970601d0d122996147aa5a5c89bd831ac38310060b8cf7a0849  anc/README.md
2a9944e7dd7e5ba87ab42540ef159dd6a6abb3e6fb71606d1b9c9a1ae8bb1905  anc/checks/audit_sources.py
2427d1dcc748117650a57bfac8f15843ff4b29a4bb6af7331ca72492243043f7  anc/checks/capped_gain_bellman_certificate.json
1bbe1ad9029ab2f52f1a2fd06f497e732aa3c2ccac53c48ef1473c990e837121  anc/checks/check_paper_consistency.py
4614f2b07f3171a53229b8765a2f22f607bdd5bf0c169ff76d8d52a07e84b62f  anc/checks/run_verification.py
c2b3edc4cbd54c5d610f81521df4d38ebc32ecb3bc5d041be5bccd48a8ad9fe7  anc/checks/verify_capped_gain_bellman.py
6bafd19e9cc6d5d6e5ccc197a6ce5f12ecd5c836c02f18c3427d32bff6a71c01  anc/checks/verify_capped_gain_full_chain.py
f401e894c17dfd635d33fa1cd1774824727b38e152154260de097e7b2c7a655c  anc/checks/verify_rank8_compact_certificate.py
000ec727872dc5a36d0a470c21756684a04d541bd60a1b19fb837b0bf54487e3  anc/docs/LITERATURE_REVIEW.md
61dc4dff26ec16626bc8f739148f495d65bed6bc06cbefa994bc0ebfa53aaa4d  anc/docs/SCALAR_THEOREM_MAP.md
595ae8a65ee4d74852a0f8a6a2670803ea44fe01e4962f4bd34767c971cc850e  anc/formal/AuditPadding.lean
85c59b365155be1e99194072adbe5241b973c338a1ec04f96363bee4a4d1d4d8  anc/formal/AuditPaper.lean
8bdeab9e52466d6a9ad023b28dd9bffe5e52f6df5fdb1d97c0b054b95b29c75b  anc/formal/AuditSimplification.lean
2db765c0f3a804dda62047eee7b188a108d24ffe4df7ca0b4f49dc5c01be9f4c  anc/formal/Erdos7.lean
0cf2e7e8642141d6cf8c7bcc9906c7df0d99ab266d62c86ac9cb5ea870e20624  anc/formal/Erdos7/ArithmeticReduction.lean
5932ba293a3ac0ef8593d28de6d6683bf462db31747b8c0f1c3434dcc1eab4c2  anc/formal/Erdos7/CappedGain.lean
9f844aa0e8f88eada6d8b7107ddb7f2e3aa3063237db2df3bb08693b742309b0  anc/formal/Erdos7/CappedGainBlock.lean
542d4d55f3bc37dae0c44f5815d4b66fee191a3770f2c03b79e93d2589ddece9  anc/formal/Erdos7/CappedGainCovering.lean
b7275bc24f020748554a5f2010c4a9e8268a4363fd6691ecc41b2338f0fbb881  anc/formal/Erdos7/CappedGainDepth.lean
a1ab3d503e97b10b4524391df4585102584eab47a26aa4447ffcd21540b5b9c1  anc/formal/Erdos7/CappedGainDistortion.lean
9cc127d1f7a4014de2689aef8641676d392e7258627a4cfc723b0896797f96d3  anc/formal/Erdos7/CappedGainEnvelope.lean
1f7010df6738a87cda4e45ccee1062561aa983cb346a223067ad05eab3f6c489  anc/formal/Erdos7/CappedGainFunctional.lean
78362463df2c3997e6a7fdbf7d345e1409d908d5ca42a51d8762fde1cc998e88  anc/formal/Erdos7/CappedGainGeometric.lean
7f4541df6ec9f2ac5edaa6f3f6054b1d59a7c2ac47090a9fff121cc18973bc9c  anc/formal/Erdos7/CappedGainLattice.lean
cdcbb84f1f17aa62d639796ec4f405e186f9f287b9abe6273d09fccab3953166  anc/formal/Erdos7/CappedGainLift.lean
50a75c3df518a51d2ffce353fa5168a8ea3a815d03b4c31008f6f81b6da917da  anc/formal/Erdos7/CappedGainProbability.lean
f6d3565ae629318ca6347851ddcf092b9c6db9e89dc3acb0326a583011e14dac  anc/formal/Erdos7/CappedGainRearrangement.lean
dc66abdfd02a97eadafce0a43779fac7f4b325e59bd0ef6b31f3c643565540d3  anc/formal/Erdos7/CappedGainScalar.lean
9fa9954a53a70e7625b1c9d1142b5423e4f9778329a2dd5dbfbc186f006015f2  anc/formal/Erdos7/CappedGainTrees.lean
c61eb5217c124ed7461e5ea7893759e95267f034930ad6017cacce8bb909a5bf  anc/formal/Erdos7/CappedGainTypes.lean
8821f4a1e642a005cd33e48cce345e4a8c8e31e77dc7a7d7e3f2b0a0fb0f44ce  anc/formal/Erdos7/Causal.lean
33973ceb1db69eda1e1738093fddd31a20e1652c6372a3381a060dad542dd193  anc/formal/Erdos7/Certificate.lean
a07d9778f81740dedcddb92a9517979deb48a2c4f24ea3636056706e8b2a9d87  anc/formal/Erdos7/Cylinders.lean
3214449a0e7983a1d21ab721c3beb3865fa66542ea82971837b5539334254da4  anc/formal/Erdos7/Distortion.lean
f7404a193f1bf6ef2b3cd6741453e469966e594ff60e9192cb6363fa124b6195  anc/formal/Erdos7/DistortionChain.lean
ad3e8702a076eb81fa1cfd5da10e0f0b5b95dce12a4052ebcb0f2208d0074637  anc/formal/Erdos7/FiniteProbability.lean
727757b25f792dace30db388f1b66f3d2d8a0749830639f0030e91541ff3cced  anc/formal/Erdos7/GateModel.lean
051268de09179fb09c32a2626945d13854a4f74b836374b4b6d0f6ab98f219fe  anc/formal/Erdos7/Hybrid.lean
7382df9ab68ecd8baf040d08089f68501700cb091b168cdb1dbb603c48da7516  anc/formal/Erdos7/OpenRuns.lean
dbf76b83f8bf58fea875efa044f5c791bc7cb655a9e8620e1a8a0d6204c340ae  anc/formal/Erdos7/ProductGates.lean
1feb45c300488d2d89e2cef9c7bb9a915d39046070eaf3084513364128addac5  anc/formal/Erdos7/ProxyCertificate.lean
97b22ffc264df036bd43510fb0ad460a7907f2753ae4305764b065e31c389fa8  anc/formal/Erdos7/Rank8Arithmetic.lean
308f99b3132ca45e0312816633809d04184bbd7c4f2bdf5d08ca5f297a5e228f  anc/formal/Erdos7/Rank8Certificate.lean
e81b8017541eaa0f548176a458346d69432440391e830221d4427992bb100b42  anc/formal/Erdos7/Rank8Cylinders.lean
993185e32b6df8315e5f0219d4e060e4feae990cafaf7cb9869f2ccf25ff96a2  anc/formal/Erdos7/RankedRearrangement.lean
850f191707b1044be1c6c64d1abe2f2a2f6a5dc6f9cbeae11b299a4f15e7a0e2  anc/formal/Erdos7/RunDominance.lean
66f35dfe1741580137d58888910fe48f8088e5a354d986a6412e3268ed8ef871  anc/formal/Erdos7/Runs.lean
1ac462e39fbf96839685d5242b24d26d10f6bb075adc66ebdb02c14ec6de2906  anc/formal/Erdos7/SixBlockCharge.lean
d027c8a2bf06803312b5b05e2f941a7c92f06f4ca2aff02df434dd8caca44980  anc/formal/Erdos7/SixBlockExpectations.lean
9550513c2c948c6e2e8eedf94c410245a715afad593ce44eb22a13121c1a3d37  anc/formal/Erdos7/SixBlockGates.lean
a2f56f41bb02b30f2a36619e486fee9099d323f8732e6688a1c25448eab0c1fb  anc/formal/Erdos7/SixBlockModel.lean
0006bc11fa89d185abf0762afcb1f908b26a1774a5037de04a62bce02da64e0a  anc/formal/Erdos7/SixBlockNoncover.lean
40913b61d6966c480eaec017e50d23638bc5c924010bae886e9c50df21776bd3  anc/formal/Erdos7/SixBlockReduction.lean
28d13560f1a13cea1e06dff58563443b41c2c36b4d541950af0e15144fcc6ecb  anc/formal/Erdos7/SixBlockTotal.lean
54eeadae8666c949dba0ff1b3bee564baf10b9aed874b805bf5285efda396da3  anc/formal/Erdos7/Supermodular.lean
14818401f722b8dd3a5dfab3fd4225dd7cfbe6bdda989511523f9e26e4111aa6  anc/formal/Erdos7/TreeSelection.lean
2226df38c228f429832ff34ac51bf5d26f25a51f078afc4107f7c617404b295d  anc/formal/Paper.lean
e2445e96ea60d2c4890edc4f3994025ef77efd29df20ea95f085ec08056a6b80  anc/formal/README.md
376a3daf667332b2a40270050b43bbd7f75e1de3fa304495aa2719732e2590f1  anc/formal/docs/API_INDEX.md
4f7c7a819b4fd759c2cc68eff8e2ef7b8be4fec8afe8b1d78df06857365f01a5  anc/formal/docs/BUILD_AND_TRUST.md
7dfaab1e3b19af97b5c1e90c75d7f1bfd48f16f22ab46e4f748a8cf275fb3ad6  anc/formal/docs/CHANGES.md
f0855d16b5d4aa8ac59fe7f88a684a3464886e82d78064f975bbc72430658157  anc/formal/docs/SEMANTICS.md
dab07c893be1fd8a3f798989f50d75cc6d11610f742dd9e99158b4d2eb4023a9  anc/formal/docs/THEOREM_MAP.md
507691ce3f07694fc8096c1b6d4c661eb4cf3da644e35d47edaff55ae7030b53  anc/formal/lake-manifest.json
ceb72d885db924a819f34d5d85b638d0384368b2f7f7f23f369dafd499eb4167  anc/formal/lakefile.toml
72681913b978b3f7c2f48229836771f736f6e97d833917726b2263afbc6108ed  anc/formal/lean-toolchain
4d034c777a469cd680d716f355aefcf0e850fb3c586a3b2788b696fc23931382  anc/scalar/FORMALIZATION.md
f37ed71f5fb80c4f8bd62590c6db7956ab5f65673585291dc2eb01ba24b55061  anc/scalar/METHOD_SCALING.md
ae1eeac39d6a1cf9e7209818f9ab06f3f21936cdfdf27f364e71cd1b1a121158  anc/scalar/README.md
c83b1be3c0e2ddcfcfb4ec6a80c9f94706fb4bd168e59c040c556da902318b47  anc/scalar/barrier_certificate.json
91ed64b04b6c5fb2ecdd5c383768cacf8999b19eb6b00b921694fe6e9a50e1e1  anc/scalar/check_lean_regeneration.py
e56345797f6a255dd28dec0e176683dd6a2453749a354ef2a81b24f6c9ba7fe2  anc/scalar/emit_lean_coverage.py
e83000e89e0aeeece42f31b0eb31f27abb89420423572e3b18c79e42cbe9fdca  anc/scalar/emit_lean_numerics.py
24297d764c5ae130be2e001b1bd1f9b6fffcff4ef2d2e6fb1eae90a6fb3f4ae9  anc/scalar/emit_seven_witness.py
e1792b4bdecd4624c70af164ba9cc75a2fa6a8428d46ae823594ba89916eddbd  anc/scalar/export_lean_candidates.py
78bd96e1aff9b4cd6f69b1337dca963c110f3f156b6ece45ee6e0fa7f2219026  anc/scalar/improved_rank8_certificate.json
5932ba293a3ac0ef8593d28de6d6683bf462db31747b8c0f1c3434dcc1eab4c2  anc/scalar/lean/Erdos7/CappedGain.lean
7f4541df6ec9f2ac5edaa6f3f6054b1d59a7c2ac47090a9fff121cc18973bc9c  anc/scalar/lean/Erdos7/CappedGainLattice.lean
cdcbb84f1f17aa62d639796ec4f405e186f9f287b9abe6273d09fccab3953166  anc/scalar/lean/Erdos7/CappedGainLift.lean
dc66abdfd02a97eadafce0a43779fac7f4b325e59bd0ef6b31f3c643565540d3  anc/scalar/lean/Erdos7/CappedGainScalar.lean
8821f4a1e642a005cd33e48cce345e4a8c8e31e77dc7a7d7e3f2b0a0fb0f44ce  anc/scalar/lean/Erdos7/Causal.lean
ad3e8702a076eb81fa1cfd5da10e0f0b5b95dce12a4052ebcb0f2208d0074637  anc/scalar/lean/Erdos7/FiniteProbability.lean
54eeadae8666c949dba0ff1b3bee564baf10b9aed874b805bf5285efda396da3  anc/scalar/lean/Erdos7/Supermodular.lean
94dd3e74ebea7da448fd4ccd05200792e38a433340731dfdf1648d0818055a1a  anc/scalar/lean/NOTICE.md
01307a124a86d0deca90593cdaf69358c3e555a2ec297ab31c1df1f146a905de  anc/scalar/lean/RankScaling.lean
ed5283831613c73a12ed9fcffa5ba37276230c5c46504331492b3ccbe786b4b8  anc/scalar/lean/RankScaling/Affine.lean
a8c788f43b63eabefd623f376c1c3fab8418d7ec22cc22dbfc9f684240ae1fd7  anc/scalar/lean/RankScaling/Arithmetic.lean
f4c721d3c751bce5bc3c0358eec7a39f49b3f90f16b74e5dd97ebab3e2457aa8  anc/scalar/lean/RankScaling/Audit.lean
0ccb87271c6e93d7ebd714aaeea590983a7a5e73ea4e9c9e61fa736f5b2257e4  anc/scalar/lean/RankScaling/Ceiling.lean
469d91304a0a3646e70877df0eeba66ec6de56580caf2352370ee4de0d969be7  anc/scalar/lean/RankScaling/Cell.lean
ea6de458ef24dd78ee74d2109b5b777f59387a640dcc6a3670a5b129a004614b  anc/scalar/lean/RankScaling/CheckerTests.lean
4f859829b476d49cc4c0d7e7378c2cc303d7893b79fb07b6e78cb0c222cc512f  anc/scalar/lean/RankScaling/Clearing.lean
00446860a99bc1c093ce1ea4d837b426f4c52b4d982be0aea2567550a93e19a6  anc/scalar/lean/RankScaling/Composition.lean
04cd4b86756f26af37171a814b2979b7290eed57642ab0bb3d5b7d62db1518ab  anc/scalar/lean/RankScaling/Consequences.lean
d6f99d76ba118b08339a8feb0afa095a5a246e9512e93c6025f336ee0664228d  anc/scalar/lean/RankScaling/ConvexTerminal.lean
6d81b1429847e0a59f9e6200a565884842c62ec474189f48109b0c9e3af5259a  anc/scalar/lean/RankScaling/Coverage.lean
a1a76c09e5975e4ab7b9a02a4c06bdfd07fc469c0709d7d31e687ff819bb7bde  anc/scalar/lean/RankScaling/ExactModel.lean
81da5802bff1bcf5a727593f601d86cd248ac0cecf79f6c16236b2d2d4241ea3  anc/scalar/lean/RankScaling/ExactTables.lean
f95b9c78e04bd4f921d22236ce4541648c17d75bb97234f44540b4e61a077e52  anc/scalar/lean/RankScaling/InfiniteConsequences.lean
1200dcfbdc4f99e2766f380a909dac2c3947b0c0d275187481c5db111a5a02a7  anc/scalar/lean/RankScaling/InfiniteContinuations.lean
10ec4ae4b0cd136675eb3af68ade79ed8ac3b18918e6ed61dba92d089b836e0c  anc/scalar/lean/RankScaling/InfiniteModel.lean
445f2b8fbfe32e7729a413c043d5e09e504bdb7f4eacc161ea30ac9fa700b0c4  anc/scalar/lean/RankScaling/InfiniteMonotonicity.lean
31d41d0b5d94a6a1b5afa182b5a25f847f37f37c8e8c21e0183e766e327a8327  anc/scalar/lean/RankScaling/InfiniteShaped.lean
e7502dd173054aa1cbdbf4d4bd7e176832af6dd72d84127d30042d5386c8d66d  anc/scalar/lean/RankScaling/LargerLists.lean
a96a54a3a6af16d1a87f370b3472b85b9d44febccc4e3ff3795ffec97ce8dec3  anc/scalar/lean/RankScaling/PrintAxioms.lean
ab0f8e55a2ee7c782817d83787707296a1954842e9f9eb1990ee622a62742477  anc/scalar/lean/RankScaling/PublishedBridge.lean
4818ffafa2c7b8a6186dc4bc5943d4efe1d5f9a369b7fb6427312ebbd8f8bab3  anc/scalar/lean/RankScaling/RealDominance.lean
74b14868d05afa45578a0315b51eb74ccf1b2b6deb01348c4902ebe629ea31c8  anc/scalar/lean/RankScaling/Scalar.lean
df8714a0f1855b19af7f361a068c13e2b9c1e0bfd97bf0f63cf6131861a11cc2  anc/scalar/lean/RankScaling/SevenWitness.lean
d2168b43a8cc6d72e3b78af251ec02d0fb8a5346a3fdbd0e5baf368a0a5f0a45  anc/scalar/lean/RankScaling/ShapedChains.lean
41a375c1e1592f52622ef959d1378a0be06a46ae67ae1c296f3e237608659f99  anc/scalar/lean/RankScaling/Soundness.lean
5e993a7f100dbcc55b976276df12ebd2d89b205fc6e7890f620cfc5b1ff984fa  anc/scalar/lean/RankScaling/TerminalChains.lean
8e35c91d492bd79fa8660a0540238c78d9a18d5db39c40f87b72f998d3644d3e  anc/scalar/lean/RankScaling/Threshold.lean
6f8d892ae8302fa1dde8f67b06bca6af09bd81043d1d63cc3cacb9c2cb9c32c2  anc/scalar/lean/RankScaling/ThresholdClipping.lean
6dedf61ddf3ca54104398f9f077f247bc6ac45ebf52fc329aada690c40b499fb  anc/scalar/lean/RankScaling/UpperCertificates.lean
f847604ced20533621926f164e34d41c44f3fe338d0d11ae1dab8e6f938ead53  anc/scalar/lean/ScalingDominance.lean
f9b5021bfa975fe94dd592bb67bdd28f3962b673b492fca1152f79c2dd3e7370  anc/scalar/lean/lake-manifest.json
21890f51387762dd7519cfc9f84da5e992bb34f84602758cc60faae0fdf293fe  anc/scalar/lean/lakefile.toml
72681913b978b3f7c2f48229836771f736f6e97d833917726b2263afbc6108ed  anc/scalar/lean/lean-toolchain
9ebf20a0a5510959ece4e546da6af2207b0ae1d8c911773c6a7a0e360459258d  anc/scalar/lean_candidates/coverage_modules.json
f2372206004bfc3a8da9e90a5294fda3d1b49b36fcff8d8a20675fe52374912a  anc/scalar/lean_candidates/final_lean_verification.json
c61ffe4fea404a91d6aca00a2fa59ce55f3d0ae11e40d5a7de96369a33758fbc  anc/scalar/lean_candidates/final_logs/axioms.log
582d5464edf4feeec39c9c5ece676c67db7b9957c4d838d7b2cb5b4991408482  anc/scalar/lean_candidates/final_logs/closed_theorems.log
c6a1639d7279c904ebf2b691857b716f7719f836a916e41d0273a4c254d25208  anc/scalar/lean_candidates/kernel_replay.json
601a6a120df6019f769f80ec0a070d3cc70561aca57a18f739fec39b7bec15b6  anc/scalar/lean_candidates/manifest.json
3095127a7bfb2912437493dbd3f6f6116ae43803398a4f75bc02e0927a705824  anc/scalar/lean_candidates/numerical_modules.json
2842bf80c758088465345517562e74cadf2ac58dd988d04078c23d727ae23de1  anc/scalar/lean_candidates/regeneration_verification.json
9a5e63c2507b201f26586c78d553d2cb73f2b43e07298f76a7e0fcdbff5f7129  anc/scalar/lean_candidates/runtime_verification.json
a03ee4761c4326972f9394a1e0d9a51e0b8f81116b58777944dcf50fc922b701  anc/scalar/lean_candidates/source_audit.json
d2ae7b7a995cbc42216ce7e155c40d1d3e6b9828245ec55692e2640f953b5016  anc/scalar/replay_lean_final.py
d37d0d6afb735f21f86186948434261e8d11a8717b62ed1f9a03a4e8c55568f3  anc/scalar/replay_lean_numerics.py
2a76df4b2077951edbe54f5a6ba6f4e388ca831e445503e1d80f624d384f11e2  anc/scalar/verify_improved_rank8.py
b28751b877c2fb45c5af9e1a27505e051d635db9e79a7682d6a36ed1165ffaf2  anc/scalar/verify_lean_runtime.py
6f1cc51642b8d45f02b2d6dccb85ba9093ce34cb82a6b180a713fb840abd80c8  anc/scalar/verify_scaling_barrier.py
290210dce92eb58c143c66b3a3222ed130058fda90adefde94e3e70206ca62f6  main.tex
