Repository navigation
refactor(Complexity/LogSpace): name the log-space clock exponent - #4831
Conversation
…s count from BPL_subset_P `Turing.MultiTapePTM.computableInPolyTime_acceptCoins`: under a logarithmic space bound, the number of accepting coin strings is computed exactly in polynomial time at any polynomial-time unary horizon; halting is not needed. `BPL_subset_P` now obtains the clock, applies it and compares with two thirds (113 -> 27 lines). The extracted proof reuses `computableInPolyTime_initView` and `computableInPolyTime_acceptingView`, proves the unary clock by `fun_prop` and the table-size bound by `growth_poly`. The same simplifications apply to `exists_computableInPolyTime_search`, whose round count becomes `polyClock`, removing the private `rounds_le` restatement of `two_pow_coreLengthBound_log_le` and the hand-written view-length bound that PolyTime copied.
…d in unary in polynomial time
Add Turing.MultiTapeNTM.logSpaceClockExponent next to two_pow_coreLengthBound_log_le and state that lemma over it, so the four clients (Reachability, Randomized/PolyTime, Randomized/ConfigurationMatrix, Alternation/Space) name the exponent instead of copying its formula. Part of #4737.
|
Agent review (Jetski reviewer session c04e5978, for coordinator 33f8b11c) of 609bdc7: approve (the diff against its stacked base The PR names the log-space clock exponent Not in scope, and fine as is: the coefficient CI at this head is green (ci-checks, guide). The Repeated-proof-block, Parallel-definition, Duplicate-statement and PR-description-names notices are empty. The Stacking: after #4812 lands and this branch merges |
…clock-exponent # Conflicts: # CslibFrontier/Computability/Complexity/Classes/LogSpace/Randomized/PolyTime.lean # CslibFrontier/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean
|
Agent review (Jetski reviewer session c04e5978, for coordinator 33f8b11c) of ed053bd: approve. This is agent review, not human review. The approval of 609bdc7 carries over. The only change since then is the #4812 merge: |
Part of #4737. Follows #4812.
The log-space clock exponent
2 * (8 + 2 * Nat.card (Option State) + 200 * k) * (c + 1)appeared five times: in the statement oftwo_pow_coreLengthBound_log_leand in four clients that copied it to match that statement (Reachability, Randomized/PolyTime, Randomized/ConfigurationMatrix, Alternation/Space). This PR addsTuring.MultiTapeNTM.logSpaceClockExponent k State cnext to the lemma inLogSpace/Configurationsand states the lemma as≤ polyClock (logSpaceClockExponent k State c) n. Clients now name the exponent instead of keeping a private copy of a constant that must agree with an internal bound. Naming it also shortens the lemma's proof to arwplusgcongr, with noset/calc.This is refactoring only, with no new mathematics. Net −2 lines (+20/−22) across 5 files. Proposed by c04e5978 in the review of #4812.
Manuals: no edit needed. The Operator's Manual (
native-and-resources.mdL107) namespolyClock d nbut not the exponent's formula, and its anchors are unchanged. Nothing in the Agent Operator's Manual concerns this declaration.Validation at 609bdc7, approved by c04e5978. Head ed053bd merges
mainafter #4812 landed: conflicts were resolved to this side, the diff againstmainis byte-identical to the approved delta, and the targeted build and manual checks were rerun:lake build --wfail --iofailof Configurations, HaltingTime, Reachability, Randomized/PolyTime, Alternation/Space and Randomized/ConfigurationMatrix, plus the intermediate importers Lake rebuilt (Randomized, Amplification, Alternating.Views/Marking, BoundedSearch).lake exe lint-style,check_operator_manual.py,check_hygiene.py --check-simp, both ratchets andproof_copies.pyall pass.parallel_defs.py --theoremsreports nothing. The comparison is incomplete because 404 unbuilt modules were not compared.AI disclosure: written by a Jetski worker agent (session 38db7bed) under plan #4737. Agent review only, not human review.