diff --git a/Complexity/Computability/Circuit/Arithmetic/Waring.lean b/Complexity/Computability/Circuit/Arithmetic/Waring.lean index 575e8384c5..d57e1e9705 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 ddd2655b1e..68509c72c2 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 6b90edb8e1..5cb3d0ce82 100644 --- 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 index c96270bb32..b3e3ef46da 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 d2f6036fba..c69700fb21 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 d2708c28a2..a8157a98f6 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 907588313b..d2880040a5 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 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 index 5de4f8e8ed..221a49f311 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 bd8f2dba93..8f85f8a181 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 d4c11f23ac..97c8d6a44d 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 f846be3c3d..9946959e6a 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 d2dc72c164..732978e4f8 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 603852f125..d7b2c63556 100644 --- 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 index beea44814e..a79a0cf89e 100644 --- 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 index 6f4c5230d2..253b55d614 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 2e737aa720..481cb2c625 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.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 index 7a375d6c62..f6e380d3dc 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 ccf14d146f..f685c59de0 100644 --- 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 index cdd9417e12..e4b1910fbd 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 f383fc91fe..5bd800c08f 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 cb5fb625a4..bfd9c96cad 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 c2a56640c9..dfc0199299 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 8a6d59501f..84025a54b1 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 bfe092b527..cd836cedb2 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 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/LogSpace/ConfigurationGraph/Bounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Bounds.lean index 3c7a673624..47711718bc 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 e26ae2ba77..475c0c43c9 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 427a4004c3..67066228f1 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 8657a57249..962b5c5a22 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 adde8e3241..9303742e89 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 1b5d69f144..e96823c503 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 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 eeae75d579..093cb81d79 100644 --- 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 index 30cf4db5d9..331596172b 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 70d1ee7b83..f6c17b7fa0 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 0a942bbc87..6b9bd57e87 100644 --- 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 index 4efb15acd3..0109d3e3e5 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.