d225b9edf9a3f3cfd893873841c7f96656dcf3d836ddf5d899fd2d11403f8042  .gitignore
a1b92b014dce27fbadf6670244f12e40de0b3c01c682a72103e15ea719a9219b  Audit.lean
309309c41214ad99c209b069934907a87a7b31c40e5bc4f66d15e5ae01e69dc4  BFPP.lean
ebe412255c6ad8bead78b98b5b565bbc54d77e6929ba4fcda0010851781c52e6  BFPP/Analysis.lean
33f1affbc3e712b8415ff268c41af02a8cc30237e14c5d143b5beea614daf713  BFPP/BallOrderGeometry.lean
9945ca341377638886cb9c0cdb08b36e5be526e0d6528477a3df552066c07be8  BFPP/BallScaling.lean
9aec82ae26fe68648266dbbdbd4609c2cfa9928a08ef21a762756fba17be7b42  BFPP/BooleanGap.lean
60dc113f810636018ccefb076d1a2f8311da85de29801ac38a29892be2526381  BFPP/BoundedFamilies.lean
6cfc358467fb3604256803785efb852ebd87933d45ba251bd2187427a0df3a54  BFPP/C0Profiles.lean
b979bec520807a39f2280cf6cced425d306e4fd26947c10377943f3246a4d125  BFPP/Center.lean
cfe7d7bea9bb28bd1811838b624a66929b0c35bff9bef2e2d234de79487ceabd  BFPP/CenteredSynthesis.lean
712a1f7188af13feb2b1b2b3514890cc97a9a98936450b71d217ea4c4c6bb1b7  BFPP/ChainCompleteness.lean
2e710ce68fef433fa52c16a259c4f0548c1674836490db80592779c0702a854d  BFPP/Characterization.lean
3c6a7e00f064cdf9eb1e58ff7bed8d96828088c27af371f3a8dd1f223b3639e7  BFPP/ClopenCompleteness.lean
ddfff03e4515db66d5d8409b296f4aad506f98c7bc3e689962f69409113fc5e7  BFPP/ClopenPairs.lean
7230405cd9e0813918b4b65d58dfe647d82974d40be40e5e303ccae55ebef234  BFPP/CofinalReindexing.lean
6a0378b21863a1f0c2ff7790b3625306738242d0b1c99275b3dda5ed3f7d190d  BFPP/CofinalSequences.lean
4fb2ebf1235771fda1c64ac2e1f6dbe0af485277aa0a213849105238eaf8c01e  BFPP/ComplexBall.lean
5e04402a7b99f0db7dd9bd21c502e37c9cecbf953df2ac47fe35cc9030d954ac  BFPP/ContinuousBall.lean
1380d465309cf83771f0aede1b827df1776b1de3ee87c32cb9db2d1eadf5563a  BFPP/ConvexIntegral.lean
4ce10cb1dee1b098d3a85be01e3b5a04da6331991469b533c37d79a14c04f31e  BFPP/CountablePairs.lean
4a547d01bb8eb9b229e74b42b361aefa5b53efb776a5267fe88bf6338895642a  BFPP/Cozero.lean
aae427df2f2011694ec9d8b716b58333cae483e91fa50739e6ef5eb9ad2fedc2  BFPP/Deficits.lean
825f569e0cb7c6adbba47d1ec0c6fbd684f833467d0e8455c4aad9e865f6f492  BFPP/DelayPrefixBound.lean
a9815e82bfbaf904dccb0fab403bcc2ee49f6fcb0013caf447b96be95228e583  BFPP/DiscretePropagation.lean
a598e97e4c2a7cf6928b3f64506d91a1fa5b3d05b51e0cdb279945de3a4564ac  BFPP/EDSupremum.lean
2e9408a15aeba71b3dd749458d9bddb7ac035c6423a928b60606756a090efaba  BFPP/EncodedDomain.lean
affe122b916715053dc908f45024f7c6247aede611ab72aa123df115bbb14c97  BFPP/EncodedMaps.lean
781a33a3eafd4574c9bb7bc94c0b1c01adecff7aa565d066e6bb0159b074e821  BFPP/EncodedRecurrence.lean
ab93132623b0b99e34ba3d4896d861e5a60f6c90e69c97b76268c5deab2a99eb  BFPP/EncodedRules.lean
9833acd288f3305035432eaaf5c7e6387518db023c97ebf02ff570e778783f06  BFPP/EnvelopeOrder.lean
8f53391e1053d89c104cb7602d950af094e454fb7b4babc0e1c3324c3b000db0  BFPP/Envelopes.lean
102fd3eeaa9eb36c12f681dba7716141e855425d2ce64d23e8264d001e042d25  BFPP/ExtensionDelay.lean
4abb41ce495e6a6996825dee8c3b829815eb0b3486787e9be7658c3d4d5cb2a5  BFPP/Families.lean
b19b61409dae8f87623fab9aa2de23e9990330157ac68d9141a4b87b2346624d  BFPP/FiniteSynthesis.lean
7ed59d19869702c6c629977b861aabe49eb3d3498d42d380356e72f27d1f8a9d  BFPP/FSpaceNecessary.lean
973795736d31c0662c7dcef2fcfc06d4fa41c38c4ed25c987eacd3cdab3ba38e  BFPP/Hartogs.lean
330d2fee1ed86d64b5fb3f91395c63a04f5536deeab97f00ac1d15f28a357025  BFPP/IndexedGaps.lean
2e89cdac6024a90efd538220a2661a3ac9688192100683f4f19a2552e60990df  BFPP/Interleaving.lean
b5bc97e3365536ad04a664222b3ad9968be20b7badf83a2dc9bf09d35b95f428  BFPP/InterleavingEnvelopes.lean
bfcbb242d5c42ce4d91c37dd6f335507b7550d8d539dda8ad7bda21f7b857e0f  BFPP/InvariantIntervals.lean
e3f3f1ac11dbc61d95e8e52bbf5bc635080026831e9d0e3ca6c9ad4153a281e3  BFPP/LatticeFixedPoint.lean
3568fd11210abaf9a01e7188fb81fdc7d3f97f7b45004a95771479877005fdcc  BFPP/MainTransfinite.lean
380c602e31bc4883ad5a0f1ac9d4790381110bbd1baa93c23e9054e5a6c81549  BFPP/Necessity.lean
3349af31f7a58a33b10809df54341066ac0a117eb4ee0422e63802b1780a80d2  BFPP/NormalizedAppendix.lean
b423e541276177f329dd69ac0bb14736ac76c2b7147b4ec7843f7750b5aadda6  BFPP/OrdinalCofinality.lean
f50ff6ea7efb8f74228f2bf2572ff6178553fc5c9bbf8b97477071422da83c1e  BFPP/OrdinalIndex.lean
429704eaac2f0ce28969884362ff8001e38490ecdfe67f6fbebfedc2f6315cda  BFPP/OrdinalPairs.lean
92c7d09e5f50d8bc4cff08ace97fa2a14aac69b313a13b903fbd10fdc7ed1dac  BFPP/PointwisePrefixes.lean
411d0a7a971f5ab9b905c94108e215ce8a6a12baf2d1009709b6a13ebc30546d  BFPP/PointwiseSupremum.lean
87eb511efc9db8f8675b1a525c946282e7f213e118e718033cc10a3452f56cc3  BFPP/PositiveSynthesis.lean
fa42409fa53df8b8130bef227b25ca5a3ab7d7e6494271a7565b8e8735e8c724  BFPP/PrefixFactorization.lean
bf0bbe46fd2ba04505f1e57f3a71b19f4921a3819660e8f6eac86fb5991b3324  BFPP/ProfileExtension.lean
a914239e62b482d3e330e5307b94314ac2974eb2a3a40f24afdf0b368ae41bcb  BFPP/ProfileGeometry.lean
91bd9f191342dd9e91015b815fd17844467674087a14a169eef8660c43501b28  BFPP/ProfileRestriction.lean
ffe3bcd0882e812a6bb9bbdf14fe14278ec9e3229c66f8f8a9697eec3d654ab3  BFPP/Profiles.lean
c6e4141107dfc9ce835ae834fa23f3a2d7c38e52a106f2fc3a261b4a58735a4f  BFPP/Realization.lean
d5741f2450e90441d913f62f869c92278885b5a1a2a4fa22d8b862564bd760aa  BFPP/Regularization.lean
9ab58dee5662dd4534bbc91edaa5d4a96f6e1b5223181dab651401b81ba0a239  BFPP/RegularPairs.lean
840c5156e01dec6822e6f64113e75ba092148e9c191871a10d042fa9ef199c7d  BFPP/SaturatedChains.lean
6fcf3a2226945a5b65e804898d1bde9b46e698ff431237b264e67f54d7063bbc  BFPP/SignExtension.lean
9f988845b0968b53edb7f96f1e68b58e4d0c02c212f412fe0d1fb5cb48877ad7  BFPP/SignRealization.lean
8d95749ac7b13207ecce1ccd932f320a83e6bc3f9b483942f4363c14b6702899  BFPP/SignRecursion.lean
62e88722fa129d31e678b7a0b048466a232bf4c69ff5f89921e3f13e0c004aa1  BFPP/SignTermination.lean
bfb9cb76d9ed19185bcbfcc0ebe7f0d20358b1301aa027e3cb8fc3a32d15bdab  BFPP/StepAlgebra.lean
aa4be4ceb8391d99732842929ec1d3e68136131bf82e64d1f3e7ec3ef0613488  BFPP/StepFunctions.lean
837a0799b573cd57dcc3d668f29f26f8c916032ba2012f42a5b738e403240f53  BFPP/Suprema.lean
1f694395e413a0a524b1183e4e04b1ae62ef092f66417c0b80cea284f256198a  BFPP/SynthesisIntegral.lean
7028dff839c88c1eab199e254cc7119d6c2b9242940a793341dcd0fe6b80f326  BFPP/SynthesisMeasure.lean
899eb91429929f77f977a80747f9d24847dea7daba7ecd65a881ff0fd33bc9b8  BFPP/TerminalNormalization.lean
7629643edce36fa98cf3b9281f42568ec075655e6e001638063a6a060c1a618a  BFPP/TerminalSupremum.lean
d18e7715a4b32cb5f776c2641442e28ad6777b33fedaf5919921a42f080a96f2  BFPP/Transfer.lean
91f2967373016b2f74e707b34b57ef0c7c4a3be4438357c9d92ec8bb128b4295  BFPP/TransfinitePropagator.lean
9c6af6c5084400352c7c0230af4bad0e9cbacaf229df27a82050867ca33317e2  BFPP/TwoProfileGeometry.lean
1ffae0739416130144cc2739fcba3ba6b881cd02a364c9b79bfddfa332597b4a  BFPP/TwoProfiles.lean
bfd8c860377e2be775f0383ae90ea57918eb4c7018be64d68fb844bc85a7db1e  BFPP/TwoProfileStructure.lean
53eaa2f08049fd95c5cae946c4277d1120aa60e9c3fe9b1d419130a211942af9  build-final.log
69b1ca5483343b51fbdc0493049dde70b99e90ad579fc7c30d9904707f2544e7  COVERAGE.md
96af6ba0f90ed91e9459992bb39abfaa29595c0ce91646fdf0c89c4e47e8ca6d  lakefile.toml
8190e75a201741065fe508b28955dd64dd72d090babe5f70ce6848879d68ae88  lean-toolchain
175a659ec6dbf5122c39b570002050c998425d8f8f7ab7f358809d37e7253a28  README.md
473f7589af90fe1511e146960c10ddf301ec5f56bc70bebff00dfe1442bf505b  scripts/build-local.ps1
f20b7a998518f4a0781b51985aac7cc9c9956c4d4b836651e2ce355a5b264add  scripts/check-local.ps1
28128db2102f403a1788d48b5a256299a25f12eef8f11baa06c5c1c91e17ad0b  VALIDATION.md