# All paths relative to LEAN_PROJECT
# sha256	bytes	lines	in main local import closure	path
ecd7fb17ecf7308e54d72eea7a5c756198b9d5e6b5cdabf773fca9eed7f48335	564	10	False	AmbientLatticeBoundsAudit.lean
30d3f545bce051b3621a881ae7c374d9d98b37bb14d20ed2ae339668f49dbfed	24972	582	True	BanLat/Basic.lean
51e351f291a15a8d88d42f17f787dada806f5dccc6e39775173dbe3fde9d54dc	28251	628	True	BanLat/Disjoint.lean
9d2254f8c8dab409a223ffa01e7a66cf044278039c82f995c286ad2e38f65cd3	22655	521	True	BanLat/Dual.lean
313cc63220e11d1b44a792d1cfa88990a63d90e000b82484bdc80165005d1a4d	21813	504	True	BanLat/LLexpr.lean
50017cb69948b8e4059c65e502f1ec3f631ce7d92e5104343156e84f6aade33b	22142	483	True	BanLat/Normed.lean
1a38127619695e2862fb93408bc24272d19a02f72a09783daf32e81b922e2595	26230	609	True	BanLat/Operators/Hom.lean
a563efcec03e343455826da46e359b819a39a0b0e53de85d17fb76a6579842d2	8627	225	True	BanLat/Operators/OrderBounded.lean
ff39c2e000bdd315c914a68708d2fd3854a74accbe0ed5ec3901c331347dfe7d	14782	334	True	BanLat/Operators/Positive.lean
67f3f9dff27a45c5c3b914051a69c45b5af8c23efa1154ac33e8609af74828fb	1044	34	True	BanLat/Operators/Regular.lean
51846724ccfe2955e7ed2f584237c107e08356f2bdb2ec62ca5638090afab92b	58201	1365	True	BanLat/Operators/RieszKantorovich.lean
5e55e5876b0141ceeaa11d075b8048311eef9b5c2c314f8011e4c557f3696ff4	16988	371	True	BanLat/OrderComplete.lean
93ed97cca155d8bf0a69bed4cffe229e0cb9183a809d8088855f1ccf399fdd30	2472	61	True	BanLat/OrderUnit.lean
c6c50461b12c0243b9ebf8efef0a4ad8ffa44e85f0d99148e4257168921da5fa	12491	305	True	BanLat/RieszDec.lean
d2b215633f9ab3b5327e8648fa0674a281f3598ad565260b2f5c02312f6b4231	7784	211	True	BanLat/Substructures/Band/Basic.lean
fb0087e729830d65c7f668a28cb9273abf7d39d52b39c07122096843c46ae1c9	5600	147	True	BanLat/Substructures/Band/DisjointComplement.lean
6bad98d67759be2f88047dfaf9192864ce60bb7790e659eba1cd844ce152273d	20560	467	True	BanLat/Substructures/Band/Generated.lean
8a9f48e31362404d21f04fc4a43ed10de79e08ec5f37cf890132ae7ac48d8290	4123	124	True	BanLat/Substructures/Band/Lattice.lean
d7d5fa1abe3602a7d56333de5818d4c2c1aa232047e95b4bc756e63b78328779	17832	409	True	BanLat/Substructures/Band/PPP.lean
5400e8d1efbbfda77ccc00e0f8a00e93030960f9325ac5541044686b58469127	51891	1050	True	BanLat/Substructures/Band/Projection.lean
a2c95d09b57d04eb5ac12b20ae852d5e31ca35ed6437aefcccbc5a90bcd72c33	51545	1118	True	BanLat/Substructures/Ideal.lean
e2df596909a94e153be31e04957c4e218d2d763ceeb97a3fec016e18de8c3ea6	42813	951	True	BanLat/Substructures/Sublattice.lean
b1ec832beab67664c64222e7781acf3b4f5b3cd80bf8dbec11f53b353a191172	418	7	False	BasisBoundsAudit.lean
282e6cc9d1647988e0214e169672c56b1ad5fc0abb195cf341087863db123a18	282	8	False	BasisBoundsCheck.lean
542170589de08b05402d4f9e2570cd70169c5378efe5748ba3565352714ab7e1	3594	77	False	ComplementedSubspace.lean
b131350879249514eb6eb47b46cdafdbc8ad1e465483f32047ebd86ef2e72c9c	2155	46	False	ComplementedSubspace/ActualProjectionBidualDPR.lean
a3385b8565d37f4e49491bbd8cfdc1bff2cb42c3ad530690ca3ca7ea0e4cbd85	2047	43	True	ComplementedSubspace/ActualProjectionDPR.lean
9f7b62844c96bf17bc6cf7be1b3798aff60c52a3cd533995aa285a39ec50c1f8	2151	44	True	ComplementedSubspace/ActualProjectionDualDPR.lean
cf65a5aa2da2262f84695696283cda9f3b918215ce12fd777b2e0e70c355f347	3741	94	True	ComplementedSubspace/Ambient.lean
c43668cfe5263a64c711faef86de4372206b6b84f37a66515d3e9a38d865db1d	7404	175	True	ComplementedSubspace/AmbientBasis.lean
5f674f8cb28d0d1d36b8e720c19a947868605c04521122567b677747b3e6f209	4822	115	True	ComplementedSubspace/AmbientFiniteApproximation.lean
15a495e3b9e2d0cc724f267b8818d9e718119fbeb43ccb374c46975a533ba2ab	4768	125	True	ComplementedSubspace/AmbientLattice.lean
30fecdacb0b7f245923efc245bf369e56211664b1cdebe2d458e1346f8d16155	5257	111	True	ComplementedSubspace/AmbientProjection.lean
3879a418f8a2f6f6fde013b939695d88f46656b297ad4260d573178c53a123c3	2139	51	False	ComplementedSubspace/AmbientSchauder.lean
50191618fbda12052d9eed73e99850acc880bbf74423d89589e725dc0ea8bd82	1243	36	True	ComplementedSubspace/AmbientSeparable.lean
bcf3ad915f3defb4ff941c898b02ba9ce0395c1332fc40eae8db59013c58381a	1385	33	True	ComplementedSubspace/AmbientUniformConvex.lean
c047aa5f7c27973de4a07f8b3146bead52603dbb6cca9c6894828d9ddeebcbce	5137	112	False	ComplementedSubspace/BasisBounds.lean
c8521ad7ba31f01bf0c0a7634e9b4c5f5a9a65de600ae216374628b5f4c710ca	2658	60	True	ComplementedSubspace/BasisRestriction.lean
8a28498807724e83e59b714bfad51c191f405e4cadbc76bba54844bc378565a7	3202	72	True	ComplementedSubspace/BasisTransport.lean
b4d53b895cfabb37bd96cdcd90ce3c5796fd0e977a91513c6c7051877cb36af7	5379	112	False	ComplementedSubspace/ComplexAmbient.lean
bb39557df190b8f970dcfc7a6b3ed58ca80fdb7957fc1b0906bcb8182965fcbe	10939	223	False	ComplementedSubspace/ComplexAmbientSchauder.lean
ba3689e116cced5d2c40ca0823bcd549f9693929a19f1300c7c23d1a5aa71e88	960	22	False	ComplementedSubspace/ComplexCorollary.lean
621ef045c17dc3c26dda85c241e2dd5846233f87ab4c6a2d4282cf2abc8f6462	2312	47	False	ComplementedSubspace/ComplexCorollaryAssembly.lean
cb874e7ffb81312e608354f9a480da630c9b6a6925d489713825b6545459f046	98	3	False	ComplementedSubspace/ComplexCorollaryAudit.lean
17c6880f4a3b6dbf03428338354ac759b362a7c00d871c49d3bc36f27d7d7866	6937	127	False	ComplementedSubspace/ComplexFrameCoefficient.lean
d7625763107dc031fc00531d701110197245a971ef85ed4d3e5cd86a970f7e26	4660	97	False	ComplementedSubspace/ComplexFrameCoefficientRange.lean
25d9d67bbebe6e0707772e05d0eeda01e40fc851de9b7e85092c5382a333050c	7225	154	False	ComplementedSubspace/ComplexFrameProjection.lean
05bc816e8cd4090627918e60da48c497eb83511c03432f63320e21a7edbe973b	7561	156	False	ComplementedSubspace/ComplexFrameRealification.lean
0580204035bc2ae8ede703d7988c58b485bc36e6fd635d97790bc0713e833ba3	5654	110	False	ComplementedSubspace/ComplexProjectionEnergy.lean
16e855f4a09d8fd4efc8c52c412bcdf183468fc1d9d8b5312f41d4bc812b7948	5175	99	False	ComplementedSubspace/ComplexProjectionRealEquiv.lean
e7f51b27f5ad9812cc3fe10d01eebf85c6f1220529f7531b8256846bc649414e	8697	192	False	ComplementedSubspace/ComplexRealDPR.lean
752c8a1edcd070d8d476016317f634469cb517910806bbd631950a96df4549dd	590	9	False	ComplementedSubspace/ComplexRealDPRAudit.lean
e0aa95ebd0f414be5c305d4930327c9460d10d75ec4e4d4b4ecff4f39b1a1e97	5314	116	False	ComplementedSubspace/ComplexRecursiveProjection.lean
b4830bda1298b214d2bf817c40466ac6fd92cce1c53933e1623374d84b42699a	3906	85	False	ComplementedSubspace/ComplexReindexedFrameProjection.lean
50888e94422317ee745edb59b251a5268ab3bbb443eb8caf0b9c81c51388eeb6	8573	168	False	ComplementedSubspace/ComplexTensorProjection.lean
b8dd0e1b53e1da5078218af1bc03093dc7c44d618cdc3f3bc068eaa02598bf2a	5279	108	True	ComplementedSubspace/CorollaryStatement.lean
f2c1cd77e22f742ef21465dd646a440e3cc49ac2d52985d82e79d3f3e0f3df4d	3376	80	True	ComplementedSubspace/DPRIsomorphism.lean
0bfd5269c89cf507ce09dec97a573d364b426c636dd2068d9f1494c84cf3e140	2149	55	True	ComplementedSubspace/DPRObstruction.lean
47d7940cc1fb78fff4cacdefe7faf2abe1b1af72566cf7f6aa57ddad4e7abdb1	462	14	False	ComplementedSubspace/DPRPredicates.lean
fd61437d513847bfe98421764fe725bc8096d8cf0ca04a64c91d0dbb39b4305a	9304	211	True	ComplementedSubspace/DPRtoGL.lean
6317ffc9b98877a90d9b3bf21a9adaeb82ca5d8827865d89ff43efb0632d10ed	1211	32	True	ComplementedSubspace/DenseContractions.lean
44689723e948fb2a5cbfcd99f62e2b1c706388646104cdea81182353aefd6cb6	1266	33	False	ComplementedSubspace/DenseContractionsScalar.lean
aeaccf496f84a3b414561604cbbb2982c296b97ae21d46d47aee2f4a60e808ea	2060	48	True	ComplementedSubspace/DiagonalFrameProduct.lean
8fc4567967139882a6fb87e30485765b3a93178a5d810a45615078b0e238ae0b	4293	90	True	ComplementedSubspace/DiagonalFrameSummand.lean
6c8c0840aa83c40b24423d1f8b2ba0978cdf526d4b13196d00f7d710d36a81de	7342	161	True	ComplementedSubspace/FiniteApproximation.lean
2947c81b8f0d42034fbd75562c3c83cb0b771564ef098433ab7d39e556b3913c	5104	106	True	ComplementedSubspace/FiniteBasisTraceBound.lean
4c748407a3541edd5c6b288ddac4ebd5f9f11b1953b811bb06bda183c00af45e	2205	53	True	ComplementedSubspace/FiniteBidual.lean
bcb31f688538327f3782ef71ed2efebb1b852ffeed7ffbfefc2ffe71d041c022	1577	33	False	ComplementedSubspace/FiniteBidualDPRLower.lean
c20708a337c386fb120a3a35a3190ccec5f5ecddaf17ad08e16f60aa966c76f1	2958	62	True	ComplementedSubspace/FiniteBlockDPRLower.lean
a8a14d7ee79cfcef0eef1e8b7dd090765b2c695e6a2c34ff257985ff24841abc	5139	92	True	ComplementedSubspace/FiniteBlockObstruction.lean
58ddbd8fd95a378b40badde0fd4ceb1dab4a6be8fea7265f5137f35188eb4378	4395	82	True	ComplementedSubspace/FiniteCoordinateSelection.lean
94742aea3304bd769f6b552e1ca0416d3328cdd6ee6e274031722159aec2f813	5540	127	True	ComplementedSubspace/FiniteCorrection.lean
5c2f69a2ec8729c8cc571d1a94a3a0f626cb06c0e6fb9d413158eadb5463c8a6	2347	54	True	ComplementedSubspace/FiniteCubeBound.lean
eb484185924f9d14a10afef2d70862873585ddc14b28a1b5456a9f95dc320398	2385	59	True	ComplementedSubspace/FiniteDualBasis.lean
6e4f469b111c39ae14b273169e93510c2dc9a67da34ec4a5932234ccf533bfe6	3343	69	True	ComplementedSubspace/FiniteDualDPRLower.lean
7e7a9c409ffe5d6d71a3159626dfce2368b08a1061ba7c6ade5b2edd11845467	2366	52	True	ComplementedSubspace/FiniteDualSuperspace.lean
379b3135d2ab8675e3b9240a3fd1cb6c8de424f4f67ac7d0c301ea55d5b93725	2504	63	True	ComplementedSubspace/FiniteFrame.lean
32bff88599b6fc6671342176eb0c2ab1e5adb33a8762e1e49a97d9c0bc0a9cfb	5895	115	True	ComplementedSubspace/FiniteHeadHilbert.lean
6fc8cfe97b6aeedeb36e64a835ab3040fc2b1430ea8be166169edbe9147ef531	2986	73	True	ComplementedSubspace/FiniteHilbertAverage.lean
f0fd206cbc042906351617c036d6a20a8120426f1d01341ec0a543d1308cfd9c	1152	19	False	ComplementedSubspace/FiniteHilbertWitnessAudit.lean
d3504078f5ad9966735841a01a97e509566673abc9b8842606ede7e763a6a309	10468	216	True	ComplementedSubspace/FiniteLpGeometry.lean
23b4e1a891e849f4b178b0fb07b43adf75c3fb9f24a7792fb85db4c48ab89fd8	5180	98	True	ComplementedSubspace/FiniteOverlapBasisColumns.lean
0f11567d750cb9c3f5d2802bc6a29b72ceb85611d13a1340689aebe55477027a	4152	76	True	ComplementedSubspace/FiniteOverlapBound.lean
98236aa39ec4de97587f365a4eaa857c9cef06f0857625189de8885406c33a40	2154	43	True	ComplementedSubspace/FiniteOverlapConclusion.lean
879da90d3515e12c823da4647517bab6542316b316dde4daacf0edde27f8e380	1574	35	True	ComplementedSubspace/FiniteOverlapDualScale.lean
f9cfd7b0d164e73f5e1de02ce03003087054b9b70c62238cbd7b69eff22df402	6484	122	True	ComplementedSubspace/FiniteOverlapGoodSecond.lean
a816942918033a1d448fa102dd168c65a0dab68fc7645cd4d83899a438638af4	5524	108	True	ComplementedSubspace/FiniteOverlapLp.lean
6d6bafa7eb67b68309f4817542bf625334bb6c22667dba964c0350dd5bc0fed0	4181	88	True	ComplementedSubspace/FiniteOverlapMatrixNorms.lean
b153ccc3a4e51b5f8689b02aaeeb9828fba6ac59f29a30f27936b4fd621f5b26	3682	81	True	ComplementedSubspace/FiniteOverlapMoments.lean
5c1c86fc03e56139cbaf6f5cafa764b07bf1c534938153ad8bb7241c19d96c07	7976	142	True	ComplementedSubspace/FiniteOverlapObstruction.lean
2b19be87a99d4b1ac528c80cf9beb8a40072cdf116d647d406cd4b5d9126409f	5861	116	True	ComplementedSubspace/FiniteOverlapRandomization.lean
a60c1c2c544051b57cdc3a55652f26b0b38f1fc213cf859708408b32b6c78769	12773	266	True	ComplementedSubspace/FiniteOverlapScale.lean
75a3de594a5cad76aeed7978a857e51b2d84c6ed4dc7f75b8a3aebb7c5c864d3	754	12	False	ComplementedSubspace/FiniteOverlapScaleAudit.lean
6f51f4cbf868e4e3bf26a13fb8a0557086fbdbe92baa692e850fd75dd75ec3e7	9043	165	True	ComplementedSubspace/FiniteOverlapUpper.lean
5b90bd768ea730909132ac9ea0916409ec5346fcf012290f7e36e771a724ed49	444	8	False	ComplementedSubspace/FiniteParameterAudit.lean
c28ac1eead96655022591993083ffa1a55e8b3ae8ecc5331afeb83ba265e5692	5383	123	True	ComplementedSubspace/FiniteParameterBounds.lean
3eb14759310d2d9d44a5fc3cad4f3c34ad1defc50deb787d7a397bf4eabb8dc1	11369	258	True	ComplementedSubspace/FiniteParameterGap.lean
efe6e44207e493b4a4f96256d8ba6b649acb308acf839d56dbf958bc4f209276	1842	35	True	ComplementedSubspace/FiniteProductObstruction.lean
2809bca2d08a5a4497b447116651a83fc894eff2c8d365d5ffa7b4f686d1ac4f	9057	192	True	ComplementedSubspace/FiniteProjectionTrace.lean
bf66a07267b955e5f27e7044957b9a2f7e7271a0acd1d783c545618a2466f9c3	5423	101	True	ComplementedSubspace/FiniteSelectedHilbertModel.lean
5e92e926e345daec8931dab8ac21c8ed37ab8d1ba50cd6034b0f3042fbd57245	4137	95	True	ComplementedSubspace/FiniteSelectionCoordinates.lean
5e5d5c44960df9c65ef60d3b8575cc62cd9b3a984473e0579cd23512862b515d	10082	229	True	ComplementedSubspace/FiniteSigns.lean
a921891bdb41b6dd57c95947b4e53886ca57a0ab4b9ba2c3798fec8b59baf7b2	2418	53	True	ComplementedSubspace/FiniteSignsComplex.lean
11629847ce860774366c41c37883126d52c02e4a0e2668a2ed26a5cd464598d0	5593	108	True	ComplementedSubspace/FiniteSignsInterpolation.lean
4156ce51dbb60a5270821b30de9c66aab560fb026105fa99e796d9d20112f340	3008	83	True	ComplementedSubspace/FiniteSuperspaceSplitting.lean
157741f05ccc26cb8733884edfe8f7a027225bd126c1a5df93a8fa2514647c15	6291	124	True	ComplementedSubspace/FiniteTraceOverlap.lean
8654e1c06f1e452acdceaf2dfc57a6711156515bd73d548b2dfa1e185ddb5e70	3126	71	True	ComplementedSubspace/FiniteTraceSelection.lean
70ca3d68efc108d054db4f2bba99a3d53f9184cf8bb0b57abacc7b8046163d46	4085	92	True	ComplementedSubspace/FrameCoefficient.lean
25beaa201d06a38d2ee2f36a2ea9232e3f6843a9146589f356cdb78cb387a330	4152	93	True	ComplementedSubspace/FrameCoefficientHilbert.lean
25f6b0cd76a139583221fc2110a08dff83ecb137d640fb1b086ddb3d840d7b39	2357	48	True	ComplementedSubspace/FrameCoefficientNorm.lean
a0b417aa6b29cd50ece756e906c750305221ff100c37a4ca84cb5059926b38c4	2042	51	True	ComplementedSubspace/FrameCoefficientRange.lean
66aa1ab2eeda8cb80adce4cc9999432780b1382be1c9217da3608c419a3dc87d	2538	53	True	ComplementedSubspace/FrameCoefficientReindexedRange.lean
c99edfd191546d4bc79d93f38a69df1db9abbb5abc0c145c044fc60a977a4450	9891	219	True	ComplementedSubspace/FrameProjectionNorm.lean
328058fd2da0542b217b62d7f993ab32596eda6db83b7f56d04dda601d919c03	4681	109	True	ComplementedSubspace/FrameProjectionRange.lean
1b86a0368a10ba5859e478280e5535063ddcbf2a0ea7fdc276fe9d16e209f83d	4323	101	True	ComplementedSubspace/GLDualRetraction.lean
73b7e706f0223634c3aac87d8c9d8bd4127206fde355d047f58490b537bb36d3	9551	206	True	ComplementedSubspace/GLRetraction.lean
cd6dae85d346023abee70c67bd72b30bc1226d227433f2e01d307d1724f10dc5	4882	117	True	ComplementedSubspace/HilbertComplement.lean
25f47937d625f6b360dbbf0ff9eb6a33372aa39a56caae8cc4ef261fbf162bf1	11058	237	True	ComplementedSubspace/HilbertOverlap.lean
e5f209811f9eff3ee3f3ecacccb0e77abed6dc30ff31c2411a5bea15d16b2423	1569	34	True	ComplementedSubspace/HilbertTraceTransfer.lean
0acddd6eb16a34d8346a5f0cacb9df65da66481c1d5a5e7e0511f289a1b7a9bd	1945	38	True	ComplementedSubspace/InfiniteFrameObstruction.lean
0488f204843bfdca70793d677b2dcc4884ffe41a60339ee637d0d000449db6f9	3320	67	False	ComplementedSubspace/IsometricProductDPRLower.lean
f2572af0e42e05ec5e9cc86ea70adffe937b050e09f50a7a17572d64c9b6c1b6	3332	88	True	ComplementedSubspace/IsometricProductSplitting.lean
ac38f607840630954fca0dcaac3301940bffaf4f6285e1a0bc03aacf7b0ea336	2261	54	True	ComplementedSubspace/LatticeApproximation.lean
37e06710226e0d05f30d653bc265042f639aa45218fc603f316196a2482307c6	3908	87	True	ComplementedSubspace/LatticeBasis.lean
81762cd605274f44c248531445c850c7f27e7b78e1c88e5e9f073674ddd84731	1860	47	True	ComplementedSubspace/LatticeNonisomorphism.lean
55ec903b3a24186808f817d0e32d920cff93c24bb85e046e3a225195c2be64cd	18057	403	True	ComplementedSubspace/LatticeSpectral.lean
16c8f562a11de1e24c58690321777ecb91429a9a9073c154ee1ea653a98da085	9259	214	True	ComplementedSubspace/LocalHilbert.lean
dfc5b6f3f27c5119af3ccc435d5c24f6827d16c123fcb81c56d868a6eeb45bc5	1507	26	False	ComplementedSubspace/LocalHilbertAudit.lean
64f421fe7ef04fd95dece8ad2c9b3f63b723f22bd7e60c11891c5e8b7d20fc3e	12650	284	True	ComplementedSubspace/LocalHilbertCompactness.lean
cb6da170830cb2c51267d2d0ae29f6bbf43893b66e82950a16918a374f0bdd1e	5735	134	True	ComplementedSubspace/LocalHilbertCoordinates.lean
be507a3181bc331ee337e22b69ed0a5166a0dd78b528cf22ffd4b852238f941f	6424	132	True	ComplementedSubspace/LocalHilbertDual.lean
fce82710e2ec9c4ff98b920aee9194156ff35878f378ba0ac55546e6ac452dc0	1098	25	False	ComplementedSubspace/LocalHilbertDualTop.lean
402cae0847716b8d13345a237d0c989d5f683c6e432d16f0b313544f9a4719e7	197	4	False	ComplementedSubspace/LocalHilbertDualTopAudit.lean
873d9a7c348c34ccee16fe66300f55eeb76c0dafaa6a57e017186e649f639188	3466	74	True	ComplementedSubspace/LocalHilbertEmbeddedRenorm.lean
006bbe89c5d7df3fda5b2385bf04806665aa2ec47ef5e372acfa2d9a59afeda3	4662	101	True	ComplementedSubspace/LocalHilbertFactorization.lean
833de74e88964c3d46da39d56487db4a15409f4f59db50a0d5708613b3724363	6264	125	True	ComplementedSubspace/LocalHilbertHeadRenorm.lean
5a19771c61d2c83bc171c19c24d36128b40a9c50b1792e00162de9f2cf7d6425	6489	134	True	ComplementedSubspace/LocalHilbertProjection.lean
b228acf4ebc9580be43a0a87a1cc1e27fc05431c5218fa7f39be2cb9207c8925	1158	26	True	ComplementedSubspace/LocalHilbertProperty.lean
98ed8ff7cd6228438d765be36d58b0a4d368a4e3f8819adc39f288682d4ea482	8115	157	True	ComplementedSubspace/LocalHilbertQuotient.lean
8eed3ef6c2e8ac32a20ba118ec19bf3ac0c9600a833899f317171089cfef47b2	1013	15	False	ComplementedSubspace/LocalHilbertQuotientAudit.lean
f1d73206e02676f82e59f1c0c2607a19e44717b2c35176720f0274edf3809146	3698	71	True	ComplementedSubspace/LocalHilbertRecursiveKernelDual.lean
d9a711e14c57f5f51e8ab0d59e8565e96dbcb6e9ef3d978bb3c7946740e883a9	986	22	False	ComplementedSubspace/LocalHilbertRecursiveQuotient.lean
33f2c71af9bef3545221e68053477588799f922de43ea930f75971e1e5e5644d	9350	195	True	ComplementedSubspace/LocalHilbertSum.lean
b8b9d994b5981c951b5e3bbd3b70694df36e50ec0eafefa826243ecc29ac49c4	13593	284	True	ComplementedSubspace/LocalHilbertSumDual.lean
35c6df1f513e10dabd05d102af49c089ec34445648d65d8142f9d26a7828e592	2029	49	True	ComplementedSubspace/LocalHilbertTransport.lean
3ca23f64e18fcc14e9ee4a2a535acb40305acd9edc2862b6101f897f7bb14857	16438	381	True	ComplementedSubspace/LocalUnconditional.lean
1845df35a6a98c0611213c4c6e8dc3ec5c09061a7123556ff25e9b2e0edcaa44	6528	140	True	ComplementedSubspace/LpHeadTail.lean
a776dfab72af942512150da9c0db55db30ac05c9ed6e940d21f98660ddbe1b34	6988	148	True	ComplementedSubspace/LpSubmodule.lean
a5ad7b44fa3d31b2caf86cfe1df7980799e2428e3dcb13696412e3a0e9d431a5	2546	58	False	ComplementedSubspace/LpSubmoduleScalar.lean
3e4804fee62e5dd9a4628f3e322b3b40a946f721fa83951b587ae713eaba937c	3610	74	True	ComplementedSubspace/LpTwoParallelogram.lean
5da989db4b1fff92a3526515308d09e7f9aacff96ef5842a558e3db6d9327d64	8910	168	True	ComplementedSubspace/LpTwoUniformConvex.lean
f219d389f0edfbb905126735b2bd90fd8083a5cf7ed17aa785ad53308a5cb465	3750	77	False	ComplementedSubspace/LpUniformEquiv.lean
aea063fb3a4feac48ca51eb9f2e5234221032d21a2a67f459f495a96233211f3	3143	89	True	ComplementedSubspace/NormSqSplitting.lean
f0f5be10a561733c77c8a4c54f2f2954fdd154f10d0ab31b51c1688efbca0116	7864	154	True	ComplementedSubspace/NormalizedHilbertSynthesis.lean
378a293532f31438920433805add44964399da5d0b8237cf562237ea3044d8d9	2633	69	False	ComplementedSubspace/Parameters.lean
883201e285b25218140363d24a6d5ae057908ae197f127cf686dc980b7a10734	5379	124	True	ComplementedSubspace/ProductFrame.lean
7a6a8a1988ef3d9bfaad74acaeb8b135eafb2219f631c0531167fc2ffb7caad3	1184	34	True	ComplementedSubspace/ProductFrameIndex.lean
230f65d3c7b8fb56e9a7aefc97667b21073d35aae94c89740736cd02d253772f	2748	60	True	ComplementedSubspace/ProductFrameLp.lean
cbf741b32f8185450e96af0bd516f9cc7aee6c2c671126fbb9c677e2d226ecd1	8570	190	True	ComplementedSubspace/ProductFrameMoments.lean
daa22a2952060f29e2be1bc4a5801d0dfd643a89b4baf00649367c9e8f1cbf14	10494	219	True	ComplementedSubspace/ProductFrameRowWitness.lean
28e17de55f8094bddf6b06286c09ec49a54db675ec01c7b5ab9c569a4da02009	5679	117	True	ComplementedSubspace/ProductFrameSignContraction.lean
63a21e262596c7cdc6b0832de2f7b56bedb784177f0084fb1df8dba9f349a5ce	6405	138	True	ComplementedSubspace/ProductFrameSignSample.lean
3a22dee4034e1f35e3cc2b199dc557fcd675c7b2414a39e1514ede3b05eb20be	7798	184	True	ComplementedSubspace/ProductFrameSymmetry.lean
ceb640e3af666b3912844befa09a6e6f9fa61e07e2ac852e099cf0220aeff377	6426	139	True	ComplementedSubspace/ProductFrameTrace.lean
dac30fd7fe2c091cdd7620c50a8725bd8f07b219743f3aff0f83f38d2212d026	7886	155	True	ComplementedSubspace/ProductFrameTraceBound.lean
8cbdf48735c7d0286e1e689903193b1ea23d13fe8f018c2db98bfd10ab16bcfa	2552	66	False	ComplementedSubspace/ProductFrameTranspose.lean
da712d68eb3a96c1dfc1e3cccea0c6ffbda604c35462ee91efdbd4f75121bd36	3481	81	True	ComplementedSubspace/ProductFrameWitness.lean
5a67cd437a813c7410514d01ecd8857355df557c14aff2214f1aedfefab92e24	1240	21	False	ComplementedSubspace/ProjectionAssemblyAudit.lean
360a3c53aaa91561097a4d9f52003c9ea1f8a1977f5887b97b855e65f007fdb8	2316	50	True	ComplementedSubspace/ProjectionCorollaries.lean
6e44903deac25ba95e259440c849e51717ec603f8535424d610a75c88a645ca2	4265	86	True	ComplementedSubspace/ProjectionOverlapLower.lean
5b57cfefd0652d7f9a9e9c9d3fc91fbcbe9ff19b6726d68adf6ac6eece240009	4456	99	True	ComplementedSubspace/ProjectionPerturbation.lean
fd347d414686f23890eea36e21a286dd7077c0eaa85ee36c9baee6f1dac78af5	4594	100	False	ComplementedSubspace/PureFrameDPR.lean
2c6e25d798adfba8ea576b5a781c5e2384c0cf7b8fd5481f5907e05a83f52c80	765	10	False	ComplementedSubspace/PureFrameDPRAudit.lean
ee81e17bfedc7726d9d0ad586d882c6affabd1cab63bde3fa71023c1c1a718dd	416	7	False	ComplementedSubspace/RealMainAudit.lean
095527a9d9f356f483ddc28b96c59fabbd781d2042f696d43ec0be1dc91759ee	2518	57	False	ComplementedSubspace/RealMainConsequences.lean
f9609adc151a23fdb9fb0f0bfc59e135ed5f9341d591b5e9e10aa21f8955128e	443	8	False	ComplementedSubspace/RealMainConsequencesAudit.lean
c08eb5568448a4908d5f90afd8da3ee5fdac8ee0e34e01824dc03ac6a3221917	1550	32	True	ComplementedSubspace/RealMainTheorem.lean
e4e786bac003a667d8edb34d9eefd89f90709c3be3373527470bcd3e52823d78	2556	53	False	ComplementedSubspace/RecursiveDiagonalBidualDPR.lean
f1c6dfb5e0ea4bf97af0c5ae66ea99e74059ccd5ef1b2584f2d144229cafdbd5	3472	74	True	ComplementedSubspace/RecursiveDiagonalDPR.lean
ba91acf6624716006ed51206585e29cd5a3e56d9709293830d87b565ea996956	2507	52	True	ComplementedSubspace/RecursiveDiagonalDualDPR.lean
daa62e75b85090c6cc1716ca8e24cc47710aac7cbe9931d4f8f9c9e926da1cd7	3562	70	True	ComplementedSubspace/RecursiveHeadHilbert.lean
b1eaa41d636df5c947a4802e817f0a0f21374008d3f4c1a4d8570bd4f1293942	2843	60	True	ComplementedSubspace/RecursiveKernelHilbert.lean
f8853a154ff22c5719c782f68031bafe8d5c84fd8724b53db5945fa9d35f7b5c	13500	305	True	ComplementedSubspace/RecursiveParameters.lean
2d25a94879b7289a7546b0031aedee168a66965ce932a39e6ef619f8083eca4c	417	7	False	ComplementedSubspace/RecursiveParametersAudit.lean
a6bd8d6ac7310f8083ac2e63472a330dd8ca4ae953506866b73cf465c554b516	9767	179	True	ComplementedSubspace/RecursiveProjection.lean
028c16f70a05efcb6db95137d0a1d2014523880f980cc88d51c3d333c5002901	2176	46	True	ComplementedSubspace/RecursiveTailHilbert.lean
500e79de37d725f26f55bae55b59a545bee1886614fb6ad1363721dbc97fcaa3	7919	166	True	ComplementedSubspace/ReindexedFrameProjection.lean
e8bc5f58a504b0360dac97e49cf7dc56fa08ea74ffd3699a3c1ac4ba7aa9cadf	5645	123	True	ComplementedSubspace/SchauderDPR.lean
e196841bc3ac504cd6e80acd6c23471f129e3941add191b55127e04569186b4f	5955	121	True	ComplementedSubspace/SelectedCoefficientHilbert.lean
1a7a9e86f799d387003baba65a544da78386af02ceef0e04180a4700d37f7d04	1936	42	False	ComplementedSubspace/SelectedFrameBasis.lean
8548ed455ac4675872d9aa5acc4b771a6ef5c61f911f15d13fe7ec6b76dd37c3	10879	225	True	ComplementedSubspace/SelectedHilbertReplacement.lean
138b176c395ca17fc9c440ce8d8df655269fc2d7ac9037285f7ace5fedeaca53	9590	191	True	ComplementedSubspace/SelectedProjectionSetup.lean
8eeb17225fd0da439e2530f8fa503d596e8bbe8b25024ef78400593dc87f6648	10985	240	True	ComplementedSubspace/TensorMoment.lean
e5f33e5a9bb60bdd5ec99cc09d719ee62c29e9f5ef3dc1dceec496b9f4faa5a7	9174	198	True	ComplementedSubspace/TensorProjection.lean
8bae1822f09c36532811144dfad0faefd1724ac184c0167745fae48f0af4cd97	2912	68	True	ComplementedSubspace/TheoremStatement.lean
af4c40800fe8c7aeefcc1f0da019743694ad886b5462bf542958d6d2415358cd	5811	120	True	ComplementedSubspace/UnconditionalHilbertSynthesis.lean
a56ce7c482e8eef564c3651d037e55db5ef20558db0b3f0f9be2c4fe682e92b9	410	7	False	ComplexAmbientAudit.lean
8b63d55b023f0b29b31fc6dcd395f783485a14be3f50011becc9e65064497f69	951	15	False	ComplexFrameRealificationAudit.lean
d13940877d0228fb6df94cf42c7613ffc73a5b3e40387875593e9edbfda44f60	563	9	False	ComplexProjectionAudit.lean
8e6b79ea4d316cb497f40272168f237d0eb9e03cff95958e5c193376d84d1408	918	11	False	ComplexRecursiveProjectionAudit.lean
74337ac29004a76c3ee8496fcf1e7fc39d9624f9d099f303b202fd6d545aa604	385	7	False	DPRtoGLAudit.lean
5460c4fd9fcdf719e15a54d7f9cd4fdbf1979e41e046e1f92d586c2db7842dfc	241	4	False	FiniteDualDPRLowerAudit.lean
8f4c8cebf97ce110aeea9fdc1d81cac2220bddcad1b722328346ff7f03d1d1b3	725	10	False	FiniteHeadHilbertAudit.lean
aee86e84137d817e672fc4ce372efa8b184e3959ecfd6f8c207a4a5d9dc93dd1	3095	50	False	FiniteObstructionAudit.lean
bdd5667dc0a8944eedb66c2a8ca8c96ac111eda85dc512b899d5b7681b9acfe7	216	4	False	FiniteSelectedHilbertModelAudit.lean
828b632a711e7dc8d009908d155fa8d6327f9260b5e47ff29a395f16a4416488	370	7	False	GLRetractionAudit.lean
9f6a325f5be251b3856c87e426a45c501912d17fed4203fb74f06b2b9cc9d8cd	376	7	False	HilbertComplementAudit.lean
5bca1ed29ec7b71074d177ea75edd058a4874d12fad4ba91914b91bd7de18e72	367	7	False	HilbertOverlapAudit.lean
4b901ca4122b4f9664086914ac26e7a7694855e14318af88d8b52d01c5bbca5b	429	7	False	LatticeApproximationAudit.lean
d48a6accc5d7bfb021fdbfdce2456323161b9e80eea0dbb4e6125cb8ff801899	357	6	False	LatticeNonisomorphismAudit.lean
8d86a4bc1ddcf86b735539c27aa1d4484ca7e9281e79ece1086de404eef9748d	344	5	False	LocalHilbertEmbeddedRenormAudit.lean
a0f1d129823ae79959a0db3f7e543c9fd290189fcb09316b8ab9f85f9e4573c0	403	8	False	LocalUnconditionalAudit.lean
6fc89bc0497c0a808a5ec653ee075cf42a572575f4ac7cc94b7c7afbee5216d0	393	7	False	LpUniformEquivAudit.lean
4819a6b830d5d35c955a1ff237387a68c7edaa14e93b21710c198113287a552c	4923	120	False	MainRealTheoremDefinitions.lean
28d39562ae38377baecfcce15bc7162f44abafc8bea2fb3350b0442ad3c91feb	4991	122	False	MainTheoremReview.lean
91009154c9c47c9934048bf7ebef702a50cc5f1e204b2db932cc697d122876f4	411	6	False	NormalizedHilbertSynthesisAudit.lean
d796058c4f9c1e8070f90c1b61b425521e556f5505749bfcf94827a63216d182	265	5	False	ProjectionCorollariesAudit.lean
da32277b0cb7c6cd0af03175d64766f244f602c223bff32fdbc2840d7d049e39	185	4	False	ProjectionPerturbationAudit.lean
9ce1e99a24296e72593ef5f7ecac4d76afb0b652235cc1bc4326f34a4671618f	1014	22	False	RealConstructionAudit.lean
e31c256b489de087fbf297fab01305a6377530b7aacde3f04643900d90c76a6b	431	6	False	RecursiveKernelHilbertAudit.lean
38892e7fd666f871f1e437542f07b3c57f4bdee3936aab5b3b7a2bb0be966210	421	7	False	SchauderDPRAudit.lean
62c646544bd4e7b3d442e38200aac997c7b4460aa8d801c2cc5abb70a5928145	442	6	False	SelectedCoefficientHilbertAudit.lean
c50019ae47ba8b38b35b5fc69ea290bb8ec0ff8994813aa6649a41c5e8272f6b	262	4	False	SelectedFrameBasisAudit.lean
ca72ce849f3ba2d57bb2642fc2e9eee18593412009cdd8603ca52f099b6a5062	458	8	False	SelectedHilbertReplacementAudit.lean
ca3b869e8a53785497d7da2bbd303ab74eaeb6c6e7761732bb62c32a30d3ab44	639	9	False	SelectedProjectionSetupAudit.lean
838692e00ea5d99494fbe9f2a0a82a033b2fd0fa49bcdd9a5446b0959aee15ed	1083	22	False	TensorMomentAudit.lean
0c4118800b1f75ce421a5971188bd5f61b81b30dbbaab5ff4d2ccaeae4b2c24f	1322	23	False	TrialAudit.lean
25fd7072add542713a48f5ea3c2185b059820ea930adb285a770fa7971f45f43	973	22	False	WholeProjectAudit.lean
91057e35ab1c7e8428019ea576aec22d383289c82062c56b73b861ad3c022ec6	4444	99	False	experiments/unverified/ProjectionPerturbationDraft.lean
da32277b0cb7c6cd0af03175d64766f244f602c223bff32fdbc2840d7d049e39	185	4	False	experiments/unverified/ProjectionPerturbationDraftAudit.lean
452913370a3c789e349e21525a7258879da254d35ea69c4f42dd7332fc2663c3	1093	24	False	verification/independent-audit-2026-09-05/MainIdentity.lean
d7cdde0d7041a8c6021b7dda99865b4c415612e072b26fe0e650241eb8e5652f	153	6	False	verification/independent-audit-2026-09-05/PrintAxioms.lean
795406e7f826673476d956b56fc6ac72707479ac5a0825a94076b466c8a91965	708	19	False	verification/independent-audit-2026-09-05/PrintDefinitions.lean
da19376e92f4136f1f3b37e784f227286350137c242edfb0a6c4f91b04499e00	10130	192	False	verification/independent-audit-2026-09-05/TraceDependencies.lean
