Friction report

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

paper statements

Lean declarations (Phase 2)

—

aligned pairs

—

friction items

Severity	Kind	Node	Note	Source
warn	`unresolved_ref`	lemUniform spectral gap for affine group actions	The spectral gap rests on external property (T) results of Shalom (Theorems 2.1, 2.6, Corollary 2.3), not on skeleton statements.	sections/averaging.tex:32
warn	`unresolved_ref`	lemExponentially mixing averaging operator on conditional space	L_s contraction uses the external Riesz–Thorin interpolation theorem.	sections/averaging.tex:108
info	`inferred_dep`	lemColumn test separates heavy and light columns	critique: The proof (hierarchy.tex 355, 375-376) applies Equations hier-sampling-pair and hier-sampling-tail. The text introduces these as "The consequences of Lemma needed here" (lines 185-195).	sections/hierarchy.tex:314
info	`inferred_dep`	lemResidual matrix D is bounded and dominating	critique: The proof of lem:hier-residual (hierarchy.tex 471-479) uses "the fixed point with this same multiplier g" and "Equation gives Δ(x,y)≤q^{-1}f/32". Both come from Lemma 4.1, and the statement also cites the k_* chosen there, but no edge exists.	sections/hierarchy.tex:411
info	`structure_uncertain`	lemWalk variants avoid storing endpoints	Proof forward-references thm:ctrl-realization for space accounting of nested restoration; this is a forward pointer, not a logical dependency.	sections/averaging.tex:180
info	`inferred_dep`	lemMean prefixes are small against targets	"the child bound remains valid" / "Equation is then bounded by" uses the mean-comparison bound for a budget-m sample term against true stochastic inputs	sections/estimation.tex:538
info	`structure_uncertain`	lemClean calculation is independent of the salt	lem:fp-clean cites lem:ctrl-replay for the salt-access implementation, while lem:ctrl-replay's proof cites lem:fp-clean; the reference is mutual rather than a strict dependency order.	sections/fingerprints.tex:202
info	`inferred_dep`	lemCapped incoming ports give restoring paired motions	critique: The proof of lem:ctrl-cap (implementation.tex 510-539) is built on contour marks: "go forward toward the sentinel, counting other initiation marks" and "inverse maps by the common contour order". These are the next-mark/previous-mark operations of lem:ctrl-tour, which has no incoming edge from cap.	sections/implementation.tex:493
info	`inferred_dep`	lemControl records replay with later-salt independence	critique: lem:ctrl-replay states that the records "are regenerable in the sense of Definition " (implementation.tex 1087-1088). The definition is currently an orphan.	sections/implementation.tex:1086
info	`inferred_dep`	corPromise BPL equals promise L	critique: The proof of cor:promise-bpl (conclusion.tex 315-318) reads "The same $d=3$ approximation and threshold $1/2$ used in the preceding proof". That is an application of Theorem fixed-precision, but the corollary has no uses.	sections/conclusion.tex:309
info	`structure_uncertain`	thmEffective compiler from randomized to deterministic logspace	The proof environment is only a 25-line 'Completion'; the substantive argument is spread over Sections 13.2–13.5 (compiler.tex 193–530), outlined here under this label.	sections/compiler.tex:8
info	`structure_uncertain`	thmEffective compiler from randomized to deterministic logspace	claim "Fixed deterministic library separating interpreter thresholds" (sections/compiler.tex:193-251) lies outside the recorded proof; a second proof or an appendix	sections/compiler.tex:8
info	`structure_uncertain`	thmEffective compiler from randomized to deterministic logspace	claim "Padding preserves acceptance probability exactly" (sections/compiler.tex:256-312) lies outside the recorded proof; a second proof or an appendix	sections/compiler.tex:8
info	`structure_uncertain`	thmEffective compiler from randomized to deterministic logspace	claim "Callback compiles virtual padded input reads" (sections/compiler.tex:353-429) lies outside the recorded proof; a second proof or an appendix	sections/compiler.tex:8
info	`structure_uncertain`	thmEffective compiler from randomized to deterministic logspace	claim "Simultaneous work-space bound for all tapes" (sections/compiler.tex:452-471) lies outside the recorded proof; a second proof or an appendix	sections/compiler.tex:8
info	`structure_uncertain`	thmEffective compiler from randomized to deterministic logspace	claim "Bit-time bound by configuration counting" (sections/compiler.tex:473-530) lies outside the recorded proof; a second proof or an appendix	sections/compiler.tex:8
info	`inferred_dep`	claimResidual nonnegative with bounded row support	outline: "Fixed-point residual nonnegative, bounded row support" rests on claim-lem-hier-fixed-point-1	sections/hierarchy.tex:111
info	`inferred_dep`	claimEntry bound via increasing support sequences	outline: "Entry bound via increasing support sequences" rests on claim-lem-hier-fixed-point-2	sections/hierarchy.tex:127
info	`inferred_dep`	claimFactorial decay of iteration differences	outline: "Factorial decay of iteration differences" rests on claim-lem-hier-fixed-point-2	sections/hierarchy.tex:151
info	`inferred_dep`	claimFactorial decay of iteration differences	outline: "Factorial decay of iteration differences" rests on claim-lem-hier-fixed-point-3	sections/hierarchy.tex:151
info	`inferred_dep`	claimDistance to full invariant subspace bounded	outline: "Distance to full invariant subspace bounded" rests on claim-lem-env-affine-1	sections/averaging.tex:74
info	`inferred_dep`	claimSpectral gap on finite transitive actions	outline: "Spectral gap on finite transitive actions" rests on claim-lem-env-affine-2	sections/averaging.tex:91
info	`inferred_dep`	claimSource-release cost f/u via incoming cap	outline: "Source-release cost f/u via incoming cap" rests on claim-lem-est-mean-comparison-1	sections/estimation.tex:258
info	`inferred_dep`	claimFine bin scale cost by early reconditioning	outline: "Fine bin cost (b/a)^{s-1} by early reconditioning" rests on claim-lem-est-mean-comparison-2	sections/estimation.tex:297
info	`inferred_dep`	claimSecond channel, detector and reward comparisons	outline: "Second channel, detector and reward comparisons" rests on claim-lem-est-mean-comparison-2	sections/estimation.tex:312
info	`inferred_dep`	claimMany heavy entries close all gates	outline: "Many heavy true entries close all gates" rests on claim-lem-buf-relative-stability-1	sections/compression.tex:328
info	`inferred_dep`	claimSentinel modification gives Lipschitz propagation bound	outline: "Sentinel modification gives Lipschitz propagation bound" rests on claim-lem-buf-relative-stability-1	sections/compression.tex:341
info	`inferred_dep`	claimSentinels leave perturbed calculation unchanged	outline: "Sentinels do not change perturbed calculation" rests on claim-lem-buf-relative-stability-3	sections/compression.tex:365
info	`inferred_dep`	claimPreloss and no-overflow error bounds	outline: "Preloss and no-overflow contributions" rests on lem:buf-reference	sections/compression.tex:491
info	`inferred_dep`	claimPreloss and no-overflow error bounds	outline: "Preloss and no-overflow contributions" rests on claim-prop-buf-error-1	sections/compression.tex:491
info	`inferred_dep`	claimFalse-type first overflow charge bound	outline: "False-type first overflow charge" rests on claim-prop-buf-error-1	sections/compression.tex:498
info	`inferred_dep`	claimTrue-type overflow mean part via rarity	outline: "True-type overflow mean part via rarity" rests on lem:buf-rarity	sections/compression.tex:508
info	`inferred_dep`	claimNoise part needs no sum over overflow groups	outline: "Noise part via uniqueness of first overflow" rests on lem:buf-relative-stability	sections/compression.tex:518
info	`inferred_dep`	claimFloor and capacity exponents make sums converge	outline: "Choice of floor and capacity exponents converges" rests on claim-prop-buf-error-2	sections/compression.tex:536
info	`inferred_dep`	claimFloor and capacity exponents make sums converge	outline: "Choice of floor and capacity exponents converges" rests on claim-prop-buf-error-3	sections/compression.tex:536
info	`inferred_dep`	claimFloor and capacity exponents make sums converge	outline: "Choice of floor and capacity exponents converges" rests on claim-prop-buf-error-4	sections/compression.tex:536
info	`inferred_dep`	claimFloor and capacity exponents make sums converge	outline: "Choice of floor and capacity exponents converges" rests on claim-prop-buf-error-5	sections/compression.tex:536
info	`inferred_dep`	claimEscape indicator bounded by witness discrepancy	outline: "Escape indicator bounded by witness discrepancy" rests on lem:atom-ports	sections/fingerprints.tex:368
info	`inferred_dep`	claimOutput error dominated by row-failure indicator	outline: "Output error dominated by row-failure indicator" rests on claim-lem-fp-escape-1	sections/fingerprints.tex:380
info	`inferred_dep`	claimRight-factor charge via actual incoming cap	outline: "Right-factor charge via actual incoming cap" rests on claim-lem-fp-escape-1	sections/fingerprints.tex:388
info	`inferred_dep`	claimDirect and left offending ports charged	outline: "Direct and left offending ports charged" rests on claim-lem-fp-escape-1	sections/fingerprints.tex:419
info	`inferred_dep`	claimPrecision gain absorbs scale and reset costs	outline: "Precision gain absorbs scale and reset costs" rests on claim-lem-fp-escape-3	sections/fingerprints.tex:430
info	`inferred_dep`	claimPrecision gain absorbs scale and reset costs	outline: "Precision gain absorbs scale and reset costs" rests on claim-lem-fp-escape-4	sections/fingerprints.tex:430
info	`inferred_dep`	claimPropagated clean height has small row norm	outline: "Propagated clean height H_x bounded" rests on claim-lem-fp-direct-1	sections/fingerprints.tex:555
info	`inferred_dep`	claimCollision gain via conditioning on clean sigma-field	outline: "Conditioning on clean sigma-field gives collision gain" rests on lem:fp-envelope	sections/fingerprints.tex:577
info	`inferred_dep`	claimCollision gain via conditioning on clean sigma-field	outline: "Conditioning on clean sigma-field gives collision gain" rests on claim-lem-fp-direct-2	sections/fingerprints.tex:577
info	`inferred_dep`	claimRemaining terms bounded by child discrepancies	outline: "Remaining terms bounded by child discrepancies" rests on lem:fp-buckets	sections/fingerprints.tex:599
info	`inferred_dep`	claimClean active tasks meet target bounds	outline: "Clean active target bounds within induction" rests on lem:est-prefix	sections/fingerprints.tex:630
info	`inferred_dep`	claimCoupling recurrence from child charges	outline: "Coupling recurrence from escape, collision, assembly" rests on lem:fp-buckets	sections/fingerprints.tex:641
info	`inferred_dep`	claimConstants chosen to close coupling recurrence	outline: "Choosing D2, D1, epsilon closes recurrence" rests on claim-prop-fp-coupling-2	sections/fingerprints.tex:675
info	`inferred_dep`	claimCoupling plus clean bound gives target	outline: "Coupling plus clean bound gives target" rests on claim-prop-fp-coupling-1	sections/fingerprints.tex:693
info	`inferred_dep`	claimCoupling plus clean bound gives target	outline: "Coupling plus clean bound gives target" rests on claim-prop-fp-coupling-3	sections/fingerprints.tex:693
info	`inferred_dep`	claimOrder of constant choices is consistent	outline: "Order of constant choices is consistent" rests on claim-prop-fp-coupling-3	sections/fingerprints.tex:703
info	`inferred_dep`	claimBand recursion yields approximation integer	outline: "Band recursion gives approximation integers" rests on claim-lem-arith-multiplication-1	sections/arithmetic.tex:299
info	`inferred_dep`	claimSigned floor shifts preserve residues	outline: "Residue implementation with signed floor shifts" rests on claim-lem-arith-multiplication-2	sections/arithmetic.tex:329
info	`inferred_dep`	claimGate indexing and adder trees per band	outline: "Gate indexing and adder trees per band" rests on claim-lem-arith-multiplication-3	sections/arithmetic.tex:359
info	`inferred_dep`	claimClock gap pays band path length	outline: "Clock gap pays band path length" rests on claim-lem-arith-multiplication-4	sections/arithmetic.tex:382
info	`inferred_dep`	claimClipped reciprocal approximation has exact streams	outline: "Exact stream via elementary ops and multiplication" rests on claim-lem-arith-reciprocal-1	sections/arithmetic.tex:458
info	`inferred_dep`	claimEarly-word payment at early input places	outline: "Early-word payment at early input places" rests on claim-lem-arith-reciprocal-3	sections/arithmetic.tex:506
info	`inferred_dep`	claimSuffix branch holds no coefficient word	outline: "Suffix branch holds no coefficient word" rests on lem:arith-elementary	sections/arithmetic.tex:518
info	`inferred_dep`	claimSuffix branch holds no coefficient word	outline: "Suffix branch holds no coefficient word" rests on lem:arith-multiplication	sections/arithmetic.tex:518
info	`inferred_dep`	claimSuffix branch holds no coefficient word	outline: "Suffix branch holds no coefficient word" rests on claim-lem-arith-reciprocal-4	sections/arithmetic.tex:518
info	`inferred_dep`	claimOne clock coefficient works throughout	outline: "Common clock coefficient telescopes record bound" rests on lem:arith-elementary	sections/arithmetic.tex:798
info	`inferred_dep`	claimOne clock coefficient works throughout	outline: "Common clock coefficient telescopes record bound" rests on lem:arith-multiplication	sections/arithmetic.tex:798
info	`inferred_dep`	claimOne clock coefficient works throughout	outline: "Common clock coefficient telescopes record bound" rests on lem:arith-rank	sections/arithmetic.tex:798
info	`inferred_dep`	claimClock invariant bounds shared facilities	outline: "Clock invariant bounds shared facilities" rests on def:ctrl-allowance	sections/implementation.tex:1316
info	`inferred_dep`	claimClock invariant bounds shared facilities	outline: "Clock invariant bounds shared facilities" rests on claim-thm-ctrl-realization-5	sections/implementation.tex:1316
info	`inferred_dep`	claimPredecessors of local edits and branches	outline: "Predecessors of local edits and branches" rests on claim-lem-ctrl-local-graph-1	sections/implementation.tex:361
info	`inferred_dep`	claimCursor-step predecessors via paired inverse	outline: "Cursor-step predecessors via paired inverse" rests on claim-lem-ctrl-local-graph-1	sections/implementation.tex:371
info	`inferred_dep`	claimCanonical case codes give local incidence order	outline: "Canonical case codes give local incidence order" rests on claim-lem-ctrl-local-graph-2	sections/implementation.tex:398
info	`inferred_dep`	claimCanonical case codes give local incidence order	outline: "Canonical case codes give local incidence order" rests on claim-lem-ctrl-local-graph-3	sections/implementation.tex:398
info	`inferred_dep`	claimProbe copies fit enlarged A,D bound	outline: "Probe copies fit enlarged A,D bound" rests on def:ctrl-allowance	sections/implementation.tex:405
info	`inferred_dep`	claimProbe copies fit enlarged A,D bound	outline: "Probe copies fit enlarged A,D bound" rests on claim-lem-ctrl-local-graph-1	sections/implementation.tex:405
info	`inferred_dep`	claimScoring program assembles short suffix only	outline: "Scoring program assembles short suffix only" rests on claim-lem-ctrl-score-rank-1	sections/implementation.tex:592
info	`inferred_dep`	claimDecreasing-value contour tours count rank	outline: "Decreasing-value contour tours count rank" rests on lem:ctrl-tour	sections/implementation.tex:607
info	`inferred_dep`	claimDecreasing-value contour tours count rank	outline: "Decreasing-value contour tours count rank" rests on claim-lem-ctrl-score-rank-2	sections/implementation.tex:607
info	`inferred_dep`	claimOrder statistic accuracy and inverse-probe bounds	outline: "Order statistic accuracy and inverse-probe bounds" rests on claim-lem-ctrl-score-rank-1	sections/implementation.tex:627
info	`inferred_dep`	claimOrder statistic accuracy and inverse-probe bounds	outline: "Order statistic accuracy and inverse-probe bounds" rests on claim-lem-ctrl-score-rank-3	sections/implementation.tex:627
info	`inferred_dep`	claimRanks, compression and list selection	outline: "Ranks, compression and list selection" rests on claim-lem-ctrl-recipes-2	sections/implementation.tex:867
info	`inferred_dep`	claimFinite acyclic stratum ordering within group	outline: "Finite acyclic stratum ordering within group" rests on claim-lem-ctrl-recipes-2	sections/implementation.tex:969
info	`inferred_dep`	claimFinite acyclic stratum ordering within group	outline: "Finite acyclic stratum ordering within group" rests on claim-lem-ctrl-recipes-3	sections/implementation.tex:969
info	`inferred_dep`	claimUniform generation and arithmetic record bounds	outline: "Uniform generation and arithmetic record bounds" rests on claim-lem-ctrl-recipes-5	sections/implementation.tex:1047
info	`inferred_dep`	claimSalt permissions give later-salt independence	outline: "Salt permissions make lower structure later-salt independent" rests on claim-lem-ctrl-replay-2	sections/implementation.tex:1134
info	`inferred_dep`	claimTruncated digits give accurate dyadic values	outline: "Truncated digits give dyadic accurate values" rests on claim-thm-fixed-precision-1	sections/conclusion.tex:194
info	`inferred_dep`	claimTruncated digits give accurate dyadic values	outline: "Truncated digits give dyadic accurate values" rests on claim-thm-fixed-precision-2	sections/conclusion.tex:194
info	`inferred_dep`	claimBinary-search median is accurate	outline: "Binary-search median is accurate" rests on claim-thm-fixed-precision-3	sections/conclusion.tex:230
info	`inferred_dep`	claimBinary-search median is accurate	outline: "Binary-search median is accurate" rests on claim-thm-fixed-precision-4	sections/conclusion.tex:230
info	`inferred_dep`	claimTransducer runs in polynomial time	outline: "Polynomial time by configuration counting" rests on claim-thm-fixed-precision-6	sections/conclusion.tex:264
info	`inferred_dep`	claimFixed deterministic library decides interpreter promise	outline: "Fixed deterministic library separating interpreter thresholds" rests on thm:fixed-precision	sections/compiler.tex:193
info	`inferred_dep`	claimFixed deterministic library decides interpreter promise	outline: "Fixed deterministic library separating interpreter thresholds" rests on lem:compiler-interpreter	sections/compiler.tex:193
info	`inferred_dep`	claimFixed deterministic library decides interpreter promise	outline: "Fixed deterministic library separating interpreter thresholds" rests on cor:promise-bpl	sections/compiler.tex:193
info	`inferred_dep`	claimPadding preserves acceptance probability exactly	outline: "Padding preserves acceptance probability exactly" rests on lem:compiler-interpreter	sections/compiler.tex:256
info	`inferred_dep`	claimCallback compiles virtual padded input reads	outline: "Callback compiles virtual padded input reads" rests on claim-thm-effective-simulation-1	sections/compiler.tex:353
info	`inferred_dep`	claimCallback compiles virtual padded input reads	outline: "Callback compiles virtual padded input reads" rests on claim-thm-effective-simulation-2	sections/compiler.tex:353
info	`inferred_dep`	claimSimultaneous work-space bound on all tapes	outline: "Simultaneous work-space bound for all tapes" rests on claim-thm-effective-simulation-1	sections/compiler.tex:452
info	`inferred_dep`	claimSimultaneous work-space bound on all tapes	outline: "Simultaneous work-space bound for all tapes" rests on claim-thm-effective-simulation-3	sections/compiler.tex:452
info	`inferred_dep`	claimBit-time bound by configuration counting	outline: "Bit-time bound by configuration counting" rests on claim-thm-effective-simulation-4	sections/compiler.tex:473