Repository navigation
Research/partial complex stopped - #119
Closed
seanabreau wants to merge 4 commits into
Closed
seanabreau wants to merge 4 commits into
seanabreau wants to merge 4 commits into
Conversation
…10^13 Add the source-pinned physical witness, exact assembly, finite Lean certificate, and independent verification targets. Retain the inherited analytic and fixed-tape assumptions and predecessor attribution.
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.
This builds on #104 (
948ce1510df750f4c18b96bdaef436a86f8bf834) and the exact #113 cyclic-strip producer (0eee4d507092a96bde88de703f07574ba17401a8).Under those interfaces,
The saving is 54.4687% above$2^{-14}$ .
Construction
Bit network (23,23). Apply #104's common-basis, opposite-bank stopped compiler to every proper projector of Swapnil Jain's frozen round-seven word, pinned at
741e7aa078392553815df7926ee17ac5e25a8c38. Every nonzero projector residual is one reversed child of its full rank. The strict coarse saving is15513/125000000; stopping at atom exponent1/1000, with ordinary leaf saving384599/10^10, gives ordinary bit saving1240183559/10^13.Complex network (24,24). Keep #113's producer and legal matching: 68,188 additions, 8,120 roots, 37,802 matched links and 38,506 physical auxiliary roles. Reconstruct the invertible matched scalar word
L, signed rational scatterJ, and exact complete adjointC=JL.A 32,488-event closure computes the 24 retained centers first, preserving every role's full access order, including read/read dependencies. Checks cover 209,340 accesses, retained-center boundaries and 8,096 ordinary root reads. Selected scratch is untouched by the closure and injection.
Select 9,356 nondegenerate partial subframes (3,309 distinct frames), each contained in its first owner and every target hyperplane receiving its adjoint coefficient. Target readouts follow actual nested chains. All residuals are nondegenerate; alternating cases use the retained inverse-Gram/Gauss interface.
For dimension d inside an owner of rank b, the first child changes from b to b-d, and the exterior from m-h to m-h+d. Source and sink phases change together: in stage one use
+q_sigmaandq_F+q_sigma; in stage two use-q_sigmaandq_F-q_sigma. The completed operator remainsq_F. Target-front chain replacements preserve rank mass. The strict complex saving is5893637/62500000000 = 0.000094298192.The complete adjoint has 11,678,073 nonzero coefficients per invocation, with numerator magnitude at most 42 over denominator 42. Charge 16 scalar operations per term and retain the predecessor allowance:
G = 2019773888 + 2*2024*11678073*16 = 758385205952.Recompute the denominator-21 exact grid, literal precision guard, completed-child height induction and
C1=1contract. Halving factors 367, 100 and 9 give row coefficient 12,961; p^27000 supplies degree gap13989/25 > 0. All copies, scalar work and wrappers are paid. Withbeta=10^-6andeta=10^-8, all 47 assembly constraints and seven margins are strict.Contribution sources and prior PRs
Proof and attribution
PROOF.mdgives the physical schedule, paired endpoint gauges, stopped bit recurrence, exact grid and all-size transfer dependencies.MANIFEST.jsonandSWAPNIL_SOURCE.jsonbind sources and inputs;NOTICEand imported headers preserve Apache-2.0 and source-specific attribution.New work used OpenAI Codex and twenty GPT-6-sol agents at medium reasoning effort, with independent audits.
EXPERIMENTS.mdrecords more than twelve tested directions and rejection of a scalar-valid schedule with unpaid frame descents.This is a conditional research bound. Analytic, prime, ordered-affine streaming, restored-row, exact-recovery and fixed-tape interfaces, constructive setup and eventual thresholds remain premises. Bit stage-two reversal and complex complement/time-reversal remain written dependencies. Finite Lean arithmetic does not formally verify the complete multiplication theorem.
Validation
1.1417e-10(bit) and1.5791e-13(complex), G, precision, rows, all 47 constraints and seven margins. Controls reject omitted copies, wrong sinks, degenerate frames and illegal selections.bit_grid,cx_gridandsigned_assemblyprint empty axiom lists; analytic enclosure interpretations and all-size transfers remain external.make verifypass, covering all eleven groups, isolated regressions and historical patch checks.Reproduction
make -C research/partial-complex-stopped verify make -C research/partial-complex-stopped verify-sources \ SWAPNIL_SOURCE=/path/to/pinned/round7 PR104_SOURCE=/path/to/pinned/pr104 cd research/partial-complex-stopped/kernel python3 generate.py lean KernelNew.leanThe README supplies pinned checkouts; CI repeats source and kernel checks.