# Completed page audit: Marcolli, Berwick, and Chomsky, *Syntax-Semantics Interface: An Algebraic Model*

Audit started: 2026-07-22
Audit completed: 2026-07-22

## Source identity and protocol

- Local source: `2311.06189v1.pdf`
- arXiv identifier: `2311.06189v1 [cs.CL]`, dated 10 November 2023.
- Authors: Matilde Marcolli, Robert C. Berwick, and Noam Chomsky.
- SHA-256: `ed4daccfdf3ebe31c21204ec5e0c3f3c857e00df93674920902115a6a9935fa9`
- Extent: 75 physical PDF pages, all with extractable text.
- Direct ordered reading is complete for all 75 pages. The embedded-image
  inventory was used to locate the figure pages. All 19 numbered figures were
  rendered and inspected on physical pages 22, 24, 31-35, 38-42, 61, and 66;
  the algebraic case tables on pages 15, 20, and 47 were also rendered and
  checked.

## Page-by-page matrix

| Physical page | Section | Content read or inspected | ProofNet-IR consequence |
|---:|---|---|---|
| 1 | abstract; contents | Proposed Hopf-algebra/Rota-Baxter model of the syntax-semantics interface and first half of the section map. | Adjacent algebraic motivation only; the abstract states no linear-logic theorem or proof-net experiment. |
| 2 | contents; §1 | Remaining section map and introduction of syntax/semantics modeling goals. | Establishes source scope and prevents importing section titles such as “Minimal Search” into MLL without checking their meaning. |
| 3 | §1 | Comparison of semantic models, syntax-first program, renormalization analogy, and LLM controversy motivation. | The physics analogy is explicitly a guiding heuristic, not evidence for proof-net correctness or performance. |
| 4 | §§1.1-1.2 | Four interface requirements, syntax as computation, semantics as proximity, and free symmetric Merge. | A different formal system with different syntax and semantics; no project theorem dependency. |
| 5 | §§1.2-1.2.1 | Binary rooted trees, accessible terms, Hopf algebra of workspaces, Merge action, and contraction-versus-deletion quotients. | Closely relevant representation vocabulary, but its quotient operations are not ProofNet-IR occurrence reindexing or sequentialization. |
| 6 | §1.2.2 | Operadic TAG composition versus the magma/Hopf-algebra structure of Merge on workspaces. | Demonstrates that similar tree operations can define genuinely different algebraic structures. |
| 7 | §1.3 | Abstract head functions and equivalence with inductive projection properties. | Partiality and occurrence-sensitive paths are useful design cautions; no MLL result. |
| 8 | §1.3 | Completion of the equivalence proof, many head choices, planar embeddings, and obstruction to a global head function. | A head/planarization choice is not canonical graph identity. |
| 9 | §§1.3-1.4 | Partial head functions motivate renormalization; Hopf algebra and Rota-Baxter roles are separated. | Explicitly distinguishes intrinsic combinatorics from an accessory target model. |
| 10 | §1.4 | Hopf algebra assumptions, Rota-Baxter algebra/semiring definitions, and characters. | Definitions are internal to the paper's framework and cannot justify the MLL checker. |
| 11 | §1.4 | Characters on semirings/cones, syntax-to-semantics interpretation, non-coalgebra morphism warning, and Birkhoff factorization. | Strong warning against equating a structure-preserving map at one layer with preservation of all structure. |
| 12 | §§1.4-1.5 | Recursive algebra/semiring Birkhoff factorizations and start of semantic-space requirements. | Recursion uses a graded connected Hopf algebra; it is not the proof-net splitting-tensor recursion. |
| 13 | §§1.5-1.5.1 | Consistency-across-substructures aim and contested versus established neuroscience analogies. | The paper itself labels part of the neuroscience motivation controversial and indirect. |
| 14 | §§1.5.2-1.5.3 | Semantic proximity, convexity, neighborhoods, vector/semiring models, and conceptual spaces. | Adjacent modeling vocabulary only. |
| 15 | §§1.5.3-2.1 | Syntax-induced semantic composition and first max-plus/ReLU toy model; rendered Rota-Baxter case table. | The model is explicitly a toy model; its ReLU computation is not an empirical proof-search result. |
| 16 | §2.1 | Semantic probes, a head-driven semiring character, and its extension to forests/cones. | Demonstrates a proposed evaluator over trees, not a certified MLL checker. |
| 17 | §2.1 | Limit of head-only semantics and Birkhoff searches over nested subforests. | The authors explicitly identify oversimplification; do not treat it as library validation. |
| 18 | §2.1 | Detailed ReLU factorization cases and bounds over accessible-term chains. | Algebraic selection property within the toy model only. |
| 19 | §§2.1-2.2 | Interpretation of positive substructures, rejection of the head-only model, and geodesic convexity. | Records the source's own limitation and transition to a richer model. |
| 20 | §§2.2.1-2.2.3 | Comparison functions, rendered threshold-operator table, and setup for a probability-semiring character. | No project dependency. |
| 21 | §2.2.3 | Recursive convex semantic assignment and proof that it defines a character. | A representation theorem under semantic-space assumptions, not arbitrary graph canonicalization. |
| 22 | §2.2.3 | Two induction choices and rendered Figure 1 comparing three sentence embeddings. | Visual audit confirms the proposed geometry; it remains an illustrative constructed example. |
| 23 | §§2.2.4-2.2.5 | Threshold Birkhoff factorization selects high-agreement accessible terms; higher-dimensional neighborhood proposal. | Selection is not focused sequent search and has no measured proof-net advantage. |
| 24 | §§2.2.5-2.3.1 | Rendered Vietoris-Rips example and start of vector/max-plus character construction. | Persistent-topology discussion is a proposed extension, not implemented evidence. |
| 25 | §§2.3.1-2.3.2 | Completion of vector character and linear-span/coefficient-semigroup property. | Background only. |
| 26 | §§2.3.2-2.4 | Hyperplane refinement, ReLU chain optimization, and rejection of tensor-product semantic composition. | Optimization is internal to accessible semantic subtrees, not proof search over MLL derivations. |
| 27 | §§2.4-2.5 | Critique of tensor-product models and Boolean truth-value character. | No proof-net result. |
| 28 | §§2.5-3 | Boolean example diagnoses locally meaningful substructures; syntax-image/inverse-problem thesis begins. | Useful distinction between local acceptance and global composition; not a switching theorem. |
| 29 | §3 | Construction of tree immersions/embeddings in a semantic manifold, with perturbations for collisions. | The result is assumption-heavy and not a canonical graph-isomorphism algorithm. |
| 30 | §§3-4.1 | Possible computational hardness of reconstructing syntax from its semantic image; moduli-space program and Externalization setup. | Directly warns that a forward embedding does not supply an efficient inverse. |
| 31 | §4.1 | Rendered Figure 3 separating free Merge, Externalization, semantic mapping, and combined process. | Visual audit reinforces separation of processing layers. |
| 32 | §§4.1-4.2 | Rendered Figure 4 mapping the two channels to associahedra, BHV spaces, and real-curve moduli; definitions begin. | Different quotient/moduli spaces make equivalence choice explicit. |
| 33 | §4.2 | Associahedra, degenerations, cubic decomposition, and rendered Figure 5. | Tree parenthesization geometry is adjacent only. |
| 34 | §4.2 | Rendered Figures 6-7: cubical associahedron decomposition and weighted planar tree to ordered points. | Confirms planar order and metric data are separate fields. |
| 35 | §4.2 | Rendered Figures 8-9: BHV tree space, compactification, and Petersen-graph link; origami projection count. | Abstract-tree moduli do not solve ProofNet-IR's chosen proof-net equivalence automatically. |
| 36 | §§4.2-4.3 | Generic fiber count, head-selected subcomplexes, and lift to a planar moduli space. | A lift depends on a head choice; it is not canonical under arbitrary renumbering. |
| 37 | §4.3 | Semantic proximity assigns internal-edge weights and yields partially defined sections. | Partial section with model-specific weights, not a total sequentializer. |
| 38 | §§4.3-4.5 | Rendered Figure 10, semantic embedding in moduli spaces, Externalization as a language-dependent section, and example setup. | Explicitly distinguishes semantic and language-dependent sections. |
| 39 | §4.5 | Rendered Figures 11-12 selecting an associahedron vertex and a BHV edge for a four-leaf example. | Visual example only. |
| 40 | §4.5 | Rendered Figures 13-14 assigning metric coordinates and lifting through a tiled associahedron. | Visual example only. |
| 41 | §4.5 | Rendered Figures 15-16 gluing associahedra into real-curve moduli/orientation cover. | Visual audit confirms the quotient geometry described in text. |
| 42 | §§4.5-4.6.1 | Rendered Figure 17 of origami folding, comparison of two sections, and Kayne LCA discussion. | Multiple preimages reinforce why a serialization representative is not an abstract identity theorem. |
| 43 | §§4.6.1-4.6.3 | Partial LCA algorithm, Cinque lexicon, and syntactic parameters as covering transformations. | Algorithms and transformations are language-specific and partial. |
| 44 | §§4.6.3-5.1 | Cross-language section comparison and introduction to semiring parsing for Merge. | “Parsing” here is not the ProofNet-IR JSON parser or MLL proof reconstruction. |
| 45 | §5.1 | Roadmap from Merge-derivation rings to bialgebroids, semiringoids, and factorization. | Source/target matching motivates categorical APIs, but supplies no code-level theorem. |
| 46 | §§5.1-5.2.1 | Directed-graph duality roadmap and four linguistic forms of Merge. | The paper's “Minimal Search” is defined over these Merge forms, not focused linear-logic search. |
| 47 | §§5.2.1-5.2.2 | Rendered workspace-size table separating External/Internal from Sideward/Countercyclic Merge and definition of the derivation algebra. | Critical terminology boundary: this table has no MLL connective or switching semantics. |
| 48 | §5.2.2 | Laurent-series Rota-Baxter projection and characters encoding weighted Merge derivations. | Background only. |
| 49 | §5.2.2 | Refined character detects unwanted intermediate Merge operations; simple projection is insufficient. | Shows why recursive correction can be stronger than output filtering, but only in its own model. |
| 50 | §§5.2.2-5.3 | Theorem 5.4 identifies linguistic Minimal Search with Birkhoff factorization; Hopf algebroid definition begins. | Must not be cited as proof-net sequentialization or focused-search completeness. |
| 51 | §5.3 | Hopf/bialgebroid axioms, grading, and construction from Merge workspaces/derivations. | Source/target composition is explicit; no current implementation dependency. |
| 52 | §§5.3-5.4.1 | Workspace coproduct encoding, algebroids as directed graph schemes, and graph-duality lemma. | Adjacent graph/category formalism only. |
| 53 | §§5.4.1-5.4.2 | Bialgebroids as reflexive/transitive graph schemes and Rota-Baxter algebroid definition/properties. | Paper's graph semantics differ from proof-net switching graphs. |
| 54 | §§5.4.2-5.4.3 | Projector/module consequences, graph-function examples, and semiringoid generalization. | Background only. |
| 55 | §§5.4.3-5.4.4 | Rota-Baxter semiringoid definition and Birkhoff factorization for algebroid morphisms. | Background only. |
| 56 | §5.4.4 | Directed-graph formulation of factorization and weighted diagrams of Merge derivations. | A graph diagram encodes derivation paths here; it is not a proof net. |
| 57 | §§5.4.4-5.5 | Semiringoid factorization and Boolean/probability/max-plus parsing of Merge derivations. | No benchmark or theorem about ProofNet-IR generation. |
| 58 | §§5.5-6 | Claimed unification of Merge semiring parsing and introduction to Pietroski compositional semantics. | Internal paper conclusion only. |
| 59 | §§6-6.1 | Pietroski Combine versus syntax-driven image of Merge; vision/pattern-theory comparison. | Different semantic problem domain. |
| 60 | §§6.1-6.1.2 | Geodesic realization of Combine, idempotents, and adjunct example setup. | A non-injective semantic map is explicitly allowed, unlike a certificate equivalence proof. |
| 61 | §6.1.2 | Rendered Figure 18 of adjunct semantic points and Boolean implication behavior. | Visual example reveals limitations of the simplified convex model. |
| 62 | §§6.2-6.2.1 | Predicate saturation, operad/algebra definitions, and syntactic objects as an algebra over free commutative binary Merge. | Operadic structure is conceptually adjacent, not the MLL sequent calculus. |
| 63 | §§6.2.2-6.2.3 | Partial operad algebra on semantics and proposition that syntax plus a map determines the semantic action. | Depends on a chosen partial map and one-point compactification; no project theorem. |
| 64 | §§6.2.3-6.3 | Proof of operad-action compatibility, acknowledged collision/ambiguity simplifications, and Pair-Merge problem. | The authors explicitly state model simplifications. |
| 65 | §6.3 | Adjunction outside head-function domain and proposed orientation in semantic space. | Partial-domain workaround, not a total algorithm. |
| 66 | §§6.3-7 | Rendered Figure 19 of two-peaked semantic structures and introduction to transformers as characters. | The figure exists only in the semantic image, not the syntactic magma; layer distinction is explicit. |
| 67 | §7 | Attention query/key/value algebra, unordered bidirectional setting, and disclaimer that efficiency is not analyzed. | Directly disallows using this paper as performance evidence for any ProofNet-IR experiment. |
| 68 | §§7-7.1 | Attention output, attention-head versus syntactic-head distinction, and a max-attention character. | Terminology is explicitly disambiguated; model relies on a chosen partial head function. |
| 69 | §§7.2-7.3 | Exact/approximate attention-detectability definitions and threshold factorization. | Empirical detectability is dataset/context relative, not a general theorem about proof graphs. |
| 70 | §§7.3-7.3.1 | Syntax-constrained attention character, failure localization, small-data limitations, and inverse-problem framing. | Suggests a possible experimental method but supplies no ProofNet-IR data. |
| 71 | §7.3.1 | Mixed prior neural-model findings, architecture dependence, physics metaphor, and computational-hardness conjecture. | The source calls the area contentious and offers an analogy, not a complexity proof. |
| 72 | conclusion; acknowledgments; references | LLMs as experimental apparatus rather than linguistic theory; acknowledgments and references 1-19. | Supports requiring theory-plus-evidence and not claiming model advantage prematurely. |
| 73 | references 20-50 | Sources on Hopf algebras, topology, grammar, neural syntax, and moduli spaces. | Bibliographic accounting only. |
| 74 | references 51-83 | Sources on operads, computation, semantic spaces, Merge, parsing, and language models. | Bibliographic accounting only. |
| 75 | references 84-86; affiliations | Final references and author affiliations/contact details. | Bibliographic/provenance accounting only. |

## Current claim boundary

All 75 pages and all 19 figures are accounted for. The source provides precise
algebraic models for linguistic Merge, semantic composition, tree moduli, and
attention, and repeatedly distinguishes proposed toy models, conjectural
inverse-problem hardness, and cited empirical observations. It contains no
Danos-Regnier switching criterion, MLL checker correctness theorem,
desequentialization/sequentialization theorem, proof-net canonicalization
algorithm, or experiment showing that proof nets improve formal proof search.
In particular, its Theorem 5.4 concerns Minimal Search among linguistic Merge
derivations and must not be represented as a result about focused MLL search.