SamuelSchlesinger · Oct 25, 2026 · Oct 25, 2026 · Oct 25, 2026 · Oct 25, 2026 · Oct 25, 2026
diff --git a/Complexity/Computability/Circuit/Arithmetic/Waring.lean b/Complexity/Computability/Circuit/Arithmetic/Waring.lean
@@ -32,6 +32,7 @@ unrestricted arithmetic circuits. All computation premises are formal polynomial
 
 ## Main results
 
+* `Cslib.Circuits.Waring.four_pow_lt_mul_cost`: exponential lower bound on Waring term count.
 * `Cslib.Circuits.Waring.choose_le_card`, `Cslib.Circuits.Waring.centralBinom_le_card`:
   lower bounds for ordinary finite sums.
 * `Cslib.Circuits.Waring.choose_le_cost`, `Cslib.Circuits.Waring.centralBinom_le_cost`:

diff --git a/Complexity/Computability/Circuit/Arithmetic/Waring/Compilation.lean b/Complexity/Computability/Circuit/Arithmetic/Waring/Compilation.lean
@@ -38,6 +38,7 @@ the construction is asserted.
 
 ## Main results
 
+* `Cslib.Circuits.Waring.termMultiplicationCount_le`: binary powering multiplication bound.
 * `Cslib.Circuits.Waring.eval_compile`: all outputs agree under a semiring interpretation.
 * `Cslib.Circuits.Waring.polynomial_compile`: equality of formal polynomial outputs.
 * `Cslib.Circuits.Waring.cost_program_compile`: exact arbitrary weighted cost.

diff --git a/Complexity/Computability/Circuit/Boolean/BatchLookup.lean b/Complexity/Computability/Circuit/Boolean/BatchLookup.lean
@@ -37,6 +37,8 @@ include these constants; the polynomial gate bound does not certify constructor
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.batchLookupCircuit.eval_withPadding`: table values returned for
+  all requests.
 * `Cslib.Circuits.Boolean.eval_batchLookupCircuit`: arbitrary repeated queries are answered exactly.
 * `Cslib.Circuits.Boolean.batchLookupCircuit.size_withPadding`: exact total gate count.
 * `Cslib.Circuits.Boolean.size_batchLookupCircuit_le`: a bound linear in table size plus request

diff --git a/Complexity/Computability/Circuit/Boolean/Broadcast.lean b/Complexity/Computability/Circuit/Boolean/Broadcast.lean
@@ -39,6 +39,8 @@ The constructor is executable; its gate bounds do not certify the constructor's
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.broadcastCircuit.eval_values_eq_true_iff`,
+  `Cslib.Circuits.Boolean.eval_broadcastCircuit_value`: sorted destination values and shared scans.
 * `Cslib.BitString.propagate_sorted_tagged_eq_true_iff`: the propagated value at a destination
   is true precisely when a matching source has a true value.
 * `Cslib.Circuits.Boolean.eval_broadcastCircuit_header`: every header is preserved.

diff --git a/Complexity/Computability/Circuit/Boolean/CarryLookahead.lean b/Complexity/Computability/Circuit/Boolean/CarryLookahead.lean
@@ -53,6 +53,7 @@ linear-size prefix network. All gates, including constants and negations, count.
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.depth_carryLookahead_le_log`: logarithmic circuit depth bound.
 * `Cslib.Circuits.Boolean.val_eval_carryLookahead`: exact unsigned addition at every width.
 * `Cslib.Circuits.Boolean.depth_carryLookahead_le`, `size_carryLookahead`: depth at most
   `7 + 2 * clog 2 (w + 1)` and exactly `15*w + 2*(w+1) + 3*(w+1)*clog 2 (w+1)` gates.

diff --git a/Complexity/Computability/Circuit/Boolean/KeyedSort.lean b/Complexity/Computability/Circuit/Boolean/KeyedSort.lean
@@ -24,6 +24,7 @@ including duplicates and payload, are preserved; sorting need not be stable.
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.eval_keyedSortCircuit`: output records match the sorted enriched bodies.
 * `Cslib.Circuits.Boolean.keyedSortCircuit_perm`: preservation of complete records.
 * `Cslib.Circuits.Boolean.monotone_keyedSortCircuit` and
   `Cslib.Circuits.Boolean.antitone_keyedSortCircuit`: recomputed output keys are sorted.

diff --git a/Complexity/Computability/Circuit/Boolean/Routing.lean b/Complexity/Computability/Circuit/Boolean/Routing.lean
@@ -40,6 +40,14 @@ for batched lookup are separate clients.
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.routeCircuit.headers_perm`,
+  `Cslib.Circuits.Boolean.routeCircuit.value_eq_true_iff`: header preservation and
+  matching OR values of the matching-and-broadcast stage.
+* `Cslib.Circuits.Boolean.monotone_routeCircuit`,
+  `Cslib.Circuits.Boolean.eval_routeCircuit_header_of_rank`,
+  `Cslib.Circuits.Boolean.eval_routeCircuit_value_eq_true_iff_of_rank`: sorted restored headers and
+  fixed-rank destination values.
+* `Cslib.Circuits.Boolean.cost_program_routeCircuit`: additive cost of the two sorts and broadcast.
 * `Cslib.Circuits.Boolean.routeCircuit_headers_perm`: all headers are retained.
 * `Cslib.Circuits.Boolean.eval_routeCircuit_value_eq_true_iff`: destination OR semantics.
 * `Cslib.Circuits.Boolean.eval_routeCircuit_value_of_unique_source`: fixed-position copying.

diff --git a/Complexity/Computability/Circuit/Boolean/ShannonSynthesis.lean b/Complexity/Computability/Circuit/Boolean/ShannonSynthesis.lean
@@ -32,6 +32,7 @@ the resulting circuit's size; it does not certify the synthesizer's running time
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.ShannonSynthesis.bound_le`: gate ledger bound for the finite split.
 * `Cslib.Circuits.Boolean.ShannonSynthesis.computes_synthesize`: correctness of synthesis.
 * `Cslib.Circuits.Boolean.ShannonSynthesis.size_synthesize_le`: the finite `27 * 2 ^ n / n` bound.
 * `Cslib.Circuits.Boolean.ShannonSynthesis.exists_circuit`: the corresponding existence theorem.

diff --git a/Complexity/Computability/Circuit/Boolean/Sorting.lean b/Complexity/Computability/Circuit/Boolean/Sorting.lean
@@ -58,6 +58,7 @@ The circuit constructor is executable; the gate-count theorems do not certify it
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.cost_program_bitonicSortTraceCircuit`: exact cost of the traced sort.
 * `Cslib.Circuits.Boolean.eval_bitonicSortCircuit`: agreement with the generic algorithm.
 * `Cslib.Circuits.Boolean.eval_bitonicSortTraceCircuit`: exact trace and record semantics.
 * `Cslib.Circuits.Boolean.monotone_bitonicSortCircuit` and

diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold.lean
@@ -47,6 +47,8 @@ does not assert an algorithm for evaluating rationally encoded circuits.
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.WeightedThreshold.preserves_ofThreshold`: threshold translation preserves
+  Boolean semantics.
 * `Cslib.Circuits.Boolean.WeightedThreshold.eval_gate_eq`: the dense gate equation, with repeated
   wire coefficients aggregated.
 * `Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_transcript_eq`: the restricted transcript

diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Menus.lean
@@ -56,6 +56,8 @@ internal weights (`two_pow_lt_of_directionMenus_intWeight`, `two_pow_lt_of_direc
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.WeightedThreshold.cost_menuBlockDecomposition`: capacity cost factors
+  across directions.
 * `Cslib.Circuits.Boolean.WeightedThreshold.card_biasMenu_le_two_pow_gateSupport`: bounded internal
   fan-in `k` bounds `|biasMenu p gate|` by `2 ^ k`.
 * `Cslib.Circuits.Boolean.WeightedThreshold.card_biasMenu_le_one_add_sum_natAbs`,

diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/PendingBias.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/PendingBias.lean
@@ -56,6 +56,8 @@ forcing `(pendingBiasStates p k).card` to be at least the number of distinct row
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_inputSummary_eq`: equal input summaries
+  produce identical gate valuations.
 * `Cslib.Circuits.Boolean.WeightedThreshold.pendingBiasTrace_eq_pendingBias`,
   `Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_decide_pendingBiasTrace`: Theorem 6.1, exact
   pending-bias state simulation.

diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean
@@ -58,6 +58,10 @@ its gate transcript (`StrictMarginProgram.eval`):
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.existsUnique_ilpValid`:
+  unique valid ILP transcript.
+* `Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sum_inTranscriptCell_ite`:
+  disjoint-support indicator expansion recovering the output bit.
 * `Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inTranscriptCell_iff_eq_eval`,
   `.existsUnique_inTranscriptCell`: unambiguous transcript cell characterization and partition.
 * `Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inTranscriptCell_iff_dominance`,

diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean
@@ -60,6 +60,7 @@ enumerative coding for weight-bounded words (Theorem 4.3) is in
   `Cslib.Circuits.Boolean.WeightedThreshold.length_le_sum_choose_gateActivity_of_isChain`:
   alternating-run capacity bounds along `scalarScore w`.
 * `Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_card_attainableTranscripts_of_direction`,
+  `WeightedThreshold.two_pow_lt_mul_max_card_attainableTranscripts_of_direction`,
   `Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_sum_choose_of_direction`,
   `Cslib.Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_sum_choose_gateActivity_of_direction`:
   rectangle-free scalar activity bounds (Corollary 4.2).

diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/TranscriptTree.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/TranscriptTree.lean
@@ -39,6 +39,9 @@ This construction is semantic and noncomputable; no efficient compiler is assert
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.WeightedThreshold.gateComparison_eval_eq`,
+  `Cslib.Circuits.Boolean.WeightedThreshold.gateQuery_eval_eq`: earlier gate values suffice to
+  evaluate comparisons and queries.
 * `Cslib.Circuits.Boolean.WeightedThreshold.exists_linear_transcript_tree`: a transcript
   determines a tree of native linear threshold queries, independent of any coordinate split.
 * `Cslib.Circuits.Boolean.WeightedThreshold.exists_transcript_tree`: the corresponding

diff --git a/Complexity/Computability/Circuit/Cyclic.lean b/Complexity/Computability/Circuit/Cyclic.lean
@@ -39,6 +39,7 @@ Native acyclic circuits embed with exactly the same gate values, outputs and wei
 
 ## Main results
 
+* `Cslib.Circuits.CyclicCircuit.ecomplexityFrom_ne_top_iff`: finite cyclic complexity equivalence.
 * `Cslib.Circuits.Circuit.eval_toCyclic`, `Cslib.Circuits.Circuit.cost_toCyclic`: the native
   acyclic embedding preserves semantics and costs.
 * `Cslib.Circuits.CyclicCircuit.evalGates_le`: leastness among pre-fixed states.

diff --git a/Complexity/Computability/Circuit/Cyclic/Feedback.lean b/Complexity/Computability/Circuit/Cyclic/Feedback.lean
@@ -31,6 +31,7 @@ This construction does not assert a finite iteration bound.
 
 ## Main results
 
+* `Cslib.Circuits.Program.evalGates_feedback`: solved internal gates match ordinary evaluation.
 * `Cslib.Circuits.Program.cost_feedback`: feedback preserves every operation weight.
 * `Cslib.Circuits.Program.eval_feedback_fixed`: the outputs satisfy the update equations.
 * `Cslib.Circuits.Program.eval_feedback_le`: leastness among pre-fixed states.

diff --git a/Complexity/Computability/Circuit/Evaluation.lean b/Complexity/Computability/Circuit/Evaluation.lean
@@ -35,6 +35,8 @@ This module does not certify a runtime bound.
 
 ## Main results
 
+* `Cslib.Circuits.Program.trace_eq_traceImpl`: compiler replacement of `Program.trace` by
+  `Program.traceImpl`.
 * `Cslib.Circuits.Program.get_evalVector`: the stored values agree with `Program.eval`.
 * `Cslib.Circuits.Circuit.get_evalVector`: the stored outputs agree with `Circuit.eval`.
 * `Cslib.Circuits.Circuit.eval_eq_evalImpl`: proved compiler replacement for circuit evaluation.

diff --git a/Complexity/Computability/Circuit/Frontier/Nondeterministic.lean b/Complexity/Computability/Circuit/Frontier/Nondeterministic.lean
@@ -47,6 +47,8 @@ fan-in two `s > (L - ε) n` with `L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.
 
 ## Main results
 
+* `Cslib.Circuits.Frontier.eventually_two_sub_mul_lt_innerSize_of_nondeterministicDecides`:
+  unconditional (2 - ε)n frontier lower bound for nondeterministic circuits of fan-in two.
 * `Cslib.Circuits.Frontier.Compiler.accepted_hiddenNetwork`: exactness of the hidden network.
 * `Cslib.Circuits.Frontier.exists_graph_of_nondeterministicDecides`: the reduction theorem for
   nondeterministic circuits.

diff --git a/Complexity/Computability/Circuit/Fusion/Cyclic/Closure.lean b/Complexity/Computability/Circuit/Fusion/Cyclic/Closure.lean
@@ -33,6 +33,8 @@ Restriction to an arbitrary admissible class of semifilters does not supply the
 
 ## Main results
 
+* `Cslib.Circuits.Fusion.PairDerivation.mem_of_outside`: an outside point belongs to every set
+  derivable at its ambient value.
 * `Cslib.Circuits.Fusion.PairDerivation.le`: leastness among predicates closed under the rules.
 * `Cslib.Circuits.Fusion.PairCover.derives_empty_iff`: derivability characterizes the target.
 * `Cslib.Circuits.Fusion.PairCover.ofDerivesEmpty`: recover a cover from target-point derivations.

diff --git a/Complexity/Computability/Circuit/Fusion/Cyclic/Compiler.lean b/Complexity/Computability/Circuit/Fusion/Cyclic/Compiler.lean
@@ -45,6 +45,8 @@ the forward lower bound also allows restricted witness classes.
 
 ## Main results
 
+* `Cslib.Circuits.Fusion.PairClosureCompiler.eval_circuit`: the compiled circuit reconstructs
+  every listed pair value.
 * `Cslib.Circuits.Fusion.PairCover.eval_toCyclic`: the circuit's least solution is its target.
 * `Cslib.Circuits.Fusion.PairCover.cost_toCyclic`: its AND cost is exactly the pair-list length.
 * `Cslib.Circuits.Fusion.pairCoverComplexity_eq_cyclic_ecomplexityFrom`: unrestricted pair-cover

diff --git a/Complexity/Computability/Circuit/Fusion/Quadratic.lean b/Complexity/Computability/Circuit/Fusion/Quadratic.lean
@@ -38,6 +38,8 @@ through a union tree.
 
 ## Main results
 
+* `Cslib.Circuits.Fusion.PairClosureCompiler.stages_stable`: point pair state stabilizes within
+  the listed pair count.
 * `Cslib.Circuits.Fusion.PairClosureCompiler.readState_stages`: `t` rounds recover the closure.
 * `Cslib.Circuits.Fusion.PairCover.cost_toCircuit`: exactly `t²` AND gates.
 * `Cslib.Circuits.Fusion.PairCover.size_toCircuit_le`: at most `4 (t + 1)² (n + t + 1)` gates.

diff --git a/Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean b/Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean
@@ -47,6 +47,7 @@ encoding, and, following the original development, for the stages of the dense t
 
 ## Main results
 
+* `Rational.intBits_step_le`: bit-length bound on values computed in one stage.
 * `Rational.detRows_eq`: `detRows (rowsOf A) = A.det`.
 * `Rational.detRows_eq_det_ofRows`: on any list of rows, `detRows` is the determinant of the
   square matrix it denotes, of dimension the number of rows.

diff --git a/Complexity/Computability/Circuit/SourceComplexity.lean b/Complexity/Computability/Circuit/SourceComplexity.lean
@@ -39,6 +39,9 @@ not use Boyack's convention assigning zero to disconnected vertices.
 
 ## Main results
 
+* `Cslib.Circuits.Circuit.ComputesFrom.map`,
+  `Cslib.Circuits.Circuit.computesFrom_map_iff`:
+  homomorphism mapping, and reflection under injective homomorphisms, of `ComputesFrom`.
 * `Cslib.Circuits.ecomplexityFrom_le_iff`: every finite budget has a circuit witness.
 * `Cslib.Circuits.ecomplexityFrom_comp_le`: composition through an intermediate supplied family.
 * `Cslib.Circuits.ecomplexityFrom_map_le`: homomorphisms cannot increase source complexity;

diff --git a/...omputability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Bounds.lean b/...omputability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Bounds.lean
@@ -23,6 +23,8 @@ many vertices, and its local routines take only logarithmically many stored bits
 
 ## Main results
 
+* `Turing.MultiTapeNTM.ConfigurationGraph.reachable_lt_pow_of_runsInSpace`: polynomial ambient bound
+  on reachable configuration vertices.
 * `Turing.MultiTapeNTM.ConfigurationGraph.fits_of_runsInSpace_of_le`: every reachable view fits a
   large enough radix.
 * `Turing.MultiTapeNTM.ConfigurationGraph.fits_of_runsInSpace`: the logarithmic-space radix.

diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean
@@ -33,6 +33,7 @@ counting folds a counter directly instead of constructing the matching sublist.
 
 ## Main results
 
+* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.filter`: filtering by a polytime predicate.
 * `Turing.MultiTapeTM.ComputableTidilyInPolyTime.cons`, `.listAppend`, `.map`, `.flatten`:
   constructing lists.
 * `Turing.MultiTapeTM.ComputableTidilyInPolyTime.cons'`, `.listAppend'`: composition rules

diff --git a/...exity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.lean b/...exity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.lean
@@ -24,6 +24,7 @@ are enormous, so the certificate makes no claim of practical execution.
 
 ## Main results
 
+* `Cslib.RotationMap.TowerTable.polytime_contract`: slot contraction runs in polynomial time.
 * `Cslib.RotationMap.TowerTable.polytime_rotateFamily`: the generic numbered-base family.
 * `Cslib.RotationMap.polytime_arithmeticExpanderRotate`: the concrete arithmetic family.
 

diff --git a/...lexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Tower.lean b/...lexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Tower.lean
@@ -22,6 +22,8 @@ unary neighbor, finite return label and framing. Fixed base rotations use finite
 
 ## Main results
 
+* `Cslib.RotationMap.TowerTable.polytime_next`,
+  `Cslib.RotationMap.TowerTable.polytime_nextRow`: constructing next level and rows in polytime.
 * `Cslib.RotationMap.TowerTable.polytime_build`: a uniform certificate for the complete table.
 * `Cslib.RotationMap.TowerTable.polytime_lookup`: read both components of a stored rotation.
 * `Cslib.RotationMap.TowerTable.length_encoding_le`: bound all rows and encoded entries.

diff --git a/...y/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable.lean b/...y/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable.lean
@@ -30,6 +30,9 @@ in `Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Towe
 
 ## Main results
 
+* `Cslib.RotationMap.TowerTable.Valid.lookup_lt`,
+  `Cslib.RotationMap.TowerTable.lookup_iterate_numbered`: neighbor range preservation and numbered
+  tower agreement.
 * `Cslib.RotationMap.TowerTable.valid_iterate`: every stored neighbor remains in range.
 * `Cslib.RotationMap.TowerTable.lookup_build`: exact agreement with the numbered tower.
 

diff --git a/...tability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean b/...tability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean
@@ -28,6 +28,8 @@ names, including its return label. Polynomial machine certificates are supplied
 
 ## Main results
 
+* `Cslib.RotationMap.TowerTable.contract_eq`: contracted table rotations agree with
+  quotient/remainder contraction of the graph (`contractFin`).
 * `Cslib.RotationMap.TowerTable.rotateFamily_eq`: exact rotation and return-label agreement.
 * `Cslib.RotationMap.arithmeticExpanderRotate_eq`: the concrete instance realizes the same family.
 

diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Machine/Equivalence.lean b/Complexity/Computability/Machines/Turing/MultiTape/Machine/Equivalence.lean
@@ -24,6 +24,7 @@ and stuck configurations; there is no clock rescaling or simulation overhead.
 * `Turing.MultiTapeMachine.Config.emptyOracleEquiv`: remove empty communication state.
 * `Turing.MultiTapeTM.toMachine`, `Turing.MultiTapeNTM.toMachine`: embed upstream machines.
 * `Turing.MultiTapeMachine.toTM`, `Turing.MultiTapeMachine.toNTM`: recover upstream machines.
+* `Turing.MultiTapeMachine.tmEquiv`: equivalence with upstream's deterministic machine type.
 
 ## Main results
 

diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Composition.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Composition.lean
@@ -27,6 +27,8 @@ separate blank work tapes. Preparation costs the intermediate word length plus f
 
 ## Main results
 
+* `Turing.MultiTapePTM.eval_runClosedConfigFrom_comp`: configuration distribution preservation and
+  time bounds for composition.
 * `Turing.MultiTapePTM.eval_comp`: the compiled output distribution is monadic composition.
 
 ## References

diff --git a/Complexity/Computability/Machines/Turing/MultiTape/SingleTape.lean b/Complexity/Computability/Machines/Turing/MultiTape/SingleTape.lean
@@ -39,6 +39,8 @@ phases:
 
 ## Main results
 
+* `Turing.MultiTapeTM.computesInTimeAndSpace_ofTM0`: simulation of Mathlib TM0 machines in
+  linear time and space overhead.
 * `Turing.MultiTapeTM.computesInTimeAndSpace_ofSingleTapeTM`: if `tm.OutputsWithinTime x y t`, then
   `ofSingleTapeTM tm` computes `y` from `x` in `2 * x.length + 4 + (t + (y.length + 1))` steps
   (and in `3 * x.length + 2 * t + 6` steps).

diff --git a/Complexity/Computability/Probabilistic/LinearHash.lean b/Complexity/Computability/Probabilistic/LinearHash.lean
@@ -25,7 +25,9 @@ The full extractor charges sampling, hashing and copying its complete public see
 
 ## Main results
 
-* `Cslib.BitString.LinearHash.computableInPolyTime_wordHash`: deterministic hashing.
+* `Cslib.BitString.LinearHash.computableInPolyTime_wordHash`,
+  `Cslib.BitString.LinearHash.computableTidilyInPolyTime_wordHash`: deterministic hashing and its
+  tidy `fun_prop` variant.
 * `Cslib.BitString.LinearHash.isPPTOn_extract`: the complete seeded sampler.
 
 ## References

diff --git a/Complexity/Computability/Probabilistic/PPT/Capture.lean b/Complexity/Computability/Probabilistic/PPT/Capture.lean
@@ -24,6 +24,8 @@ efficient deterministic concatenation.
 
 ## Main results
 
+* `Cslib.Probability.IsPPTOn.prefix`: write efficiently computed input data before
+  probabilistic output.
 * `Cslib.Probability.IsPPTOn.pair`: retain efficiently computed data alongside a sampled result.
 * `Cslib.Probability.IsPPTOn.bind_with`: a monadic continuation may capture the original input.
 * `Cslib.Probability.IsPPTOn.map_with`: a deterministic callback may capture the original input.