Proofmap

Friction report

Where the sources disagree or the structure was guessed, ranked. 115 items · 4 warn · 111 info. In v1 these are paper-internal; Lean-vs-paper rows arrive in Phase 2.

paper statements
23
Lean declarations (Phase 2)
—
aligned pairs
—
friction items
115
SeverityKindNodeNoteSource
warnunresolved_ref
thmInteger multiplication in O(n (lg n)^{1-κ}) time
Prime existence uses the external prime-interval lemma [HarveyHoeven2021, Lemma 5.1]; ring products use the established O(n log n) multiplier as a subroutine.
sections/00-introduction.tex:21
warnunresolved_ref
propPower-width chunk interchange in O(Ve^τ)
Key step uses the common-frame identity eq:common-frame-identity from §3.2, which is not a labeled statement.
sections/04-swap.tex:129
warnunresolved_ref
propSimultaneous Hadamard layer in near-linear time
The proof relies on unlabeled material preceding it in §5 (phase-frame recursion, row construction, recurrence unrolling, guard-width bound) rather than labeled statements.
sections/05-layers.tex:826
warnunresolved_ref
lemOne-dimensional resampling without sorting
The exact Gaussian identity, inverse estimate, contraction bounds and numerical maps are imported from Harvey–van der Hoeven (Theorem 4.2, Lemma 4.6, Prop. 4.7, Lemmas 4.8–4.12).
sections/07-resampling.tex:53
infostructure_uncertain
thmInteger multiplication in O(n (lg n)^{1-κ}) time
No proof environment; the proof is the whole of Section 9 (sections/08-assembly.tex), outlined here.
sections/00-introduction.tex:21
infoinferred_dep
propSimultaneous Hadamard layer in near-linear time
critique: The statement (sections/05-layers.tex:914-915) defines C_0 from "the fixed constants of Proposition ". The proof's "phase-frame construction reduces a group of e selected bits to s_c children" (line 929-930) is that proposition.
sections/05-layers.tex:826
infoinferred_dep
lemCost and accuracy of synthetic transform
The proof says exchanges of nonadjacent width-K address chunks each cost O(TpK^τ). That cost is the fixed-τ chunk-exchange bound, but the lemma is not named or numbered, so this link is inferred.
sections/06-transforms.tex:171
infoinferred_dep
lemExact negacyclic product with one truncation
critique: The statement at sections/06-transforms.tex:468-469 takes its inputs "in the component format of Proposition  with width w", but no edge is recorded.
sections/06-transforms.tex:463
infoinferred_dep
propSynthetic convolution: error, cost, and format
critique: The statement at sections/06-transforms.tex:635 begins "Under the hypotheses of Lemma ". The proof also runs its forward and opposite procedures, so the statement-level edge is missing.
sections/06-transforms.tex:633
infoinferred_dep
lemTensor resampling across d dimensions
critique: The statement at sections/07-resampling.tex:307-308 says "every pair (s_i,t_i) ... satisfies Lemma ", and the proof tensors its identity (line 342). The edge exists only on claims, not on the lemma itself.
sections/07-resampling.tex:305
infoinferred_dep
lemChirp identity and source permutation cancellation
critique: The statement at sections/07-resampling.tex:418 takes "R,Q,s_i,t_i as in Lemma ", but the DAG records no use.
sections/07-resampling.tex:416
infoinferred_dep
lemPacked selected-bit XOR on grouped streams
critique: The lemma statement (sections/11-grouped-rectangles.tex:63-64) opens with "Let a valid grouped packed stream of Definition  be supplied", but the DAG has no edge to the definition, which therefore shows up as an orphan.
sections/11-grouped-rectangles.tex:61
infoinferred_dep
claimRounded reciprocal Newton step residual bound
outline: "Rounded reciprocal Newton step residual bound" rests on claim-cor-exact-arithmetic-1
sections/09-exact-arithmetic.tex:27
infoinferred_dep
claimCapped doubling gives reciprocal to precision
outline: "Capped doubling gives reciprocal to target precision" rests on claim-cor-exact-arithmetic-2
sections/09-exact-arithmetic.tex:48
infoinferred_dep
claimRounded Newton square-root error analysis
outline: "Square-root Newton iteration error analysis" rests on claim-cor-exact-arithmetic-3
sections/09-exact-arithmetic.tex:62
infoinferred_dep
claimNewton routines cost O(B(p)) on fixed tapes
outline: "Newton routines cost O(B(p)) on fixed tapes" rests on claim-cor-exact-arithmetic-3
sections/09-exact-arithmetic.tex:92
infoinferred_dep
claimNewton routines cost O(B(p)) on fixed tapes
outline: "Newton routines cost O(B(p)) on fixed tapes" rests on claim-cor-exact-arithmetic-4
sections/09-exact-arithmetic.tex:92
infoinferred_dep
claimExact quotient and root by correction tests
outline: "Exact quotient and root by correction tests" rests on claim-cor-exact-arithmetic-3
sections/09-exact-arithmetic.tex:129
infoinferred_dep
claimExact quotient and root by correction tests
outline: "Exact quotient and root by correction tests" rests on claim-cor-exact-arithmetic-4
sections/09-exact-arithmetic.tex:129
infoinferred_dep
claimExact quotient and root by correction tests
outline: "Exact quotient and root by correction tests" rests on claim-cor-exact-arithmetic-5
sections/09-exact-arithmetic.tex:129
infoinferred_dep
claimExact quotient and root by correction tests
outline: "Exact quotient and root by correction tests" rests on thm:main
sections/09-exact-arithmetic.tex:129
infoinferred_dep
claimTelescoping dimension changes gives rank budget
outline: "Telescoping dimension changes gives rank budget" rests on claim-lem-motif-residuals-1
sections/03-motifs.tex:420
infoinferred_dep
claimNonzero binary residuals are nonalternating
outline: "Nonzero binary residuals are nonalternating" rests on claim-lem-motif-residuals-1
sections/03-motifs.tex:427
infoinferred_dep
claimNonalternating binary spaces have orthonormal bases
outline: "Nonalternating binary spaces have orthonormal bases" rests on claim-lem-motif-residuals-3
sections/03-motifs.tex:441
infoinferred_dep
claimKernel factorization extends to k columns
outline: "Kernel factorization extends to k columns" rests on claim-prop-complex-motif-interface-1
sections/03-motifs.tex:616
infoinferred_dep
claimRoute operators telescope to C^{⊗m}
outline: "Route operators from common-frame identity; C^{⊗m} on most roles" rests on claim-prop-complex-motif-interface-2
sections/03-motifs.tex:627
infoinferred_dep
claimZ corrections repair the X_a to Y_a route
outline: "Z sign corrections fix the X_a→Y_a route" rests on claim-prop-complex-motif-interface-3
sections/03-motifs.tex:644
infoinferred_dep
claimCircuit on role streams realizes shear
outline: "Circuit with shear frames yields H←H+D everywhere" rests on claim-prop-power-interchange-1
sections/04-swap.tex:158
infoinferred_dep
claimCircuit on role streams realizes shear
outline: "Circuit with shear frames yields H←H+D everywhere" rests on prop:bit-motif-interface
sections/04-swap.tex:158
infoinferred_dep
claimThree shears interchange the two chunks
outline: "Three shears interchange the two chunks" rests on claim-prop-power-interchange-2
sections/04-swap.tex:189
infoinferred_dep
claimThree shears interchange the two chunks
outline: "Three shears interchange the two chunks" rests on lem:ordered-affine-streams
sections/04-swap.tex:189
infoinferred_dep
claimRecurrence solves to O(e^τ) per volume
outline: "Volume-normalized recurrence gives O(e^τ)" rests on claim-prop-power-interchange-3
sections/04-swap.tex:197
infoinferred_dep
claimDepth-first fixed-tape schedule costs O(V)
outline: "Depth-first fixed-tape schedule costs O(V) per node" rests on claim-prop-power-interchange-4
sections/04-swap.tex:213
infoinferred_dep
claimDescriptor processing fits within child volume
outline: "Descriptor processing absorbed by child volume" rests on claim-prop-power-interchange-5
sections/04-swap.tex:244
infoinferred_dep
claimBase-m pieces via power-width interchanges
outline: "Base-m pieces via power-width interchanges cost O(Ve^τ)" rests on claim-lem-chunk-swap-1
sections/04-swap.tex:346
infoinferred_dep
claimPadding binary chunks to radix-q ranges
outline: "Binary chunks padded to radix-q ranges" rests on claim-lem-chunk-swap-2
sections/04-swap.tex:375
infoinferred_dep
claimPacked shifts match ideal XOR off bad set
outline: "Packed cyclic shifts agree with ideal XOR off bad set" rests on claim-lem-packed-selected-bit-rectangle-1
sections/05-layers.tex:292
infoinferred_dep
claimBad set is small and invariant
outline: "Bad set small and preserved by both maps" rests on claim-lem-packed-selected-bit-rectangle-2
sections/05-layers.tex:335
infoinferred_dep
claimRotations cost O(V L^τ) via swaps
outline: "Rotations implemented by swaps and controlled shifts" rests on claim-lem-packed-selected-bit-rectangle-2
sections/05-layers.tex:353
infoinferred_dep
claimRepair exceptional records by sorting
outline: "Deterministic repair by sorting exceptional records" rests on claim-lem-packed-selected-bit-rectangle-3
sections/05-layers.tex:395
infoinferred_dep
claimTotal cost and asymptotic simplification
outline: "Total cost and asymptotic simplification" rests on claim-lem-packed-selected-bit-rectangle-3
sections/05-layers.tex:433
infoinferred_dep
claimTotal cost and asymptotic simplification
outline: "Total cost and asymptotic simplification" rests on claim-lem-packed-selected-bit-rectangle-4
sections/05-layers.tex:433
infoinferred_dep
claimTotal cost and asymptotic simplification
outline: "Total cost and asymptotic simplification" rests on claim-lem-packed-selected-bit-rectangle-5
sections/05-layers.tex:433
infoinferred_dep
claimTotal cost and asymptotic simplification
outline: "Total cost and asymptotic simplification" rests on claim-lem-packed-selected-bit-rectangle-6
sections/05-layers.tex:433
infoinferred_dep
claimPacked basis changes cost uniformly near-linear
outline: "Packed basis changes cost uniformly linear-ish" rests on claim-prop-simultaneous-layer-1
sections/05-layers.tex:952
infoinferred_dep
claimRecurrence total cost and conversion to H
outline: "Recurrence gives O(Vd^λ') and converts C layer to H_0" rests on claim-prop-simultaneous-layer-2
sections/05-layers.tex:974
infoinferred_dep
claimRecurrence total cost and conversion to H
outline: "Recurrence gives O(Vd^λ') and converts C layer to H_0" rests on prop:complex-motif-interface
sections/05-layers.tex:974
infoinferred_dep
claimGuarded evaluation with single final truncation
outline: "Exact guarded evaluation and single truncation error" rests on claim-prop-simultaneous-layer-3
sections/05-layers.tex:979
infoinferred_dep
claimLayout permutation by moves and chunk exchanges
outline: "Construct layout permutation L by moves and exchanges" rests on lem:chunk-swap
sections/06-transforms.tex:233
infoinferred_dep
claimLayout permutation by moves and chunk exchanges
outline: "Construct layout permutation L by moves and exchanges" rests on lem:elementary-streams
sections/06-transforms.tex:233
infoinferred_dep
claimEach layout round meets layer hypotheses
outline: "Rounds on chunk groups meet simultaneous-layer hypotheses" rests on claim-lem-synthetic-transform-cost-1
sections/06-transforms.tex:300
infoinferred_dep
claimPrefix-slot rounds evaluated bit by bit
outline: "Prefix-slot rounds evaluated individually and exactly" rests on claim-lem-synthetic-transform-cost-1
sections/06-transforms.tex:348
infoinferred_dep
claimTwiddle rotations without coefficient sorting
outline: "Twiddle exponents and monomial as signed rotation" rests on claim-lem-synthetic-transform-cost-1
sections/06-transforms.tex:372
infoinferred_dep
claimOne truncation per round bounds error
outline: "One truncation per round gives ℓ error bound" rests on claim-lem-synthetic-transform-cost-3
sections/06-transforms.tex:400
infoinferred_dep
claimOne truncation per round bounds error
outline: "One truncation per round gives ℓ error bound" rests on claim-lem-synthetic-transform-cost-4
sections/06-transforms.tex:400
infoinferred_dep
claimOne truncation per round bounds error
outline: "One truncation per round gives ℓ error bound" rests on claim-lem-synthetic-transform-cost-5
sections/06-transforms.tex:400
infoinferred_dep
claimFull procedures include layout conjugation
outline: "Full procedures implement LBF^- and F^+B^{-1}L^{-1}" rests on claim-lem-synthetic-transform-cost-1
sections/06-transforms.tex:422
infoinferred_dep
claimFull procedures include layout conjugation
outline: "Full procedures implement LBF^- and F^+B^{-1}L^{-1}" rests on lem:synthetic-characters
sections/06-transforms.tex:422
infoinferred_dep
claimSigned carries give two's-complement blocks
outline: "Signed packing via bounded-carry blocks" rests on claim-lem-signed-ring-product-1
sections/06-transforms.tex:509
infoinferred_dep
claimCentered extraction recovers product coefficients
outline: "Centered extraction recovers product coefficients" rests on claim-lem-signed-ring-product-1
sections/06-transforms.tex:528
infoinferred_dep
claimCentered extraction recovers product coefficients
outline: "Centered extraction recovers product coefficients" rests on claim-lem-signed-ring-product-2
sections/06-transforms.tex:528
infoinferred_dep
claimNegacyclic reduction gives bounded coefficients
outline: "Negacyclic reduction and normalized product in disk" rests on claim-lem-signed-ring-product-3
sections/06-transforms.tex:573
infoinferred_dep
claimTruncation and output format of ring product
outline: "Truncation, output format and total cost" rests on claim-lem-signed-ring-product-4
sections/06-transforms.tex:594
infoinferred_dep
claimExact normalization identity via retained order
outline: "Exact normalization identity via retained order" rests on lem:synthetic-transform-cost
sections/06-transforms.tex:657
infoinferred_dep
claimExact normalization identity via retained order
outline: "Exact normalization identity via retained order" rests on lem:synthetic-characters
sections/06-transforms.tex:657
infoinferred_dep
claimError bound and disk margin
outline: "Error bound √2M(3ℓ+1)2^{-p} and disk margin" rests on claim-prop-synthetic-convolution-1
sections/06-transforms.tex:685
infoinferred_dep
claimError bound and disk margin
outline: "Error bound √2M(3ℓ+1)2^{-p} and disk margin" rests on lem:synthetic-transform-cost
sections/06-transforms.tex:685
infoinferred_dep
claimExact power-of-two scaling and output format
outline: "Exact power-of-two scaling and output format" rests on claim-prop-synthetic-convolution-1
sections/06-transforms.tex:720
infoinferred_dep
claimTotal cost of transforms and products
outline: "Total cost of transforms and products" rests on lem:synthetic-transform-cost
sections/06-transforms.tex:733
infoinferred_dep
claimTotal cost of transforms and products
outline: "Total cost of transforms and products" rests on lem:signed-ring-product
sections/06-transforms.tex:733
infoinferred_dep
claimOrdered approximations with error and time bounds
outline: "Ordered numerical maps and selection error bounds" rests on claim-lem-no-sort-resampling-1
sections/07-resampling.tex:149
infoinferred_dep
claimTape movement and Neumann iteration bounds
outline: "Tape movement and Neumann iteration bounds" rests on claim-lem-no-sort-resampling-2
sections/07-resampling.tex:246
infoinferred_dep
claimTensor identity and axis-by-axis implementation
outline: "Tensor identity and linewise expansion/compression" rests on lem:no-sort-resampling
sections/07-resampling.tex:342
infoinferred_dep
claimAxis maps contract with error dp^2
outline: "Axis maps contract; error dp^2 and line cost" rests on claim-lem-tensor-resampling-1
sections/07-resampling.tex:362
infoinferred_dep
claimAxis maps contract with error dp^2
outline: "Axis maps contract; error dp^2 and line cost" rests on lem:no-sort-resampling
sections/07-resampling.tex:362
infoinferred_dep
claimEach group collapses to a single rectangle
outline: "Each group collapses to a single rectangle" rests on claim-lem-packed-selected-bit-addition-1
sections/11-grouped-rectangles.tex:101
infoinferred_dep
claimGroup-by-group processing on fixed tapes
outline: "Group-by-group processing on fixed local tapes" rests on claim-lem-packed-selected-bit-addition-2
sections/11-grouped-rectangles.tex:123
infoinferred_dep
claimSumming group costs gives total time
outline: "Summing local rectangle bounds gives the time" rests on claim-lem-packed-selected-bit-addition-2
sections/11-grouped-rectangles.tex:133
infoinferred_dep
claimSumming group costs gives total time
outline: "Summing local rectangle bounds gives the time" rests on claim-lem-packed-selected-bit-addition-3
sections/11-grouped-rectangles.tex:133
infoinferred_dep
claimFixed exponents satisfy all parameter conditions
outline: "Fixed rational exponents satisfy all conditions" rests on prop:simultaneous-layer
sections/08-assembly.tex:16
infoinferred_dep
claimTransform sizes and precision satisfy band bounds
outline: "Transform sizes and precision satisfy band bounds" rests on claim-thm-main-1
sections/08-assembly.tex:50
infoinferred_dep
claimDistinct primes meet resampling hypotheses
outline: "Distinct prime source lengths meet resampling hypotheses" rests on claim-thm-main-2
sections/08-assembly.tex:115
infoinferred_dep
claimDistinct primes meet resampling hypotheses
outline: "Distinct prime source lengths meet resampling hypotheses" rests on lem:no-sort-resampling
sections/08-assembly.tex:115
infoinferred_dep
claimDistinct primes meet resampling hypotheses
outline: "Distinct prime source lengths meet resampling hypotheses" rests on lem:tensor-resampling
sections/08-assembly.tex:115
infoinferred_dep
claimCRT address map via controlled shifts
outline: "CRT address map via triangular controlled shifts" rests on claim-thm-main-3
sections/08-assembly.tex:207
infoinferred_dep
claimCRT address map via controlled shifts
outline: "CRT address map via triangular controlled shifts" rests on lem:ordered-affine-streams
sections/08-assembly.tex:207
infoinferred_dep
claimCRT address map via controlled shifts
outline: "CRT address map via triangular controlled shifts" rests on lem:chunk-swap
sections/08-assembly.tex:207
infoinferred_dep
claimComplex convolution via coefficient twist
outline: "Complex cyclic convolution via coefficient twist" rests on prop:synthetic-convolution
sections/08-assembly.tex:310
infoinferred_dep
claimComplex convolution via coefficient twist
outline: "Complex cyclic convolution via coefficient twist" rests on lem:synthetic-transform-cost
sections/08-assembly.tex:310
infoinferred_dep
claimComplex convolution via coefficient twist
outline: "Complex cyclic convolution via coefficient twist" rests on lem:signed-ring-product
sections/08-assembly.tex:310
infoinferred_dep
claimChirp transform and source transform procedures
outline: "Chirp and source-transform procedures" rests on claim-thm-main-5
sections/08-assembly.tex:427
infoinferred_dep
claimChirp transform and source transform procedures
outline: "Chirp and source-transform procedures" rests on lem:chirp-permutation
sections/08-assembly.tex:427
infoinferred_dep
claimChirp transform and source transform procedures
outline: "Chirp and source-transform procedures" rests on lem:tensor-resampling
sections/08-assembly.tex:427
infoinferred_dep
claimTwo scalings by S undo normalizations
outline: "Multiplication algorithm and normalization bookkeeping" rests on claim-thm-main-4
sections/08-assembly.tex:498
infoinferred_dep
claimTwo scalings by S undo normalizations
outline: "Multiplication algorithm and normalization bookkeeping" rests on claim-thm-main-6
sections/08-assembly.tex:498
infoinferred_dep
claimTwo scalings by S undo normalizations
outline: "Multiplication algorithm and normalization bookkeeping" rests on lem:chirp-permutation
sections/08-assembly.tex:498
infoinferred_dep
claimDisk margins and error propagation through transforms
outline: "Disk margins and error propagation through transforms" rests on claim-thm-main-5
sections/08-assembly.tex:558
infoinferred_dep
claimDisk margins and error propagation through transforms
outline: "Disk margins and error propagation through transforms" rests on claim-thm-main-6
sections/08-assembly.tex:558
infoinferred_dep
claimDisk margins and error propagation through transforms
outline: "Disk margins and error propagation through transforms" rests on prop:synthetic-convolution
sections/08-assembly.tex:558
infoinferred_dep
claimDisk margins and error propagation through transforms
outline: "Disk margins and error propagation through transforms" rests on lem:synthetic-transform-cost
sections/08-assembly.tex:558
infoinferred_dep
claimDisk margins and error propagation through transforms
outline: "Disk margins and error propagation through transforms" rests on prop:simultaneous-layer
sections/08-assembly.tex:558
infoinferred_dep
claimDisk margins and error propagation through transforms
outline: "Disk margins and error propagation through transforms" rests on lem:tensor-resampling
sections/08-assembly.tex:558
infoinferred_dep
claimFinal error below 1/2; rounding and carries exact
outline: "Final error below 1/2, rounding and carries exact" rests on claim-thm-main-8
sections/08-assembly.tex:677
infoinferred_dep
claimFinal error below 1/2; rounding and carries exact
outline: "Final error below 1/2, rounding and carries exact" rests on claim-thm-main-7
sections/08-assembly.tex:677
infoinferred_dep
claimFinal error below 1/2; rounding and carries exact
outline: "Final error below 1/2, rounding and carries exact" rests on lem:chirp-permutation
sections/08-assembly.tex:677
infoinferred_dep
claimFinal error below 1/2; rounding and carries exact
outline: "Final error below 1/2, rounding and carries exact" rests on lem:signed-ring-product
sections/08-assembly.tex:677
infoinferred_dep
claimCost table yields the final time bound
outline: "Cost table gives O(n(lg n)^{1-κ})" rests on claim-thm-main-1
sections/08-assembly.tex:820
infoinferred_dep
claimCost table yields the final time bound
outline: "Cost table gives O(n(lg n)^{1-κ})" rests on lem:synthetic-transform-cost
sections/08-assembly.tex:820
infoinferred_dep
claimCost table yields the final time bound
outline: "Cost table gives O(n(lg n)^{1-κ})" rests on prop:simultaneous-layer
sections/08-assembly.tex:820
infoinferred_dep
claimCost table yields the final time bound
outline: "Cost table gives O(n(lg n)^{1-κ})" rests on lem:chunk-swap
sections/08-assembly.tex:820
infoinferred_dep
claimCost table yields the final time bound
outline: "Cost table gives O(n(lg n)^{1-κ})" rests on prop:power-interchange
sections/08-assembly.tex:820
infoinferred_dep
claimCost table yields the final time bound
outline: "Cost table gives O(n(lg n)^{1-κ})" rests on lem:packed-selected-bit-rectangle
sections/08-assembly.tex:820
infoinferred_dep
claimCost table yields the final time bound
outline: "Cost table gives O(n(lg n)^{1-κ})" rests on lem:tensor-resampling
sections/08-assembly.tex:820
infoinferred_dep
claimCost table yields the final time bound
outline: "Cost table gives O(n(lg n)^{1-κ})" rests on claim-thm-main-4
sections/08-assembly.tex:820
infoinferred_dep
claimCost table yields the final time bound
outline: "Cost table gives O(n(lg n)^{1-κ})" rests on claim-thm-main-9
sections/08-assembly.tex:820