From 80ea36d081571863ef1974ff9a16238b1e22c1b0 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sun, 25 Oct 2026 11:52:23 +0000
Subject: [PATCH 1/4] doc(Computability): add Main results entries for orphan
 declarations (#949)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Item 8 of #949 for the remaining unsubmitted areas of Computability
(Circuit, Machines, and Probabilistic: 35 files).

Adds ## Main results entries in module docstrings for all 46 † orphan
declarations in these areas. All declarations were verified to have
existing docstrings and represent public API. No statements or definitions
change meaning. All source lines are <= 100 characters.

Co-authored-by: worker-jetski-b5844be2 <b5844be2-557b-4d63-859e-d7561a4d7c65>
---
 Complexity/Computability/Circuit/Arithmetic/Waring.lean   | 1 +
 .../Circuit/Arithmetic/Waring/Compilation.lean            | 1 +
 Complexity/Computability/Circuit/Boolean/BatchLookup.lean | 1 +
 Complexity/Computability/Circuit/Boolean/Broadcast.lean   | 2 ++
 .../Computability/Circuit/Boolean/CarryLookahead.lean     | 1 +
 Complexity/Computability/Circuit/Boolean/KeyedSort.lean   | 1 +
 Complexity/Computability/Circuit/Boolean/Routing.lean     | 8 ++++++++
 .../Computability/Circuit/Boolean/ShannonSynthesis.lean   | 1 +
 Complexity/Computability/Circuit/Boolean/Sorting.lean     | 1 +
 .../Computability/Circuit/Boolean/WeightedThreshold.lean  | 2 ++
 .../Circuit/Boolean/WeightedThreshold/Menus.lean          | 2 ++
 .../Circuit/Boolean/WeightedThreshold/PendingBias.lean    | 2 ++
 .../Circuit/Boolean/WeightedThreshold/Potential.lean      | 3 +++
 .../Circuit/Boolean/WeightedThreshold/ScalarActivity.lean | 2 ++
 .../Circuit/Boolean/WeightedThreshold/TranscriptTree.lean | 3 +++
 Complexity/Computability/Circuit/Cyclic.lean              | 1 +
 Complexity/Computability/Circuit/Cyclic/Feedback.lean     | 1 +
 Complexity/Computability/Circuit/Evaluation.lean          | 1 +
 .../Computability/Circuit/Frontier/Nondeterministic.lean  | 2 ++
 .../Computability/Circuit/Fusion/Cyclic/Closure.lean      | 2 ++
 .../Computability/Circuit/Fusion/Cyclic/Compiler.lean     | 2 ++
 Complexity/Computability/Circuit/Fusion/Quadratic.lean    | 2 ++
 .../Circuit/Rational/Runtime/Determinant.lean             | 1 +
 Complexity/Computability/Circuit/SourceComplexity.lean    | 3 +++
 .../Complexity/LogSpace/ConfigurationGraph/Bounds.lean    | 2 ++
 .../Turing/MultiTape/Complexity/PolyTime/List.lean        | 1 +
 .../MultiTape/Complexity/PolyTime/RotationMap/Family.lean | 1 +
 .../MultiTape/Complexity/PolyTime/RotationMap/Tower.lean  | 2 ++
 .../Complexity/PolyTime/RotationMap/TowerTable.lean       | 3 +++
 .../PolyTime/RotationMap/TowerTable/Family.lean           | 2 ++
 .../Machines/Turing/MultiTape/Machine/Equivalence.lean    | 1 +
 .../Turing/MultiTape/Probabilistic/Composition.lean       | 2 ++
 .../Machines/Turing/MultiTape/SingleTape.lean             | 2 ++
 Complexity/Computability/Probabilistic/LinearHash.lean    | 2 ++
 Complexity/Computability/Probabilistic/PPT/Capture.lean   | 2 ++
 35 files changed, 66 insertions(+)

diff --git a/Complexity/Computability/Circuit/Arithmetic/Waring.lean b/Complexity/Computability/Circuit/Arithmetic/Waring.lean
index 575e8384c..d57e1e970 100644
--- 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
index ddd2655b1..68509c72c 100644
--- 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
index 6b90edb8e..adfbfa6ad 100644
--- a/Complexity/Computability/Circuit/Boolean/BatchLookup.lean
+++ b/Complexity/Computability/Circuit/Boolean/BatchLookup.lean
@@ -37,6 +37,7 @@ include these constants; the polynomial gate bound does not certify constructor
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.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
index c96270bb3..b3e3ef46d 100644
--- 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
index d2f6036fb..c69700fb2 100644
--- 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
index d2708c28a..a8157a98f 100644
--- 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
index 907588313..1554609ad 100644
--- 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.
+* `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
index 5de4f8e8e..221a49f31 100644
--- 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
index bd8f2dba9..8f85f8a18 100644
--- 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
index d4c11f23a..97c8d6a44 100644
--- 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
index f846be3c3..9946959e6 100644
--- 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
index d2dc72c16..732978e4f 100644
--- 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
index 603852f12..60037fb3d 100644
--- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean
+++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean
@@ -58,6 +58,9 @@ its gate transcript (`StrictMarginProgram.eval`):
 
 ## Main results
 
+* `Cslib.Circuits.Boolean.WeightedThreshold.existsUnique_ilpValid`: unique valid ILP transcript.
+* `Cslib.Circuits.Boolean.WeightedThreshold.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
index beea44814..80dab4c06 100644
--- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean
+++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean
@@ -48,6 +48,8 @@ enumerative coding for weight-bounded words (Theorem 4.3) is in
 
 ## Main results
 
+* `Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_max_card_attainableTranscripts_of_direction`:
+  sharp attainable-transcript capacity bound.
 * `Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_scalarScore_between`,
   `Cslib.Circuits.Boolean.WeightedThreshold.transcript_eq_of_scalarScore_between`: order-convexity
   of gate evaluations and transcripts along `scalarScore w`.
diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/TranscriptTree.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/TranscriptTree.lean
index 6f4c5230d..253b55d61 100644
--- 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
index 2e737aa72..6343c8a20 100644
--- 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.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
index 7a375d6c6..f6e380d3d 100644
--- 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
index ccf14d146..c18e58884 100644
--- a/Complexity/Computability/Circuit/Evaluation.lean
+++ b/Complexity/Computability/Circuit/Evaluation.lean
@@ -35,6 +35,7 @@ This module does not certify a runtime bound.
 
 ## Main results
 
+* `Cslib.Circuits.Program.trace_eq_traceImpl`: compiler replacement of trace by 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
index cdd9417e1..e4b1910fb 100644
--- 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
index f383fc91f..5bd800c08 100644
--- 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
index cb5fb625a..bfd9c96ca 100644
--- 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
index c2a56640c..dfc019929 100644
--- 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
index 8a6d59501..84025a54b 100644
--- 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
index bfe092b52..e9ad659c5 100644
--- 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 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/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Bounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Bounds.lean
index 3c7a67362..47711718b 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Bounds.lean
+++ b/Complexity/Computability/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
index e26ae2ba7..475c0c43c 100644
--- 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/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.lean
index 427a4004c..67066228f 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.lean
+++ b/Complexity/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/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Tower.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Tower.lean
index 8657a5724..962b5c5a2 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Tower.lean
+++ b/Complexity/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/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable.lean
index adde8e324..9303742e8 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable.lean
+++ b/Complexity/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/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean
index 1b5d69f14..5c4a9d8ed 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean
+++ b/Complexity/Computability/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.
 * `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
index eeae75d57..675724bca 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Machine/Equivalence.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Machine/Equivalence.lean
@@ -27,6 +27,7 @@ and stuck configurations; there is no clock rescaling or simulation overhead.
 
 ## Main results
 
+* `Turing.MultiTapeMachine.tmEquiv`: equivalence with upstream's deterministic machine type.
 * `Turing.MultiTapeMachine.step_toTM`: deterministic steps commute with conversion.
 * `Turing.MultiTapeMachine.step_toNTM_iff`: nondeterministic steps commute with conversion.
 -/
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Composition.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Composition.lean
index 30cf4db5d..331596172 100644
--- 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
index 70d1ee7b8..f6c17b7fa 100644
--- 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
index 0a942bbc8..59c5cd62e 100644
--- a/Complexity/Computability/Probabilistic/LinearHash.lean
+++ b/Complexity/Computability/Probabilistic/LinearHash.lean
@@ -25,6 +25,8 @@ The full extractor charges sampling, hashing and copying its complete public see
 
 ## Main results
 
+* `Cslib.BitString.LinearHash.computableTidilyInPolyTime_wordHash`: efficient word hashing with
+  unary dimensions.
 * `Cslib.BitString.LinearHash.computableInPolyTime_wordHash`: deterministic hashing.
 * `Cslib.BitString.LinearHash.isPPTOn_extract`: the complete seeded sampler.
 
diff --git a/Complexity/Computability/Probabilistic/PPT/Capture.lean b/Complexity/Computability/Probabilistic/PPT/Capture.lean
index 4efb15acd..0109d3e3e 100644
--- 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.

From 871170a3f3ca932481301196f8e403fd7123af0a Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sun, 25 Oct 2026 12:04:55 +0000
Subject: [PATCH 2/4] doc(Computability): qualify declaration names in
 BatchLookup and Potential

- Qualify eval_withPadding with batchLookupCircuit in BatchLookup.lean.
- Qualify existsUnique_ilpValid and sum_inTranscriptCell_ite with StrictMarginProgram in Potential.lean.

Co-authored-by: worker-jetski-b5844be2 <b5844be2-557b-4d63-859e-d7561a4d7c65>
---
 Complexity/Computability/Circuit/Boolean/BatchLookup.lean  | 3 ++-
 .../Circuit/Boolean/WeightedThreshold/Potential.lean       | 7 ++++---
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/Complexity/Computability/Circuit/Boolean/BatchLookup.lean b/Complexity/Computability/Circuit/Boolean/BatchLookup.lean
index adfbfa6ad..5cb3d0ce8 100644
--- a/Complexity/Computability/Circuit/Boolean/BatchLookup.lean
+++ b/Complexity/Computability/Circuit/Boolean/BatchLookup.lean
@@ -37,7 +37,8 @@ include these constants; the polynomial gate bound does not certify constructor
 
 ## Main results
 
-* `Cslib.Circuits.Boolean.eval_withPadding`: table values returned for all requests.
+* `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/WeightedThreshold/Potential.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean
index 60037fb3d..d7b2c6355 100644
--- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean
+++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/Potential.lean
@@ -58,9 +58,10 @@ its gate transcript (`StrictMarginProgram.eval`):
 
 ## Main results
 
-* `Cslib.Circuits.Boolean.WeightedThreshold.existsUnique_ilpValid`: unique valid ILP transcript.
-* `Cslib.Circuits.Boolean.WeightedThreshold.sum_inTranscriptCell_ite`: disjoint-support indicator
-  expansion recovering the output bit.
+* `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`,

From 6b05fda66df9b563e11fa959dfc87aabdcaf09af Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sun, 25 Oct 2026 12:16:49 +0000
Subject: [PATCH 3/4] doc(Computability): address review feedback on orphan
 documentation entries (#949)

- Use CyclicCircuit.ecomplexityFrom_ne_top_iff in Cyclic.lean.
- Clarify matching-and-broadcast stage in Routing.lean.
- Clarify reflection under injective homomorphisms in SourceComplexity.lean.
- Add backticks around Program.trace and Program.traceImpl in Evaluation.lean.
- Use dot notation shorthand for two_pow_lt_mul_max_card_attainableTranscripts_of_direction in ScalarActivity.lean.
- Complete sentence with contractFin in TowerTable/Family.lean.
- Move tmEquiv to Main definitions in Machine/Equivalence.lean.
- Group computableTidilyInPolyTime_wordHash alongside plain variant in LinearHash.lean.

Co-authored-by: worker-jetski-b5844be2 <b5844be2-557b-4d63-859e-d7561a4d7c65>
---
 Complexity/Computability/Circuit/Boolean/Routing.lean       | 2 +-
 .../Circuit/Boolean/WeightedThreshold/ScalarActivity.lean   | 3 +--
 Complexity/Computability/Circuit/Cyclic.lean                | 2 +-
 Complexity/Computability/Circuit/Evaluation.lean            | 3 ++-
 Complexity/Computability/Circuit/SourceComplexity.lean      | 2 +-
 .../Complexity/PolyTime/RotationMap/TowerTable/Family.lean  | 2 +-
 .../Machines/Turing/MultiTape/Machine/Equivalence.lean      | 2 +-
 Complexity/Computability/Probabilistic/LinearHash.lean      | 6 +++---
 8 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/Complexity/Computability/Circuit/Boolean/Routing.lean b/Complexity/Computability/Circuit/Boolean/Routing.lean
index 1554609ad..d2880040a 100644
--- a/Complexity/Computability/Circuit/Boolean/Routing.lean
+++ b/Complexity/Computability/Circuit/Boolean/Routing.lean
@@ -42,7 +42,7 @@ for batched lookup are separate clients.
 
 * `Cslib.Circuits.Boolean.routeCircuit.headers_perm`,
   `Cslib.Circuits.Boolean.routeCircuit.value_eq_true_iff`: header preservation and
-  matching OR values.
+  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
diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean
index 80dab4c06..4d32002b2 100644
--- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean
+++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean
@@ -48,8 +48,6 @@ enumerative coding for weight-bounded words (Theorem 4.3) is in
 
 ## Main results
 
-* `Circuits.Boolean.WeightedThreshold.two_pow_lt_mul_max_card_attainableTranscripts_of_direction`:
-  sharp attainable-transcript capacity bound.
 * `Cslib.Circuits.Boolean.WeightedThreshold.eval_eq_of_scalarScore_between`,
   `Cslib.Circuits.Boolean.WeightedThreshold.transcript_eq_of_scalarScore_between`: order-convexity
   of gate evaluations and transcripts along `scalarScore w`.
@@ -62,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`,
+  `.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/Cyclic.lean b/Complexity/Computability/Circuit/Cyclic.lean
index 6343c8a20..481cb2c62 100644
--- a/Complexity/Computability/Circuit/Cyclic.lean
+++ b/Complexity/Computability/Circuit/Cyclic.lean
@@ -39,7 +39,7 @@ Native acyclic circuits embed with exactly the same gate values, outputs and wei
 
 ## Main results
 
-* `Cslib.Circuits.ecomplexityFrom_ne_top_iff`: finite cyclic complexity equivalence.
+* `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/Evaluation.lean b/Complexity/Computability/Circuit/Evaluation.lean
index c18e58884..f685c59de 100644
--- a/Complexity/Computability/Circuit/Evaluation.lean
+++ b/Complexity/Computability/Circuit/Evaluation.lean
@@ -35,7 +35,8 @@ This module does not certify a runtime bound.
 
 ## Main results
 
-* `Cslib.Circuits.Program.trace_eq_traceImpl`: compiler replacement of trace by traceImpl.
+* `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/SourceComplexity.lean b/Complexity/Computability/Circuit/SourceComplexity.lean
index e9ad659c5..cd836cedb 100644
--- a/Complexity/Computability/Circuit/SourceComplexity.lean
+++ b/Complexity/Computability/Circuit/SourceComplexity.lean
@@ -41,7 +41,7 @@ not use Boyack's convention assigning zero to disconnected vertices.
 
 * `Cslib.Circuits.Circuit.ComputesFrom.map`,
   `Cslib.Circuits.Circuit.computesFrom_map_iff`:
-  homomorphism mapping and reflection of ComputesFrom.
+  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/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean
index 5c4a9d8ed..e96823c50 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/TowerTable/Family.lean
@@ -29,7 +29,7 @@ names, including its return label. Polynomial machine certificates are supplied
 ## Main results
 
 * `Cslib.RotationMap.TowerTable.contract_eq`: contracted table rotations agree with
-  quotient/remainder.
+  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
index 675724bca..093cb81d7 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Machine/Equivalence.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Machine/Equivalence.lean
@@ -24,10 +24,10 @@ 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
 
-* `Turing.MultiTapeMachine.tmEquiv`: equivalence with upstream's deterministic machine type.
 * `Turing.MultiTapeMachine.step_toTM`: deterministic steps commute with conversion.
 * `Turing.MultiTapeMachine.step_toNTM_iff`: nondeterministic steps commute with conversion.
 -/
diff --git a/Complexity/Computability/Probabilistic/LinearHash.lean b/Complexity/Computability/Probabilistic/LinearHash.lean
index 59c5cd62e..6b9bd57e8 100644
--- a/Complexity/Computability/Probabilistic/LinearHash.lean
+++ b/Complexity/Computability/Probabilistic/LinearHash.lean
@@ -25,9 +25,9 @@ The full extractor charges sampling, hashing and copying its complete public see
 
 ## Main results
 
-* `Cslib.BitString.LinearHash.computableTidilyInPolyTime_wordHash`: efficient word hashing with
-  unary dimensions.
-* `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

From ed45f469d63bbfde436078a4bd1d3ddf5e8e0847 Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sun, 25 Oct 2026 08:25:22 -0400
Subject: [PATCH 4/4] doc(WeightedThreshold): qualify the attainable-transcript
 Main entry

The entry read as a bare leading-dot name; use the namespace-qualified suffix form that the
doc-name lint resolves and that fits the 100-column limit.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB
---
 .../Circuit/Boolean/WeightedThreshold/ScalarActivity.lean       | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean
index 4d32002b2..a79a0cf89 100644
--- a/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean
+++ b/Complexity/Computability/Circuit/Boolean/WeightedThreshold/ScalarActivity.lean
@@ -60,7 +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`,
-  `.two_pow_lt_mul_max_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).