Repository navigation
refactor(machines): spike, plain closure rules without a tidy calculus (#862) - #869
Closed
SamuelSchlesinger wants to merge 2 commits into
Closed
SamuelSchlesinger wants to merge 2 commits into
SamuelSchlesinger wants to merge 2 commits into
Conversation
Prove composition, pairing, case distinction and left folds for ComputableInPolyTime, and composition and case distinction for ComputableInO, directly from plain hypotheses. Each proof makes the plain machines tidy with the tidy normal form, combines them with the existing machine combinators and concludes plain computability. No tidy asymptotic predicate is imported; ComplexityTests/PlainDirect.lean checks that and closes goals from PolyTimePlain with fun_prop using only the direct rules. Spike, not for merge. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB
The tidy normal form keeps degrees, so the plain degree composition has the degrees of the tidy rule. Checked on upstream's copy machine. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB
SamuelSchlesinger
force-pushed
the
spike/no-tidy-calculus-862
branch
from
October 24, 2026 19:41
294e0d3 to
e3df3ca
Compare
SamuelSchlesinger
changed the title
SamuelSchlesinger
added a commit
that referenced
this pull request
Oct 24, 2026
Adapt the direct-construction proofs from #869 by worker-claude-tidyspike-c4b0c164. Charged O keeps independent T/S and uses its existing output charge; Degree keeps d/e independent. Focused strict build: 3602 jobs, /tmp/862-direct-resource-composition.log. This is a source checkpoint, not whole-library or S4 completion.
orbitingflea
pushed a commit
to orbitingflea/complexitylib2
that referenced
this pull request
Oct 26, 2026
…lib-community#810) * feat(machines): seed direct canonical plain polynomial-time primitives Adapt the sorry-free machine constructions from cslib-community#869 e3df3ca, credited to worker-claude-tidyspike-c4b0c164 with original mathematical authors preserved. Normalize plain realizing machines, combine explicit machine witnesses, and conclude plain; no high tidy computability predicate or bridge is imported by the new direct modules. Preserve pure PolyBounded names/credit at a lower independent home. This focused source seed is not whole-library or S4 completion. * feat(machines): prove plain resource composition directly Adapt the direct-construction proofs from cslib-community#869 by worker-claude-tidyspike-c4b0c164. Charged O keeps independent T/S and uses its existing output charge; Degree keeps d/e independent. Focused strict build: 3602 jobs, /tmp/862-direct-resource-composition.log. This is a source checkpoint, not whole-library or S4 completion. * feat(machines): prove plain degree constants and encoding transports directly * feat(machines): add direct finite-degree rule and zero-degree clients * feat(machines): prove plain degree projections from machine witnesses * feat(machines): derive canonical plain prefix folds and unary iteration * feat(machines): join direct core and loop contracts Expose generic PairEncoding projection certificates while preserving standard registered fst/snd and their explicit encoding arguments. Register standard prod, checked by a concrete plain function client. Remove only byte-identical legacy Size/Unary definitions after moving them lower. Focused core, Degree zero/universe/projection and growing-loop fixtures warning/info-strict PASS3648; standard3 axiom guards and no-high-tidy-calculus environment guards pass. Generic opaque encoding needs an explicit complete certificate because its other encoding is not inferable. Full source deletion and library frontier remain pending. * feat(machines): normalize independent uncharged bounds directly Move the existing plain BigO definition to ResourceBounds, add the accepted common-linear predicate, and share one same-machine min-space normalization proof between charged O and uncharged BigO. Add direct linear copy, constant and composition primitives. Focused strict source PASS3590 and streaming/zero-workspace/charged-negative/universe/axiom fixtures PASS3592. New source does not import a higher tidy asymptotic calculus; legacy codec raw Linear fields remain the explicit temporary exception. No uncharged composition shortcut is introduced. * feat(machines): prove degree append from normalized machines * feat(machines): construct independent degree pairing directly * feat(machines): prove independent degree conditional closure directly * refactor(machines): expose direct primitives through existing plain facade Remove superseded plain PT definitions from the legacy facade and import canonical direct source. Preserve standard projection call syntax, named encoding arguments and broader independent input universe for pair-valued projections. Existing raw client modules and their registration remain staged rather than being deleted prematurely. Direct and legacy facade source plus focused core/Degreeclosure fixtures strict PASS3664; no whole-library/parity claim. * feat(machines): derive plain invariant and growth loop contracts * refactor(machines): expose direct resource and loop families Expose direct O, Degree and loop families at existing import paths, removing superseded plain captured-loop copies. Move unchanged machine clock/output facts and the three ordinary Degree bound/PT rules lower, retaining public names and credit; the pure DegreeBounded-to-PolyBounded fact moves with its algebra. New proofs depend on direct plain rules and machine construction only. Actual original facade targets plus growing-loop/independent-resource fixtures strict PASS3690. Legacy raw client calculus remains transitional; no whole-library or final-deletion claim. * feat(machines): derive plain option degree primitives from codec machines * feat(machines): certify option presence by a direct finite-state machine * refactor(machines): expose direct option degree providers Join the independently authored direct Option family at the canonical degree import path. Generic OptionEncoding some/getD preserve 1/1; specialized isSome preserves 1/0 via a direct finite-state transducer. Actual joined source and13 provider/negative/env controls strict PASS3662. Existing raw client APIs remain transitional. * fix(machines): retain composition source compatibility Restore the existing public comp conclusion spelling f ∘ g; its definitionally equal lambda form made three existing Function.comp_apply simp uses redundant. Adjust only the new internal loop proof for that representation. Actual Products/GraphProblems and direct core/loop controls strict PASS6862 with no external client edits, assumptions or warning suppression. Frozen682 full library source frontier remains preserved as zero source errors/three warnings. * feat(machines): prove unary successor and predecessor directly * refactor(machines): share the direct unary successor machine * feat(machines): share word predicate machines for direct unary zero testing * refactor(machines): expose direct unary degree providers Expose the exact original unary1/1 contracts at their original import path, using a single shared successor machine and shared word-predicate machine with the Option family. Joined source and all unary/Option controls strict PASS3678. * feat(machines): derive plain degree witnesses from polynomial clocks Move the existing exact-time-to-PT consequence below the legacy bridge module, and add plain PT.exists_degree by retaining its one realizing machine. Resource degree is the maximum of clock/workspace degrees; output degree follows the actual clock separately. No normalization/higher tidy calculus imported. Strict source PASS3650 and unrelated-universe/existential/standard3-axiom/env clients PASS3632. This unblocks direct Decoder source work without old high-calculus imports. * refactor(genericram): make native certificates directly plain Move NativeCertificate to its model-independent source module and change its implementation field/constructors to charged plain O. Preserve exact constructor time=t/workspace=s+t and composition formulas, justified by actual plain output length. Move the unchanged IsComputable model/witness facts and bare unbounded-to-bounded machine fact below legacy halting closures. New certificate imports no higher tidy calculus; raw codec Linear fields remain the explicit temporary exception. Direct proof/body correspondence with worker559 supplier3b198 is retained without its high-level imports/backend ancestry. Model namespace tail byte-identical to d445 (digest9cf16f28); source targets PASS3708 and growing-copy/zero-workspace/comp/field-budget/env/axiom fixtures PASS3634. Outside clients and StepMachine fields remain pending. * refactor(machines): share pure framing and frame-reader machines * refactor(machines): share the existing public frame emitter kernel * feat(machines): construct charged linear resource combinators directly Prove linear transducer/framing/parser/projection rules from shared bare machines, without importing the codec provider into the word-machine core. Charged O linear composition keeps independent time/workspace: intermediate word is bounded by the same clock for time and existing output charge for workspace. Add direct concatenation/framed pairing/projections/constant-output rules. Move unchanged plain uncharged BigO bound/weakening rules lower, preserving their lack of output premise. Source and legacy facade PASS3694; concrete growing/framed/fixed-output/resource-premise negative/Type1/env/axiom plus zero-workspace/native fixtures strict PASS3650. Shared652/dee machine sources consumed once. This is Step compiler foundation, not Step field/parity/S4 completion. * refactor(machines): compile plain step resource certificates directly Replace StepMachine.Tidy by ResourceCertificate with charged plain halt/step fields and unchanged uncharged BigO whole-run formulas/HaltsAt/output equality. Move compiler proofs under Internal and keep its exact machine-level result private. Its parts use direct O combinators; NormalForm.inO supplies only bare normalized machines, with no high tidy O/Degree/Linear calculus. Reexport from the original provider path without aliases. Three generic selected-tape machine lemmas move unchanged to Internal/OnWords; eight runtime/encoding/transducer/withInit blocks byte-identical to daff, and stepTM/stepRound untouched. Source/compiler strict PASS3662 and original provider path PASS3664. Restore original f∘g spelling for O/Degree composition. This is a provider checkpoint: real emitter tests and consumer repair are next, no full library/parity/S4 claim. * test(machines): check direct streaming resource certificates A fixed finite-state emitter copies arbitrary runtime words with constant workspace via the plain ResourceCertificate compiler. Preserve exact original run/halts/output proofs, including empty input, and refute the charged whole-output analogue. Check fixed halted zero-round initialization with the canonical zero-workspace initial certificate, no high tidy calculus/old bundle in the environment and standard axioms. Warning/info-strict focused build PASS3666. Composition/writer/client closure remains a separate measured obligation. * feat(machines): prove controlled charged folds directly Preserve exact original O fold/foldWith hypotheses and independent resource formulas, normalizing only given plain witnesses before the bare machine fold. No high tidy O derivation graph is imported. Keep the full reachable-prefix state invariant; a captured parameter is encoded/charged uniformly. Add direct same-machine encoding transports and pointwise/asymptotic bound weakening. Source PASS3646; runtime-word parity, runtime captured-polarity contexts, exponential-state-bound counterexample, no-high-calculus and axiom clients strict PASS3648. Binary leaf and Step composition/client closure remain explicit, not covered by these source checks. * fix(machines): retain unary proof under canonical composition spelling Account for the original f∘g form in the direct Degree composition rule by unfolding Function.comp_def in the unary zero-test proof. Statement, machine, bounds and runtime data unchanged. Direct source joins validate warning/info-strict PASS3726; this one-line supplier has no List/Decoder payload ancestry. * refactor(machines): join direct Decoder fields and List providers Collect ONLY worker559 nine owned Decoder paths at fc258ea, worker560 exact List source/tests0df8be07 and shared pure Size19436c23, preserving authors/credit; no supplier branch ancestry or foreign area files replayed. All eight Decoder constructor telescopes/decode/inversion bodies are retained; computable field and method are plain. Original List reexports direct providers and retires only the superseded plain bitsReverse wrapper. Remove one legacy pure size lemma after its lower move. Joined original Decoder/List and all leaf/compound/word/framed controls warning/info-strict PASS3726. The Unary composition-spelling fix is separate e347. Transitive legacy Nat proof-module separation, Option.some automatic usability, field consumers/full parity/S4 remain explicit; no full-library claim. * style(machines): make reverse bound simplification explicit * refactor(machines): lower unchanged binary digit algorithms * feat(machines): construct binary resource leaves from direct folds * test(machines): check direct binary resources and carry boundaries * refactor(machines): join direct binary and decoder import paths * fix(machines): expose direct bit decoding and retain legacy witness packaging * feat(machines): derive direct computed list constructor recipes * test(machines): exercise direct generic list recipes * feat(machines): derive charged bounds from direct degree witnesses * refactor(machines): stage plain step composition pending direct equality Compiler frontier: missing O.eq and stepG elaboration at the unchanged 200k budget. Not a validated provider checkpoint. * feat(machines): derive direct word equality at original resource bounds Moves EqWords definitions and laws byte-identically with original credit. Direct Degree leaves and charged O fold use only plain machine witnesses. Focused generic/empty/unequal-word/degree-zero environment checks elaborated; four axiom closures are the standard three. StepMachineComp remains a separate open elaboration frontier. * feat(machines): complete direct step composition without high calculus imports Strict focused equality and streaming/composition/zero-init fixtures pass 3720 jobs at original budgets. Original composition formulas and programs retained; pure binary-size facts moved unchanged with existing names into Internal. Legacy helper names are explicitly transitional, not S4 completion. * feat(machines): add direct plain option construction and default rules * refactor(machines): complete direct captured option calculus and reexports * test(machines): restore concrete decoder option automation through public rules * test(machines): close literal binary decoder option automation * feat(machines): derive direct finite table lookup and updates * test(machines): preserve generic finite table contracts * refactor(tactic): stage guarded backend on direct canonical seed * refactor(machines): align native scalar and decoder consumers with direct fields Four scoped source targets plus unchanged IntBinaryDecode tests pass strict validation (5368 jobs). Concrete scalar raw witnesses are only forgotten locally as authorized; existing scalar and universal legacy statements remain staged. Runtime model, encodings, decoder runtime/inversion and numeric contracts preserved. Native counted iterate and ReadMachine comparison remain a separate direct-provider frontier. * doc(machines): retain credit for the direct lookup fold proof * refactor(machines): stage plain consumers at the counted-loop frontier WIP source frontier, not a compiling supplier: only Native ComputableInO.iterate and ReadMachine natLt are unavailable. No legacy raw loop fallback, new assumptions, aliases or registrations. The 32 constructor time/space assertions are unchanged modulo the approved raw-to-plain predicate substitution; all existing data formulas and program bodies are retained. * feat(machines): construct direct binary-counted resource iteration Moves credited pure counter and predecessor-iteration laws; direct plain round certificates feed existing exact machine combinators after NormalForm.inO. Original time/space formulas and all j <= n trajectory/output bounds retained. Direct natSub/natLt preserve the old value-sensitive bounds. Both formerly blocked Native/ReadMachine consumers and legacy binary comparison compile warning-strict (3802 jobs). * test(machines): cover counted-loop bounds and native reader consumers Strict direct-core/consumer controls pass 3806 jobs: complete telescope, zero counter/state, growing output with required charge, no-high-calculus environment and standard-three axioms; exact Native time/space values and stopped ReadMachine runtime/formulas. Original GenericRAMNative/TreeEval suites remain blocked at unmodified Simulation/Turing and TreeEval/Reader/Cert/Machine imports; no assertion, tactic or budget was weakened. * refactor(machines): repair native simulation and tree reader certificate imports Only the two measured import blockers. Direct tuple/projection/equality operations plus proof-local erasure of already-complete fixed-table/sparse-memory/component witnesses; no public converter or new primitive. Native 41 theorem blocks and existing raw step_inO header unchanged; TreeEval stateBudget/component proofs/aggregate time function unchanged. Both source targets pass warning-strict (4994 jobs). * fix(tactic): check raw certificate applicability before deferring * feat(machines): reconcile landed arithmetic frontends with direct providers * refactor(machines): align run and tree space consumers with direct certificates Preserve all existing declaration headers and Native resource formulas. Use direct charged Native certificates internally and retain the uncharged TreeEval whole-run BigO bound. Existing legacy endpoints are packaged proof-locally from complete witnesses; static legacy gather/sum/memory facts remain explicit transitional dependencies. Validation: strict Run, TreeEval.Space and direct Nat frontends pass (5664 jobs). Original TreeEval suite passes; original GenericRAMNative stops at 14 WordRAM.Native certificate mismatches, without test edits. No whole-library, full parity or S4 completion claim. AI-assisted implementation by Codex. * refactor(wordram): consume plain native certificates directly Remove exactly thirteen obsolete tidy arguments and one of_tidy wrapper in Native consumers. Public declarations, algorithms, encodings and all resource formulas are unchanged. Strict WordRAM.Native compiles. The unchanged GenericRAMNative suite reaches ten obsolete-transport mismatches in its own assertions at lines34,36,38,40,42,44,59,67,68,212. Tests remain unchanged; no library-wide build was run. AI-assisted by Codex. * test(genericram): migrate native certificate proof calls Use existing bundle polynomiality components and direct plain option certificates for the ten constructor API call sites. Preserve all test statements, runtime/numeric assertions, tactics and budgets. Existing scalar implementations remain transitional dependencies of the shared bundle. Strict original GenericRAMNative suite passes3968 jobs. One style-only wrap corrected after the initial strict attempt. AI-assisted by Codex. * refactor(machines): align reader writer and extractor certificates Migrate existing Step bundles to ResourceCertificate without changing time/space formulas. Writer uses the direct uncharged BigO endpoint; decoder clients consume plain degree/PT fields directly. Runtime programs and encodings are unchanged. Strict three sources compile. Original LyubashevskyNative and MonotoneCircuitValue suites pass; Reingold stops at unassigned USTCON.Space68 retired whole-run projection (plus cascading goal). No tests, tactics or budgets edited. AI-assisted by Codex. * refactor(machines): align connectivity and decoder consumers Use the direct uncharged Step whole-run result for USTCON without altering its binary head-position space bound. Repackage complete Decoder machine witnesses only inside existing legacy NP/TQBF proof endpoints. All39 declaration headers and runtime programs are unchanged. Strict original Reingold, NPWitness, NPExistsAppend and TQBF pass6850 jobs; Oracle.TQBF plus original Relativization pass6766. No tests/tactics/budgets modified, no whole-library repeat or main rebase. AI-assisted by Codex. * perf(tactic): scope immutable classification memo across PPT * fix(ppt): guard conditional and iteration rule applications * refactor(probability): use direct conditional certificate in selection Preserve the full selectBest interface and program. Build its existing update callback explicitly from direct unary successor/comparison, pair and conditional rules rather than raw-goal automation. No provider/converter/test/budget changes. Strict Selection source passes7038 jobs; original PseudoentropyTraining passes7116. PCP tableVerifier/checkEdge remain blocked by missing shared direct listGetD/idxOf contracts and are unchanged. Memo00d6 and shapef7 suppliers are joined once as integration candidates, not delivery-approved. AI-assisted by Codex. * feat(machines): add direct generic list lookup and first index Preserve arbitrary SizedListEncoding, explicit fallback and unary indices/results. Direct codec witness erasure and full-prefix folds implement lookup; the original credited index transition/invariant moves once to a pure shared home. Direct equality and bounded-growth fold prove idxOf, preserving first occurrence and absence=length. Direct controls pass3684 jobs with no high raw calculus and standard axioms. Encoded.checkEdge compiles with full captured labels/graph/index; original PCPEncoded reaches unassigned CloudRotation73. PCP tableVerifier still requires a shared captured-map contract; no private duplicate or test weakening. No whole-library build/main rebase. AI-assisted by Codex. * feat(machines): implement direct captured list mapping Replace the legacy transported mapWithInput implementation with the same canonical telescope, registration and direct captured-fold proof. Reuse original foldlMap invariant without copying it. Complete captured input, arbitrary encodings and callback clock determine the prefix bound, without new hypotheses. Original PCP tableVerifier and CloudRotation source certificates compile via explicit shared plain APIs; headers/runtime programs unchanged. Direct no-high-calculus controls pass3686, original PCPNP passes. Original PCPEncoded stops at expanded raw cloudRotation automation190; tactic/budget/test unchanged. No whole-library run/main rebase or parity claim. AI-assisted by Codex. * refactor(crypto): prepare plain definition and padding interfaces (cherry picked from commit 82f44cf) * refactor(crypto): retire obsolete tidy proof bridges * refactor(crypto): apply verified sweep recipe with explicit remaining failures * refactor(crypto): reconcile reviewed quantitative contracts with main Adapt the six contracts from a3857dc by codex-review-559, retaining main projection/pair construction witnesses. Source and actual PRGStretch tests pass strictly; remaining ordinary sweep diagnostics and Compactness are explicit pending work. * refactor(crypto): checkpoint manual plain statements and shared premises Preserve explicit remaining compiler/automation diagnostics; this is not final sweep validation. The reviewed quantitative contracts and original numeric/negative clients remain in scope. * refactor(crypto): align proof callers and plain client assertions Preserve functions, encodings and resource formulas. Explicit proof-local transports repair changed provider calls. Crypto client assertions now use plain deterministic certificates with their original tactics and negative checks. This is a compiler-frontier checkpoint, not completion: remaining mixed PPT/program-certificate failures and final roots/gates are recorded in the worker handoff. * refactor(crypto): carry plain providers through security clients Keep the full-input resource witness in Compactness without normalization. Preserve GMW sampling and interaction programs and prove their existing PPT contract by separate sampler and two-round composition. Complete canonical argument transports through Homomorphic, ThreeSource and Commitment clients. Strict focused providers pass; complete roots and direct-plain automation acceptance remain pending. * refactor(crypto): close full library and abstract consumers The complete Complexity and ComplexityAbstracts roots pass warning-strict validation (12108 jobs). Preserve full-input GMW view reduction and existential Compactness resource witnesses with ordinary certificate transports. Keep all client algorithms, encodings, quantified bounds and negative assertions. Complete tests, plain automation dependency, surface measurement and final gates remain pending. * test(crypto): validate all concrete sweep clients All 35 ComplexityTests/Crypto modules pass strict validation (7800 jobs), preserving runtime/negative/axiom checks. Remaining shared plain tactic consumers still require the separate checked automation prerequisite. * refactor(crypto): use the landed plain captured-map interface * style(crypto): retain warning-strict stretch formatting * fix(ppt): stage strict shared-boundary activation and controls * fix(polytime): retain supplied quantified certificate families * fix(polytime): guide scans with supplied local callbacks * fix(crypto): retain plain evidence in padding seed and MAC proofs * fix(probability): compose supplied sampler and callback certificates Repair only measured UniformNat, Selection and LinearHash proof sites. Use explicit existing preprocess/map_with/bind_with/list lookup/replicate certificates with supplied plain/local evidence; retain every statement, program, distribution, encoding and resource premise. No global raw-search fallback, new provider or test/budget change. Focused strict three-source build passes7114 jobs; all14 declaration headers unchanged. Existing complete legacy arithmetic/certificate implementations remain transitional dependencies rather than a direct/S4 completion claim. AI-assisted by Codex. * fix(crypto): compose the MAC acceptance certificate explicitly * fix(crypto): apply supplied dyadic sampler certificates * fix(crypto): compose hybrid stretch and word extraction certificates Repair only measured Sequence, Stretch and WordSeedExtraction proof sites through existing plain/local certificates. Preserve all42 complete declaration headers, runtime programs, distributions, encodings and quantitative assumptions. No provider/private duplicate, raw global fallback, test or budget change. Stretch generic captured test is proved before its parameterized reduction and reused to avoid duplicate proof recipes; every later security statement/proof is byte-identical to cc70. Focused strict three-source check passes7190 jobs. No whole-library/six-gate or surface update. AI-assisted by Codex. * refactor(ppt): expose plain map and numeric sampler premises * fix(ppt): align direct sampler and map proof arguments * fix(crypto): apply supplied probability-test certificate * fix(classes): align decoder and PCP certificate consumers Repair only six measured class/PCP proof sites using existing direct Decoder/Degree fields and shared list certificates. Preserve all238 parsed declaration headers, independent existential degrees, algorithms, encodings and numeric contracts. Legacy raw endpoints use proof-local complete machine witnesses only; no public converter/provider/alias or extra premise. Six source targets strict PASS5608; original Kannan/Kadin/TFNP/ProofComplexity/Ladner/PCPEncodedIteration strict PASS4698. No test/tactic/budget changes, whole-library run or main rebase. AI-assisted by Codex. * fix(crypto): consume canonical decoder and frame certificates Repair only five measured Decoder/frame consumer modules. Use canonical plain Decoder and independent Degree interfaces; existing legacy raw proof endpoints normalize complete plain certificates proof-locally. Migrate two Leveled map callback arguments to their existing plain interfaces. No public converter/alias/provider, runtime/encoding/resource hypothesis or test/budget change. Focused five-source warning-strict build PASS6930 jobs. Class payloadbe6 is included unchanged once as7d129087. Broader validation belongs to worker559. AI-assisted by Codex. * fix(library): compose nine measured plain certificate consumers Repair only the nine allocated proof sites on73246bc8 with existing shared plain/local evidence. Preserve complete declaration headers, models/programs, encodings, independent degrees, numeric bounds and limits. Explicit game bind/map proofs retain original sampling order and full saved state; no provider/alias/new premise or raw global fallback. Focused nine-source warning-strict check PASS7606 jobs. No original test edits, whole-library run, main rebase or further repair expansion. AI-assisted by Codex. * feat(polytime): derive optional computed list lookup directly * test(polytime): preserve optional lookup scope and empty clients * feat(polytime): expose direct captured first-occurrence lookup * refactor(ppt): expose plain computed sampling and memoization * fix(ppt): align direct computed-sampling callers * fix(ppt): complete reviewed plain map caller migration * fix(crypto): compose the three-source extractor certificate explicitly Change only the existing isPPTOn_extract proof. Shared replicate/bind/map certificates retain original input, samples and preceding outputs in exact stage order; no commutation, new premise/provider or limit change. All19 declaration headers, extract runtime definition and entire later security source are unchanged. ThreeSource warning-strict source PASS7206 jobs. Original GMWPointwise attempted once and stops at new unassigned ThreeSource/Seeded81 exhaustive-search dependency; no edits or test weakening. No broadbuild/main rebase/surface update. AI-assisted by Codex. * fix(crypto): compose seeded three-source hash certificates Change only isPolyTime_hashSamples proof through existing plain pad/map/row/flatten/hash/append certificates. Preserve full inputs, fixed row0/count/seed widths, revealed keys, runtime and security statements. No provider, premise, commutation or limit change. Entire ThreeSource subtree source closure PASS7260 jobs; reviewed47641d58 baseline/caller changes preserved and only frozen53bcec0d joined once. Next authorized combined validation runs on this immutable source. AI-assisted by Codex. * fix(crypto): compose GMW simulator efficiency certificates Use existing plain bind, map and sampler certificates explicitly without changing protocol statements or programs. Reflow the MCSP proof application. * fix(crypto): compose GMW reduction efficiency proofs * chore: lower verified current Crypto surface baseline * fix(crypto): align new-main proofs with canonical plain certificates * chore: lower verified sampler and memoize surface entries * refactor(polytime): derive Boolean equality wrappers from direct rules Preserve existing public telescopes and Basic reexports; use direct finite Boolean and encoded word equality proofs. Correct stale direct-core and encoding reexport prose. * chore(boundary): retain the actual-main ratchet pending native measurement * fix(mac): preserve message schedules in plain certificate proofs * fix(crypto): compose current-main consumers with plain certificates * refactor(crypto): align current consumers with the plain interface carrier * feat(polytime): expose direct total word framing certificates * fix(list): qualify the word framing function beside its certificate * fix(bitstring): disambiguate the framed-word function in its contract * fix(etm): compose existing certificates without repeated proof search * fix(merkle): align security proof certificates with plain interfaces * chore(imports): regenerate the current interface aggregate * fix(polytime): retain existing plain recipes for raw construction goals * Record exact OnWords kernel boundary and import guard * Use plain numeric certificates in strict repetition APIs * Adapt native simulation certificate arguments to plain APIs * Align direct repetition callers and existing plain certificate arguments * Accept plain captured certificates in the seeded hash extractor * Use existing plain extractor arguments directly * Expose direct finite Boolean XOR certificate * Expose direct proposition conjunction and conditional frontends * Use plain deterministic inputs for empirical selection APIs * Retain raw constructor compositional alternatives * Align selection callers and retain the raw schedule assertion * Keep the deferred raw constructor alternative available * Reuse complete local certificates in nested plain search * Exclude implementation metadata from certificate duplicate checks * Register the existing direct unary-to-binary conversion * Align remaining repetition callers and the landed FHE bridge * Use the plain repetition premises in simulator proofs * Lower the native public tidy baseline after the interface cutover * Reflow the merged FHE bridge proof * Name plain resource certificates accurately and update their docs * Document the plain GSW and quantitative stretch interfaces
Collaborator
Author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Spike — not for merge. Evidence for #862: can the tidy computability calculus be deleted, with each plain closure rule proved directly and tidiness used only as a machine-level construction inside proofs? Verdict and analysis are in the #862 report; this PR holds the prototype so CI checks it.
The new modules prove plain closure rules from plain hypotheses. Each proof unpacks the plain machines, makes them tidy with the tidy normal form (
ComputesInTimeAndSpace.computesTidily_tidy), combines them with the existing machine combinators, and concludes plain computability. None of these modules imports a tidy asymptotic predicate:ComputableTidilyInPolyTime,…InO,…InDegreeand the rest are not in their environment. They add no public tidy statement, and the tidy-statement ratchet still matches its baseline.…/Complexity/PlainDirect/PolyTime.lean:ComputableInPolyTimecomposition, pairing for anyPairEncoding,ifon a plain Boolean test in any encoding, left folds, and pair projections. Composition is entirely machine-level (ComputesTidilyInTimeAndSpace.comp). Pairing,ifand folds call the explicit-bound combinatorsPairEncoding.pair_mono,ComputableTidilyInTimeAndSpace.iteand.foldlwith anonymous machine constructors.…/PlainDirect/BigO.lean:ComputableInOcomposition andif, with exactly the bounds of the tidy rules. The3 sthat the normal form adds to time is absorbed by applying it with spacemin s (k t + k).…/PlainDirect/Degree.lean:ComputableInDegreecomposition, with the tidy rule's degreesmax d₁ (e₁ d₂)ande₁ e₂.ComplexityTests/PlainDirect.lean:attribute [local fun_prop]and closes goals borrowed fromPolyTimePlain.lean, including that test's negative control;Oand degree rules.Validation: all six gates passed locally (
scripts/check.sh, as a full check becauseComplexity.leanchanged) on the first commit before a rebase.scripts/check_tidy_surface.pyreports 1887 statements, matching the baseline. After rebasing onto main7f8c7d06(heade3df3ca7),mk_all --checkpasses and the prototype and test modules were rebuilt; hosted CI covers the full gates. Every new declaration depends only onpropext,Classical.choiceandQuot.sound. The PR title check fails by design:spikeis not an allowed type, and the title marks this as not for merge.Abstracts: no impact (new local-only spike modules; no selected statement changes).
AI disclosure: written by
worker-claude-tidyspike-c4b0c164(Claude Code), delegated bycoordinator-claude-c4b0c164-20261023. Not human-reviewed.🤖 Generated with Claude Code
https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB