Friction report

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

paper statements

3

Lean declarations (Phase 2)

—

aligned pairs

—

friction items

12

Severity	Kind	Node	Note	Source
warn	`unresolved_ref`	lemLifting lemma: polynomial algebra over B	The key expansion at lines 186–189 uses the universal polynomial S defined in equation eq:xyz, outside the skeleton statements.	paper.tex:164
warn	`structure_uncertain`	claimCusp and translation identities	critique: Split after paper.tex:258: lines 255–258 establish the cusp identity, while lines 259–267 independently establish the formal translation identity. Later claims use these identities separately (claim-thm-main-3 uses the cusp identity; claim-thm-main-2 uses the translation).	paper.tex:255
info	`inferred_dep`	claimRemaining equations are compatible and unimodular	outline: "Remaining equations are compatible and unimodular" rests on claim-lem-lift-1	paper.tex:197
info	`inferred_dep`	claimCompatible solution eliminates the variable W	outline: "Compatible solution eliminates the variable W" rests on claim-lem-lift-2	paper.tex:210
info	`inferred_dep`	claimCompatible solution eliminates the variable W	critique: The conclusion $C\cong A$ at paper.tex:224–225 explicitly invokes , established in claim-lem-lift-1 at lines 193–195. Compatibility alone does not supply that presentation.	paper.tex:210
info	`inferred_dep`	claimExplicit parameter identifies A with B[T]	outline: "Explicit parameter trivializes the remaining algebra" rests on claim-lem-lift-1	paper.tex:227
info	`inferred_dep`	claimExplicit parameter identifies A with B[T]	outline: "Explicit parameter trivializes the remaining algebra" rests on claim-lem-lift-3	paper.tex:227
info	`inferred_dep`	claimBase algebra is a polynomial ring	outline: "Translation makes the auxiliary base polynomial" rests on claim-thm-main-1	paper.tex:269
info	`inferred_dep`	claimUnit ideal gives affine three-space fibre	outline: "Unit ideal permits lifting the fibre presentation" rests on claim-thm-main-1	paper.tex:288
info	`inferred_dep`	claimUnit ideal gives affine three-space fibre	outline: "Unit ideal permits lifting the fibre presentation" rests on claim-thm-main-2	paper.tex:288
info	`inferred_dep`	claimAmbient identity gives critical point	outline: "Ambient identity yields a critical point" rests on claim-thm-main-1	paper.tex:306
info	`inferred_dep`	claimVanishing gradient excludes coordinate	outline: "Jacobian invertibility rules out a coordinate" rests on claim-thm-main-4	paper.tex:324