From 4eee78be098b43c3fb5ef1059d05598d20de5600 Mon Sep 17 00:00:00 2001 From: Codex Bot Date: Wed, 28 Oct 2026 21:42:45 +0800 Subject: [PATCH] docs(schema): track the 65-item schema review page --- README.md | 9 +- docs/reviews/simplex-schemas.html | 9341 +++++++++++++++++ docs/simplex-schema.md | 13 +- experiments/P0-pilot/README.md | 4 + experiments/P0-pilot/build_schemas.py | 14 +- .../results/simplex-schema-summary.json | 2 +- 6 files changed, 9375 insertions(+), 8 deletions(-) create mode 100644 docs/reviews/simplex-schemas.html diff --git a/README.md b/README.md index 1604f9a..8172015 100644 --- a/README.md +++ b/README.md @@ -276,6 +276,12 @@ Experiments have IDs (`P0`, `E0`-`E11`); the registry, phases, gates and convent [`docs/experiments/README.md`](docs/experiments/README.md). CI runner and environment notes: [`docs/infrastructure/runner-lean435.md`](docs/infrastructure/runner-lean435.md). +Browse the [65-item semantic simplex schema review](docs/reviews/simplex-schemas.html) +by opening that HTML file in a browser after cloning, or downloading it from Git. +It shows role schemas and Lean signature expressions; textbook passages and full assistant +judgment explanations remain private. The [schema design and replay instructions](docs/simplex-schema.md) +explain how the page is generated and which annotations still need review. + ## What this does not claim Lean says whether the code is *legal*, and — when there is a proof — whether it is @@ -285,4 +291,5 @@ well-formed statement of the wrong theorem passes every check here. `confidence` possible; spot-check before trusting a dataset. Source books are not committed. `.gitignore` keeps PDFs and extracted text out of -the repository; only code and the short Lean datasets belong in git. +the repository. The tracked schema review contains semantic annotations and Lean signatures, +while source-inclusive inputs remain in the ignored data directory. diff --git a/docs/reviews/simplex-schemas.html b/docs/reviews/simplex-schemas.html new file mode 100644 index 0000000..298ae8b --- /dev/null +++ b/docs/reviews/simplex-schemas.html @@ -0,0 +1,9341 @@ +P0 semantic simplex schemas

65 semantic multi-role relation schemas

Schema annotation seeds, not independently validated mathematical statements. A simplex joins the objects, assumptions and conclusion in its slots. References are partial symbol/syntax candidates. This review contains schema annotations and Lean signature text, not textbook passages or full assistant judgment explanations.

P01

source

{
+  "name": "schema:p0-f12735802ba0:548ab1a767a685aefa146455:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "field",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "field"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "fact1",
+      "kind": "fact",
+      "context": "commutative ring",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "commutative",
+          "ring"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "fact2",
+      "kind": "fact",
+      "context": "identity nonzero",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "identity",
+          "nonzero"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "nonzero elements are units",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "nonzero",
+          "elements",
+          "are",
+          "units"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:548ab1a767a685aefa146455:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "F": {
+      "name": "F",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "own": {
+      "name": "own",
+      "kind": "own",
+      "type": "class",
+      "attrs": {
+        "keyword": "class",
+        "references": [],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P02

source

{
+  "name": "schema:p0-f12735802ba0:6ea85a17cb5decb0670c4afe:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "whole group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "whole",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "object3",
+      "kind": "object",
+      "context": "identity singleton",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "identity",
+          "singleton"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "both sets are subgroups",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "both",
+          "sets",
+          "are",
+          "subgroups"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:6ea85a17cb5decb0670c4afe:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "Subgroup G (Set.univ : Set G) ∧ Subgroup G {1}",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P03

source

{
+  "name": "schema:p0-f12735802ba0:389a27cbae1957943fae2960:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "integer ring",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "integer",
+          "ring"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "unit",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "unit"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "units equal plus minus one",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "units",
+          "equal",
+          "plus",
+          "minus",
+          "one"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:389a27cbae1957943fae2960:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "premise1": {
+      "name": "premise1",
+      "kind": "fact",
+      "type": "(u : ℤ)",
+      "attrs": {
+        "binder_kind": "goal_implication",
+        "classified_by": "implication",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "premise2": {
+      "name": "premise2",
+      "kind": "fact",
+      "type": "IsUnit u",
+      "attrs": {
+        "binder_kind": "goal_implication",
+        "classified_by": "implication",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "u = 1 ∨ u = -1",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P04

source

{
+  "name": "schema:p0-f12735802ba0:b63f0ed4d1ea1e11e34e6f8a:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "a",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "generated subgroup equals integer powers",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "generated",
+          "subgroup",
+          "equals",
+          "integer",
+          "powers"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:b63f0ed4d1ea1e11e34e6f8a:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\<a\\> = {a ^ k | k : ℤ}",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "a"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P05

source

{
+  "name": "schema:p0-f12735802ba0:db4553333550bccbd3f0e21d:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "H",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "φ",
+      "kind": "object",
+      "context": "map between groups",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "map",
+          "between",
+          "groups"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "φ",
+      "kind": "fact",
+      "context": "bijective",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "bijective"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object3"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "φ",
+      "kind": "fact",
+      "context": "preserves multiplication",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "preserves",
+          "multiplication"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object3"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "isomorphic iff such map exists",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "isomorphic",
+          "iff",
+          "such",
+          "map",
+          "exists"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:db4553333550bccbd3f0e21d:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "H": {
+      "name": "H",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group H"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "own": {
+      "name": "own",
+      "kind": "own",
+      "type": "Prop",
+      "attrs": {
+        "keyword": "def",
+        "references": [],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P06

source

{
+  "name": "schema:p0-f12735802ba0:c3e75089fbfe8f386b4a22ec:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "a",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "b",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "b"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "inverse product reverses inverse factors",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "inverse",
+          "product",
+          "reverses",
+          "inverse",
+          "factors"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:c3e75089fbfe8f386b4a22ec:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "b": {
+      "name": "b",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "(a * b)⁻¹ = b⁻¹ * a⁻¹",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "a",
+          "b"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P07

source

{
+  "name": "schema:p0-f12735802ba0:91a6a0c1c21014bf08ffa3b6:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "n",
+      "kind": "object",
+      "context": "integer modulus",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "integer",
+          "modulus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "p",
+      "kind": "object",
+      "context": "prime factor",
+      "attrs": {
+        "symbols": [
+          "p"
+        ],
+        "keywords": [
+          "prime",
+          "factor"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "q",
+      "kind": "object",
+      "context": "prime factor",
+      "attrs": {
+        "symbols": [
+          "q"
+        ],
+        "keywords": [
+          "prime",
+          "factor"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "φ",
+      "kind": "object",
+      "context": "totient function",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "totient",
+          "function"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "φ",
+      "kind": "fact",
+      "context": "totient value can be found",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "totient",
+          "value",
+          "can",
+          "be",
+          "found"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object4"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "recover both prime factors",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "recover",
+          "both",
+          "prime",
+          "factors"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:91a6a0c1c21014bf08ffa3b6:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "p": {
+      "name": "p",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "q": {
+      "name": "q",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hn": {
+      "name": "hn",
+      "kind": "fact",
+      "type": "n = p * q",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "n",
+          "p",
+          "q"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hpq": {
+      "name": "hpq",
+      "kind": "fact",
+      "type": "p.Prime ∧ q.Prime",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "p",
+          "q"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "premise1": {
+      "name": "premise1",
+      "kind": "fact",
+      "type": "∃ (φ : ℕ → ℕ), (∀ m, φ m = Nat.totient m)",
+      "attrs": {
+        "binder_kind": "goal_implication",
+        "classified_by": "implication",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "∃ (p' q' : ℕ), n = p' * q' ∧ p'.Prime ∧ q'.Prime",
+      "attrs": {
+        "exists_count": 1,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P08

source

{
+  "name": "schema:p0-f12735802ba0:675ac9dbf3ec8a0553149a96:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "H",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "φ",
+      "kind": "object",
+      "context": "isomorphism",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "isomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "g",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "g"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "φ",
+      "kind": "fact",
+      "context": "group isomorphism",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "group",
+          "isomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object3"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "map preserves identity and inverses",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "map",
+          "preserves",
+          "identity",
+          "and",
+          "inverses"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:675ac9dbf3ec8a0553149a96:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "H": {
+      "name": "H",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group H"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "φ (1 : G) = (1 : H) ∧ ∀ g : G, φ g⁻¹ = (φ g)⁻¹",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 1,
+        "is_iff": false,
+        "references": [
+          "G",
+          "H"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P09

source

{
+  "name": "schema:p0-f12735802ba0:8b39fc5b656bac00bc1e863f:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "cyclic group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "cyclic",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "rectangle symmetry group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "rectangle",
+          "symmetry",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "H",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object5": {
+      "name": "φ",
+      "kind": "object",
+      "context": "isomorphism",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "isomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object6": {
+      "name": "g",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "g"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object7": {
+      "name": "n",
+      "kind": "object",
+      "context": "natural number",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "natural",
+          "number"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "nonisomorphism and preservation of powers",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "nonisomorphism",
+          "and",
+          "preservation",
+          "of",
+          "powers"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P10

source

{
+  "name": "schema:p0-f12735802ba0:3549ad65eee67f7b432a8b70:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "a",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "b",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "b"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "left right equations uniquely solvable",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "left",
+          "right",
+          "equations",
+          "uniquely",
+          "solvable"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:3549ad65eee67f7b432a8b70:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "b": {
+      "name": "b",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\\\(∃! x : G, a * x = b) ∧ (∃! x : G, x * a = b)",
+      "attrs": {
+        "exists_count": 2,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "G",
+          "a",
+          "b"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P11

source

{
+  "name": "schema:p0-f12735802ba0:0b7db1a8100c33a50a08981f:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "n",
+      "kind": "object",
+      "context": "group size",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "group",
+          "size"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "g",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "g"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "G",
+      "kind": "fact",
+      "context": "finite",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "finite"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "nth power equals identity",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "nth",
+          "power",
+          "equals",
+          "identity"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:0b7db1a8100c33a50a08981f:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G",
+          "Fintype G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "g": {
+      "name": "g",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "g ^ Fintype.card G = 1",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "G",
+          "g"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P12

source

{
+  "name": "schema:p0-f12735802ba0:e3d40d93cda13ec59c35d9a5:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "RSA method",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "rsa",
+          "method"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "messages",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "messages"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "design secure authenticated message exchange",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "design",
+          "secure",
+          "authenticated",
+          "message",
+          "exchange"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P13

source

{
+  "name": "schema:p0-f12735802ba0:aaf1250a5104a4f7c1ca0d29:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "n",
+      "kind": "object",
+      "context": "modulus",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "modulus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "a",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "Φ",
+      "kind": "object",
+      "context": "group of units",
+      "attrs": {
+        "symbols": [
+          "Φ"
+        ],
+        "keywords": [
+          "group",
+          "of",
+          "units"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "a",
+      "kind": "fact",
+      "context": "relatively prime to modulus",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "relatively",
+          "prime",
+          "to",
+          "modulus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "totient power congruent to one",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "totient",
+          "power",
+          "congruent",
+          "to",
+          "one"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:aaf1250a5104a4f7c1ca0d29:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h": {
+      "name": "h",
+      "kind": "fact",
+      "type": "Nat.Coprime a n",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "predicate",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "a",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "(a ^ Nat.totient n) ≡ 1 [ZMOD n]",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "a",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P14

source

{
+  "name": "schema:p0-f12735802ba0:57966f39253aba58777a4ffd:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "X",
+      "kind": "object",
+      "context": "set",
+      "attrs": {
+        "symbols": [
+          "X"
+        ],
+        "keywords": [
+          "set"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "real valued functions",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "real",
+          "valued",
+          "functions"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "ring identity and unit characterization",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "ring",
+          "identity",
+          "and",
+          "unit",
+          "characterization"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:57966f39253aba58777a4ffd:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "X": {
+      "name": "X",
+      "kind": "object",
+      "type": "Type",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "Ring (X → ℝ)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "X"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P15

source

{
+  "name": "schema:p0-f12735802ba0:6ef921c49672c73f8f3e0edf:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "G",
+      "kind": "fact",
+      "context": "finite",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "finite"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "rows columns contain elements once",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "rows",
+          "columns",
+          "contain",
+          "elements",
+          "once"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:6ef921c49672c73f8f3e0edf:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G",
+          "Fintype G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "g": {
+      "name": "g",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h": {
+      "name": "h",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\\\\\n  ∃! (x : G), x * g = h \\\\\\n  ∧ ∃! (y : G), g * y = h",
+      "attrs": {
+        "exists_count": 2,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "G",
+          "g",
+          "h"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P16

source

{
+  "name": "schema:p0-f12735802ba0:371fe1b32fe04da354ad4478:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "H",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "K",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "K"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "object4",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "H",
+      "kind": "fact",
+      "context": "finite",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "finite"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "K",
+      "kind": "fact",
+      "context": "finite",
+      "attrs": {
+        "symbols": [
+          "K"
+        ],
+        "keywords": [
+          "finite"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object3"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact3": {
+      "name": "G",
+      "kind": "fact",
+      "context": "isomorphic to product",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "isomorphic",
+          "to",
+          "product"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "element order divides lcm sizes",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "element",
+          "order",
+          "divides",
+          "lcm",
+          "sizes"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:371fe1b32fe04da354ad4478:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "H": {
+      "name": "H",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Fintype H",
+          "Group H"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "K": {
+      "name": "K",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Fintype K",
+          "Group K"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "g": {
+      "name": "g",
+      "kind": "object",
+      "type": "H × K",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "H",
+          "K"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "OrderOf g ∣ lcm (Fintype.card H) (Fintype.card K)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "H",
+          "K",
+          "g"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P17

source

{
+  "name": "schema:p0-f12735802ba0:a7396b1a5d5ebcd5b48ea7ba:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "real numbers",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "real",
+          "numbers"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "rational numbers",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "rational",
+          "numbers"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "object3",
+      "kind": "object",
+      "context": "complex numbers",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "complex",
+          "numbers"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "object4",
+      "kind": "object",
+      "context": "integers",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "integers"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object5": {
+      "name": "object5",
+      "kind": "object",
+      "context": "real polynomial ring",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "real",
+          "polynomial",
+          "ring"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "three fields two nonfields",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "three",
+          "fields",
+          "two",
+          "nonfields"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P18

source

{
+  "name": "schema:p0-f12735802ba0:59bb865c9bdfb8521e414743:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "complex numbers",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "complex",
+          "numbers"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "norm one subset",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "norm",
+          "one",
+          "subset"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "object3",
+      "kind": "object",
+      "context": "nonzero complex numbers",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "nonzero",
+          "complex",
+          "numbers"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "unit modulus set is subgroup",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "unit",
+          "modulus",
+          "set",
+          "is",
+          "subgroup"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P19

source

{
+  "name": "schema:p0-f12735802ba0:283d407566264b02fbee6560:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "a",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "generated cyclic subgroup",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "generated",
+          "cyclic",
+          "subgroup"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "element order defined by subgroup size",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "element",
+          "order",
+          "defined",
+          "by",
+          "subgroup"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:283d407566264b02fbee6560:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "own": {
+      "name": "own",
+      "kind": "own",
+      "type": "ℕ",
+      "attrs": {
+        "keyword": "def",
+        "references": [],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P20

source

{
+  "name": "schema:p0-f12735802ba0:7de228e675b949cd64850c04:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "e",
+      "kind": "object",
+      "context": "identity element",
+      "attrs": {
+        "symbols": [
+          "e"
+        ],
+        "keywords": [
+          "identity",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "e'",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "e'"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "g",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "g"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "fact1",
+      "kind": "fact",
+      "context": "left product equals g",
+      "attrs": {
+        "symbols": [
+          "e'",
+          "g"
+        ],
+        "keywords": [
+          "left",
+          "product",
+          "equals",
+          "g"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object3",
+          "object4"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "element equals group identity",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "element",
+          "equals",
+          "group",
+          "identity"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:7de228e675b949cd64850c04:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "e'": {
+      "name": "e'",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "g": {
+      "name": "g",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h": {
+      "name": "h",
+      "kind": "fact",
+      "type": "e' * g = g",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "e'",
+          "g"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "e' = 1",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "e'"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P21

source

{
+  "name": "schema:p0-f12735802ba0:dc1c450987f3e3a5285260f7:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "H",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "φ",
+      "kind": "object",
+      "context": "isomorphism",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "isomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "φ",
+      "kind": "fact",
+      "context": "group isomorphism",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "group",
+          "isomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object3"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "abelian iff target abelian",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "abelian",
+          "iff",
+          "target",
+          "abelian"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:dc1c450987f3e3a5285260f7:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "H": {
+      "name": "H",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group H"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\\\\\n  Commutative (*) ↔ Commutative ((*) : H → H → H)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": true,
+        "references": [
+          "H"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P22

source

{
+  "name": "schema:p0-f12735802ba0:c42dc687ecc042f5b7a00a9d:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "finite group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "finite",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "fact1",
+      "kind": "fact",
+      "context": "finite",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "finite"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "each row column permutes group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "each",
+          "row",
+          "column",
+          "permutes",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:c42dc687ecc042f5b7a00a9d:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Fintype G",
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\/\\n  (∀ g : G, ∀ g' : G, ∃! h : G, g * h = g') ∧ \\/\\n  (∀ g : G, ∀ g' : G, ∃! h : G, h * g = g')",
+      "attrs": {
+        "exists_count": 2,
+        "forall_count": 4,
+        "is_iff": false,
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P23

source

{
+  "name": "schema:p0-f12735802ba0:8491370b02906b6efdb3da5e:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "n",
+      "kind": "object",
+      "context": "natural modulus",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "natural",
+          "modulus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "p",
+      "kind": "object",
+      "context": "prime",
+      "attrs": {
+        "symbols": [
+          "p"
+        ],
+        "keywords": [
+          "prime"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "q",
+      "kind": "object",
+      "context": "prime",
+      "attrs": {
+        "symbols": [
+          "q"
+        ],
+        "keywords": [
+          "prime"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "m",
+      "kind": "object",
+      "context": "integer exponent",
+      "attrs": {
+        "symbols": [
+          "m"
+        ],
+        "keywords": [
+          "integer",
+          "exponent"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object5": {
+      "name": "a",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "n",
+      "kind": "fact",
+      "context": "product of primes",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "product",
+          "of",
+          "primes"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "m",
+      "kind": "fact",
+      "context": "lcm predecessors",
+      "attrs": {
+        "symbols": [
+          "m"
+        ],
+        "keywords": [
+          "lcm",
+          "predecessors"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object4"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact3": {
+      "name": "a",
+      "kind": "fact",
+      "context": "relatively prime to modulus",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "relatively",
+          "prime",
+          "to",
+          "modulus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object5"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "exponent power congruent to one",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "exponent",
+          "power",
+          "congruent",
+          "to",
+          "one"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:8491370b02906b6efdb3da5e:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "p": {
+      "name": "p",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "q": {
+      "name": "q",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hp": {
+      "name": "hp",
+      "kind": "fact",
+      "type": "Nat.Prime p",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "predicate",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "p"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hq": {
+      "name": "hq",
+      "kind": "fact",
+      "type": "Nat.Prime q",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "predicate",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "q"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hn": {
+      "name": "hn",
+      "kind": "fact",
+      "type": "n = p * q",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "n",
+          "p",
+          "q"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "m": {
+      "name": "m",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hm": {
+      "name": "hm",
+      "kind": "fact",
+      "type": "m = Nat.lcm (p - 1) (q - 1)",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "m",
+          "p",
+          "q"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "ha": {
+      "name": "ha",
+      "kind": "fact",
+      "type": "Nat.Coprime a n",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "predicate",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "a",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "a ^ m ≡ 1 [ZMOD n]",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "a",
+          "m",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P24

source

{
+  "name": "schema:p0-f12735802ba0:437d02fe69d580bde075648c:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "painted square",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "painted",
+          "square"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "color preserving symmetries",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "color",
+          "preserving",
+          "symmetries"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "identify symmetry group size isomorphism",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "identify",
+          "symmetry",
+          "group",
+          "size",
+          "isomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P25

source

{
+  "name": "schema:p0-f12735802ba0:5fe4f3fbbead7e6988f015a9:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "a",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "x",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "x"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "y",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "y"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "left and right cancellation implications",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "left",
+          "and",
+          "right",
+          "cancellation",
+          "implications"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:5fe4f3fbbead7e6988f015a9:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "x": {
+      "name": "x",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "y": {
+      "name": "y",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "premise1": {
+      "name": "premise1",
+      "kind": "fact",
+      "type": "a * x = a * y",
+      "attrs": {
+        "binder_kind": "goal_implication",
+        "classified_by": "implication",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "a",
+          "x",
+          "y"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "x = y",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "x",
+          "y"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P26

source

{
+  "name": "schema:p0-f12735802ba0:8a55f59982e50e4af47b3d55:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "a",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "h",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "h"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "m",
+      "kind": "object",
+      "context": "exponent modulus",
+      "attrs": {
+        "symbols": [
+          "m"
+        ],
+        "keywords": [
+          "exponent",
+          "modulus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "n",
+      "kind": "object",
+      "context": "modulus",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "modulus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "h",
+      "kind": "fact",
+      "context": "congruent one modulo m",
+      "attrs": {
+        "symbols": [
+          "h"
+        ],
+        "keywords": [
+          "congruent",
+          "one",
+          "modulo",
+          "m"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "power congruent to original integer",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "power",
+          "congruent",
+          "to",
+          "original",
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:8a55f59982e50e4af47b3d55:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h": {
+      "name": "h",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "m": {
+      "name": "m",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hn": {
+      "name": "hn",
+      "kind": "fact",
+      "type": "h % m = 1",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "h",
+          "m"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hm": {
+      "name": "hm",
+      "kind": "fact",
+      "type": "m ∣ n",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "m",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "a ^ h ≡ a [ZMOD n]",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "a",
+          "h",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P27

source

{
+  "name": "schema:p0-f12735802ba0:8d4d64143a8b214e38d7ba1b:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "S_4",
+      "kind": "object",
+      "context": "permutation group",
+      "attrs": {
+        "symbols": [
+          "S_4"
+        ],
+        "keywords": [
+          "permutation",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "π",
+      "kind": "object",
+      "context": "permutation",
+      "attrs": {
+        "symbols": [
+          "π"
+        ],
+        "keywords": [
+          "permutation"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "object3",
+      "kind": "object",
+      "context": "stabilizer subgroup",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "stabilizer",
+          "subgroup"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "π",
+      "kind": "fact",
+      "context": "fixes fourth point",
+      "attrs": {
+        "symbols": [
+          "π"
+        ],
+        "keywords": [
+          "fixes",
+          "fourth",
+          "point"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "stabilizer subgroup isomorphic to S3",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "stabilizer",
+          "subgroup",
+          "isomorphic",
+          "to",
+          "s"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P28

source

{
+  "name": "schema:p0-f12735802ba0:6017927fdafd91ca22ed6ade:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "a",
+      "kind": "object",
+      "context": "rational number",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "rational",
+          "number"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "b",
+      "kind": "object",
+      "context": "rational number",
+      "attrs": {
+        "symbols": [
+          "b"
+        ],
+        "keywords": [
+          "rational",
+          "number"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "object3",
+      "kind": "object",
+      "context": "real quadratic subset",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "real",
+          "quadratic",
+          "subset"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "object4",
+      "kind": "object",
+      "context": "conjugation map",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "conjugation",
+          "map"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "subset field conjugation is automorphism",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "subset",
+          "field",
+          "conjugation",
+          "is",
+          "automorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P29

source

{
+  "name": "schema:p0-f12735802ba0:089c452ec2f9b850733a44f6:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "H",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "φ",
+      "kind": "object",
+      "context": "isomorphism",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "isomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "g",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "g"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object5": {
+      "name": "n",
+      "kind": "object",
+      "context": "natural number",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "natural",
+          "number"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "φ",
+      "kind": "fact",
+      "context": "group isomorphism",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "group",
+          "isomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object3"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "map preserves powers and identity powers",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "map",
+          "preserves",
+          "powers",
+          "and",
+          "identity"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:089c452ec2f9b850733a44f6:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "H": {
+      "name": "H",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group H"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "g": {
+      "name": "g",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\/\\/  φ(g^n) = (φ g)^n ∧ (g^n = 1 → (φ g)^n = 1)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "g",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P30

source

{
+  "name": "schema:p0-f12735802ba0:75009c3d616f02be4d7a5824:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "M",
+      "kind": "object",
+      "context": "set",
+      "attrs": {
+        "symbols": [
+          "M"
+        ],
+        "keywords": [
+          "set"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "N",
+      "kind": "object",
+      "context": "subset",
+      "attrs": {
+        "symbols": [
+          "N"
+        ],
+        "keywords": [
+          "subset"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "n",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "a",
+      "kind": "object",
+      "context": "sequence of elements",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "sequence",
+          "of",
+          "elements"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "M",
+      "kind": "fact",
+      "context": "associative operation",
+      "attrs": {
+        "symbols": [
+          "M"
+        ],
+        "keywords": [
+          "associative",
+          "operation"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "N",
+      "kind": "fact",
+      "context": "closed under multiplication",
+      "attrs": {
+        "symbols": [
+          "N"
+        ],
+        "keywords": [
+          "closed",
+          "under",
+          "multiplication"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact3": {
+      "name": "n",
+      "kind": "fact",
+      "context": "positive",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "positive"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object3"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact4": {
+      "name": "a",
+      "kind": "fact",
+      "context": "elements belong to subset",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "elements",
+          "belong",
+          "to",
+          "subset"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object4"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "ordered product belongs to subset",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "ordered",
+          "product",
+          "belongs",
+          "to",
+          "subset"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:75009c3d616f02be4d7a5824:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "M": {
+      "name": "M",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Semigroup M"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "N": {
+      "name": "N",
+      "kind": "object",
+      "type": "Set M",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "M"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hN": {
+      "name": "hN",
+      "kind": "fact",
+      "type": "∀ x y ∈ N, x * y ∈ N",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "N"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hn": {
+      "name": "hn",
+      "kind": "fact",
+      "type": "1 ≤ n",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "Fin n → M",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "M",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "ha": {
+      "name": "ha",
+      "kind": "fact",
+      "type": "∀ i, a i ∈ N",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "N",
+          "a"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "(∏ i, a i) ∈ N",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "N",
+          "a"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P31

source

{
+  "name": "schema:p0-f12735802ba0:9091f6a277215174e821d373:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "φ",
+      "kind": "object",
+      "context": "previously defined ring map",
+      "attrs": {
+        "symbols": [
+          "φ"
+        ],
+        "keywords": [
+          "previously",
+          "defined",
+          "ring",
+          "map"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "verify this map preserves ring operations",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "verify",
+          "this",
+          "map",
+          "preserves",
+          "ring"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:9091f6a277215174e821d373:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "R": {
+      "name": "R",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Ring R"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "S": {
+      "name": "S",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Ring S"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "IsRingHom φ",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P32

source

{
+  "name": "schema:p0-f12735802ba0:0cd2f0368a0d8234c2593845:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "n",
+      "kind": "object",
+      "context": "matrix size",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "matrix",
+          "size"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "T",
+      "kind": "object",
+      "context": "real matrix",
+      "attrs": {
+        "symbols": [
+          "T"
+        ],
+        "keywords": [
+          "real",
+          "matrix"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "evaluation at matrix is homomorphism",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "evaluation",
+          "at",
+          "matrix",
+          "is",
+          "homomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:0cd2f0368a0d8234c2593845:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "T": {
+      "name": "T",
+      "kind": "object",
+      "type": "Matrix n n ℝ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "RingHom (Polynomial ℝ) (Matrix n n ℝ)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P33

source

{
+  "name": "schema:p0-f12735802ba0:8e55e625fa9b10b7b65f59f4:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "G",
+      "kind": "fact",
+      "context": "four elements",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "four",
+          "elements"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "nonidentity element squares to identity",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "nonidentity",
+          "element",
+          "squares",
+          "to",
+          "identity"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:8e55e625fa9b10b7b65f59f4:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hG": {
+      "name": "hG",
+      "kind": "fact",
+      "type": "Fintype.card G = 4",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "∃ g : G, g ≠ 1 ∧ g * g = 1",
+      "attrs": {
+        "exists_count": 1,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P34

source

{
+  "name": "schema:p0-f12735802ba0:534c6ffcf56931559e70657b:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "S_3",
+      "kind": "object",
+      "context": "symmetric group",
+      "attrs": {
+        "symbols": [
+          "S_3"
+        ],
+        "keywords": [
+          "symmetric",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "cyclic group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "cyclic",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "nonabelian and abelian hence nonisomorphic",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "nonabelian",
+          "and",
+          "abelian",
+          "hence",
+          "nonisomorphic"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P35

source

{
+  "name": "schema:p0-f12735802ba0:aa16561dceee591e35e42c4d:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "M",
+      "kind": "object",
+      "context": "set",
+      "attrs": {
+        "symbols": [
+          "M"
+        ],
+        "keywords": [
+          "set"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "n",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "M",
+      "kind": "fact",
+      "context": "associative operation",
+      "attrs": {
+        "symbols": [
+          "M"
+        ],
+        "keywords": [
+          "associative",
+          "operation"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "n",
+      "kind": "fact",
+      "context": "positive",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "positive"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "unique coherent associative product family",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "unique",
+          "coherent",
+          "associative",
+          "product",
+          "family"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:aa16561dceee591e35e42c4d:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "M": {
+      "name": "M",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Semigroup M"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h": {
+      "name": "h",
+      "kind": "fact",
+      "type": "n ≥ 1",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "premise1": {
+      "name": "premise1",
+      "kind": "fact",
+      "type": "∃! f : (Fin n → M)",
+      "attrs": {
+        "binder_kind": "goal_implication",
+        "classified_by": "implication",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "M",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "M, (∀ a : M, f ![a] = a) ∧ (∀ a b : M, f ![a, b] = a * b) ∧ (∀ (k : ℕ) (hk : 1 ≤ k) (hnk : k < n) (a : Fin n → M), f a = f (a ↾ k) * f (a ∘ (Fin.succAbove k).symm))",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 3,
+        "is_iff": false,
+        "references": [
+          "M",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P36

source

{
+  "name": "schema:p0-f12735802ba0:73ec95bfac2896218d2b1dab:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "C_n",
+      "kind": "object",
+      "context": "root of unity group",
+      "attrs": {
+        "symbols": [
+          "C_n"
+        ],
+        "keywords": [
+          "root",
+          "of",
+          "unity",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "n",
+      "kind": "object",
+      "context": "order",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "order"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "ξ",
+      "kind": "object",
+      "context": "complex exponential generator",
+      "attrs": {
+        "symbols": [
+          "ξ"
+        ],
+        "keywords": [
+          "complex",
+          "exponential",
+          "generator"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "cyclic with specified order generator",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "cyclic",
+          "with",
+          "specified",
+          "order",
+          "generator"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:73ec95bfac2896218d2b1dab:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h": {
+      "name": "h",
+      "kind": "fact",
+      "type": "n > 0",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "IsCyclic (ZMod n)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P37

source

{
+  "name": "schema:p0-f12735802ba0:6b5a55ec3bb3c85239919649:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "C_n",
+      "kind": "object",
+      "context": "root of unity set",
+      "attrs": {
+        "symbols": [
+          "C_n"
+        ],
+        "keywords": [
+          "root",
+          "of",
+          "unity",
+          "set"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "n",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "k",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "k"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "k",
+      "kind": "fact",
+      "context": "between zero and n minus one",
+      "attrs": {
+        "symbols": [
+          "k"
+        ],
+        "keywords": [
+          "between",
+          "zero",
+          "and",
+          "n",
+          "minus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object3"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "roots equal specified exponential set",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "roots",
+          "equal",
+          "specified",
+          "exponential",
+          "set"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:6b5a55ec3bb3c85239919649:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "own": {
+      "name": "own",
+      "kind": "own",
+      "type": "Subgroup ℂ",
+      "attrs": {
+        "keyword": "def",
+        "references": [],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P38

source

{
+  "name": "schema:p0-f12735802ba0:d6ddc1df3ce6b764f3fb8d73:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "H",
+      "kind": "object",
+      "context": "subset",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "subset"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "H",
+      "kind": "fact",
+      "context": "nonempty",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "nonempty"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "H",
+      "kind": "fact",
+      "context": "closed under products",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "closed",
+          "under",
+          "products"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact3": {
+      "name": "H",
+      "kind": "fact",
+      "context": "closed under inverses",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "closed",
+          "under",
+          "inverses"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "conditions imply subgroup and identity",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "conditions",
+          "imply",
+          "subgroup",
+          "and",
+          "identity"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:d6ddc1df3ce6b764f3fb8d73:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "H": {
+      "name": "H",
+      "kind": "object",
+      "type": "Set G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h_one": {
+      "name": "h_one",
+      "kind": "fact",
+      "type": "∀ h ∈ H, h⁻¹ ∈ H",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "H"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h_mul": {
+      "name": "h_mul",
+      "kind": "fact",
+      "type": "∀ h1 h2 ∈ H, h1 * h2 ∈ H",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "H"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "IsSubgroup H",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "H"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P39

source

{
+  "name": "schema:p0-f12735802ba0:ed87589326312890bea42d7c:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "K",
+      "kind": "object",
+      "context": "field",
+      "attrs": {
+        "symbols": [
+          "K"
+        ],
+        "keywords": [
+          "field"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "Laurent polynomials",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "laurent",
+          "polynomials"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "ring with identity and units",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "ring",
+          "with",
+          "identity",
+          "and",
+          "units"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:ed87589326312890bea42d7c:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "K": {
+      "name": "K",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Field K"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "Ring (LaurentSeries K)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "K"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P40

source

{
+  "name": "schema:p0-f12735802ba0:d609c5bb746fc0e05625134a:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "f",
+      "kind": "object",
+      "context": "map",
+      "attrs": {
+        "symbols": [
+          "f"
+        ],
+        "keywords": [
+          "map"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "n",
+      "kind": "object",
+      "context": "modulus",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "modulus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "object3",
+      "kind": "object",
+      "context": "integers",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "integers"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "object4",
+      "kind": "object",
+      "context": "residue ring",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "residue",
+          "ring"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "canonical residue map is homomorphism",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "canonical",
+          "residue",
+          "map",
+          "is",
+          "homomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:d609c5bb746fc0e05625134a:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "RingHom ℤ (ZMod n)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P41

source

{
+  "name": "schema:p0-f12735802ba0:4405f31187373d5e1de622d2:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "n",
+      "kind": "object",
+      "context": "natural number",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "natural",
+          "number"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "S_n",
+      "kind": "object",
+      "context": "symmetric group",
+      "attrs": {
+        "symbols": [
+          "S_n"
+        ],
+        "keywords": [
+          "symmetric",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "factorial cardinality always nonabelian when n≥3",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "factorial",
+          "cardinality",
+          "always",
+          "nonabelian",
+          "when"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:4405f31187373d5e1de622d2:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hn": {
+      "name": "hn",
+      "kind": "fact",
+      "type": "n ≥ 3",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\n  Fintype.card (Symmetric n) = n! ∧ ¬ IsAbelian (Symmetric n)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P42

source

{
+  "name": "schema:p0-f12735802ba0:05a6defa23576b7da41f8fbf:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "H",
+      "kind": "object",
+      "context": "subset",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "subset"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "H",
+      "kind": "fact",
+      "context": "nonempty",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "nonempty"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "H",
+      "kind": "fact",
+      "context": "subgroup",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "subgroup"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "product closure is necessary",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "product",
+          "closure",
+          "is",
+          "necessary"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:05a6defa23576b7da41f8fbf:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "H": {
+      "name": "H",
+      "kind": "object",
+      "type": "Set G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h_nonempty": {
+      "name": "h_nonempty",
+      "kind": "object",
+      "type": "H.Nonempty",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "H"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h_prod": {
+      "name": "h_prod",
+      "kind": "fact",
+      "type": "∀ h1 h2 ∈ H, h1 * h2 ∈ H",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "H"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "IsSubgroup H",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "H"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P43

source

{
+  "name": "schema:p0-f12735802ba0:47c39e88c29e3974e8864e90:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "fact1",
+      "kind": "fact",
+      "context": "order two",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "order",
+          "two"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "unique group up to isomorphism",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "unique",
+          "group",
+          "up",
+          "to",
+          "isomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:47c39e88c29e3974e8864e90:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G",
+          "Fintype G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "H": {
+      "name": "H",
+      "kind": "object",
+      "type": "Type",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group H",
+          "Fintype H"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hG": {
+      "name": "hG",
+      "kind": "fact",
+      "type": "Fintype.card G = 2",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hH": {
+      "name": "hH",
+      "kind": "fact",
+      "type": "Fintype.card H = 2",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "H"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "Nonempty (G ≃* H)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "G",
+          "H"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P44

source

{
+  "name": "schema:p0-f12735802ba0:fa61f8cb0e88b11e158c4eec:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "a",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "b",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "b"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "abelian defined by commuting products",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "abelian",
+          "defined",
+          "by",
+          "commuting",
+          "products"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:fa61f8cb0e88b11e158c4eec:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "own": {
+      "name": "own",
+      "kind": "own",
+      "type": "Prop",
+      "attrs": {
+        "keyword": "class",
+        "references": [],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P45

source

{
+  "name": "schema:p0-f12735802ba0:3c00c37b39285cbd7d0be732:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "fact1",
+      "kind": "fact",
+      "context": "order three",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "order",
+          "three"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "unique group up to isomorphism",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "unique",
+          "group",
+          "up",
+          "to",
+          "isomorphism"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P46

source

{
+  "name": "schema:p0-f12735802ba0:186d922a4121917ac8643316:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "real three variable polynomials",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "real",
+          "three",
+          "variable",
+          "polynomials"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "ring identity and unit characterization",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "ring",
+          "identity",
+          "and",
+          "unit",
+          "characterization"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P47

source

{
+  "name": "schema:p0-f12735802ba0:e845a95d7b5054a0dbdf34eb:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "d",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "d"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "generated subgroup",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "generated",
+          "subgroup"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "integer multiples cyclic opposite generators equal",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "integer",
+          "multiples",
+          "cyclic",
+          "opposite",
+          "generators"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:e845a95d7b5054a0dbdf34eb:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "d": {
+      "name": "d",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "(Submodule.span ℤ {d}) = {n * d | n : ℤ}",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "d"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P48

source

{
+  "name": "schema:p0-f12735802ba0:e7a3cec23c2ecdc655dd12cf:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "h",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "h"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "g",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "g"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "fact1",
+      "kind": "fact",
+      "context": "product equals identity",
+      "attrs": {
+        "symbols": [
+          "h",
+          "g"
+        ],
+        "keywords": [
+          "product",
+          "equals",
+          "identity"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2",
+          "object3"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "left inverse equals inverse element",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "left",
+          "inverse",
+          "equals",
+          "inverse",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:e7a3cec23c2ecdc655dd12cf:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h": {
+      "name": "h",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "g": {
+      "name": "g",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hg": {
+      "name": "hg",
+      "kind": "fact",
+      "type": "h * g = 1",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "g",
+          "h"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "h = g⁻¹",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "g",
+          "h"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P49

source

{
+  "name": "schema:p0-f12735802ba0:e966f3b17e32318acd5f2762:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "g",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "g"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "inverse of inverse equals element",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "inverse",
+          "of",
+          "inverse",
+          "equals",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:e966f3b17e32318acd5f2762:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "g": {
+      "name": "g",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "g = (g⁻¹)⁻¹",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "g"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P50

source

{
+  "name": "schema:p0-f12735802ba0:2c420bf6ec32069ecd0043dc:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "R",
+      "kind": "object",
+      "context": "set",
+      "attrs": {
+        "symbols": [
+          "R"
+        ],
+        "keywords": [
+          "set"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "addition",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "addition"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "object3",
+      "kind": "object",
+      "context": "multiplication",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "multiplication"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "R",
+      "kind": "fact",
+      "context": "nonempty",
+      "attrs": {
+        "symbols": [
+          "R"
+        ],
+        "keywords": [
+          "nonempty"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "ring defined by additive group associativity distributivity",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "ring",
+          "defined",
+          "by",
+          "additive",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:2c420bf6ec32069ecd0043dc:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "R": {
+      "name": "R",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "own": {
+      "name": "own",
+      "kind": "own",
+      "type": "structure",
+      "attrs": {
+        "keyword": "structure",
+        "references": [],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P51

source

{
+  "name": "schema:p0-f12735802ba0:25af34567cb2040bf41869e5:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "C_4",
+      "kind": "object",
+      "context": "fourth roots",
+      "attrs": {
+        "symbols": [
+          "C_4"
+        ],
+        "keywords": [
+          "fourth",
+          "roots"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "complex multiplication",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "complex",
+          "multiplication"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "specified roots form group with identity",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "specified",
+          "roots",
+          "form",
+          "group",
+          "with"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P52

source

{
+  "name": "schema:p0-f12735802ba0:578ae89f353ecbdc0ffb76a2:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "K",
+      "kind": "object",
+      "context": "field",
+      "attrs": {
+        "symbols": [
+          "K"
+        ],
+        "keywords": [
+          "field"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "polynomials over field",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "polynomials",
+          "over",
+          "field"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "commutative ring identity units constant",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "commutative",
+          "ring",
+          "identity",
+          "units",
+          "constant"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:578ae89f353ecbdc0ffb76a2:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "K": {
+      "name": "K",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Field K"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\\\[isCommutativeRing (Polynomial K) ∧ (1 : Polynomial K) = 1 ∧ ∀ p : Polynomial K, IsUnit p → ∃ a : K, p = C a := by \\\\- sorry",
+      "attrs": {
+        "exists_count": 1,
+        "forall_count": 1,
+        "is_iff": false,
+        "references": [
+          "K"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P53

source

{
+  "name": "schema:p0-f12735802ba0:1a8d6a5c9aa3cc5000dee474:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "group order is cardinality",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "group",
+          "order",
+          "is",
+          "cardinality"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:1a8d6a5c9aa3cc5000dee474:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G",
+          "Fintype G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "own": {
+      "name": "own",
+      "kind": "own",
+      "type": "ℕ",
+      "attrs": {
+        "keyword": "def",
+        "references": [],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P54

source

{
+  "name": "schema:p0-f12735802ba0:450c7df89ecd284b0e08504a:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "n",
+      "kind": "object",
+      "context": "modulus",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "modulus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "d",
+      "kind": "object",
+      "context": "residue",
+      "attrs": {
+        "symbols": [
+          "d"
+        ],
+        "keywords": [
+          "residue"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "object3",
+      "kind": "object",
+      "context": "generated cyclic subgroup",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "generated",
+          "cyclic",
+          "subgroup"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "subgroup equals integer and residue multiples",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "subgroup",
+          "equals",
+          "integer",
+          "and",
+          "residue"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:450c7df89ecd284b0e08504a:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "d": {
+      "name": "d",
+      "kind": "object",
+      "type": "ℕ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hn": {
+      "name": "hn",
+      "kind": "fact",
+      "type": "0 < n",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "n"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\\\\\n  (ZMod n).subgroup.closure ({ZMod.mk d} : Set (ZMod n)) = \\\\\\n  {ZMod.mk (k * d % n) | k : ℤ} = \\\\\\n  {ZMod.mk (k * d % n) | k : ZMod n}",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "d",
+          "n"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P55

source

{
+  "name": "schema:p0-f12735802ba0:f908ac15b1bf8228281bcf68:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "first group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "first",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "second group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "second",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "fact1",
+      "kind": "fact",
+      "context": "groups are isomorphic",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "groups",
+          "are",
+          "isomorphic"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "abelian properties equivalent",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "abelian",
+          "properties",
+          "equivalent"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:f908ac15b1bf8228281bcf68:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "H": {
+      "name": "H",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group H"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "iso": {
+      "name": "iso",
+      "kind": "fact",
+      "type": "G ≃* H",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G",
+          "H"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "(IsAbelian G ↔ IsAbelian H)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": true,
+        "references": [
+          "G",
+          "H"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P56

source

{
+  "name": "schema:p0-f12735802ba0:bcdfa01447e7060e1fd3d935:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "RSA method",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "rsa",
+          "method"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "message",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "message"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "design message authentication method",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "design",
+          "message",
+          "authentication",
+          "method"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P57

source

{
+  "name": "schema:p0-f12735802ba0:f86421f93f1381d2ce728bc1:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "R",
+      "kind": "object",
+      "context": "ring",
+      "attrs": {
+        "symbols": [
+          "R"
+        ],
+        "keywords": [
+          "ring"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "S",
+      "kind": "object",
+      "context": "ring",
+      "attrs": {
+        "symbols": [
+          "S"
+        ],
+        "keywords": [
+          "ring"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "f",
+      "kind": "object",
+      "context": "map",
+      "attrs": {
+        "symbols": [
+          "f"
+        ],
+        "keywords": [
+          "map"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "a",
+      "kind": "object",
+      "context": "ring element",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "ring",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object5": {
+      "name": "b",
+      "kind": "object",
+      "context": "ring element",
+      "attrs": {
+        "symbols": [
+          "b"
+        ],
+        "keywords": [
+          "ring",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "homomorphism preserves operations bijective means isomorphism",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "homomorphism",
+          "preserves",
+          "operations",
+          "bijective",
+          "means"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:f86421f93f1381d2ce728bc1:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "R": {
+      "name": "R",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Ring R"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "S": {
+      "name": "S",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Ring S"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "f": {
+      "name": "f",
+      "kind": "object",
+      "type": "R → S",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "R",
+          "S"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "Function.IsRingHom f ↔ (∀ a b : R, f (a + b) = f a + f b ∧ f (a * b) = f a * f b)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 1,
+        "is_iff": true,
+        "references": [
+          "R",
+          "f"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P58

source

{
+  "name": "schema:p0-f12735802ba0:89fe687db9136379cd276fff:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "cyclic group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "cyclic",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "rectangle symmetry group",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "rectangle",
+          "symmetry",
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "nonisomorphic groups of order four",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "nonisomorphic",
+          "groups",
+          "of",
+          "order",
+          "four"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P59

source

{
+  "name": "schema:p0-f12735802ba0:da65aa56505f6c13e6553d0d:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "H",
+      "kind": "object",
+      "context": "subset",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "subset"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "H",
+      "kind": "fact",
+      "context": "nonempty",
+      "attrs": {
+        "symbols": [
+          "H"
+        ],
+        "keywords": [
+          "nonempty"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "subgroup iff group under inherited operation",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "subgroup",
+          "iff",
+          "group",
+          "under",
+          "inherited"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:da65aa56505f6c13e6553d0d:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "H": {
+      "name": "H",
+      "kind": "object",
+      "type": "Set G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h_nonempty": {
+      "name": "h_nonempty",
+      "kind": "object",
+      "type": "H.Nonempty",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "H"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "Subgroup.of G H ↔ IsGroup (H, (*), 1, ⁻¹)",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": true,
+        "references": [
+          "G",
+          "H"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P60

source

{
+  "name": "schema:p0-f12735802ba0:ab2990e9786d5bda5a04e067:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "T",
+      "kind": "object",
+      "context": "map",
+      "attrs": {
+        "symbols": [
+          "T"
+        ],
+        "keywords": [
+          "map"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "three dimensional space",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "three",
+          "dimensional",
+          "space"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "T",
+      "kind": "fact",
+      "context": "bijective",
+      "attrs": {
+        "symbols": [
+          "T"
+        ],
+        "keywords": [
+          "bijective"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "T",
+      "kind": "fact",
+      "context": "continuous first partial derivatives",
+      "attrs": {
+        "symbols": [
+          "T"
+        ],
+        "keywords": [
+          "continuous",
+          "first",
+          "partial",
+          "derivatives"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "diffeomorphisms form group under composition",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "diffeomorphisms",
+          "form",
+          "group",
+          "under",
+          "composition"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:ab2990e9786d5bda5a04e067:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "U": {
+      "name": "U",
+      "kind": "object",
+      "type": "Set (ℝ × ℝ × ℝ)",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "hU": {
+      "name": "hU",
+      "kind": "fact",
+      "type": "IsOpen U",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "predicate",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "U"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\\\\\n  Group (Subtype (fun T : (ℝ × ℝ × ℝ) → (ℝ × ℝ × ℝ) => \\\\\\n    Bijective T ∧ DifferentiableOn ℝ T U ∧ ContinuousOn (fun x => deriv (T ∘ (Prod.fst, Prod.snd, Prod.third)) x) U))",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "U"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P61

source

{
+  "name": "schema:p0-f12735802ba0:a892779bfcaca35b91e7d611:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "T",
+      "kind": "object",
+      "context": "map",
+      "attrs": {
+        "symbols": [
+          "T"
+        ],
+        "keywords": [
+          "map"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "three dimensional space",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "three",
+          "dimensional",
+          "space"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "T",
+      "kind": "fact",
+      "context": "bijective",
+      "attrs": {
+        "symbols": [
+          "T"
+        ],
+        "keywords": [
+          "bijective"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "T",
+      "kind": "fact",
+      "context": "continuous",
+      "attrs": {
+        "symbols": [
+          "T"
+        ],
+        "keywords": [
+          "continuous"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact3": {
+      "name": "T",
+      "kind": "fact",
+      "context": "inverse continuous",
+      "attrs": {
+        "symbols": [
+          "T"
+        ],
+        "keywords": [
+          "inverse",
+          "continuous"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "homeomorphisms form group under composition",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "homeomorphisms",
+          "form",
+          "group",
+          "under",
+          "composition"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.

P62

source

{
+  "name": "schema:p0-f12735802ba0:7593062cab7c74cdecec08d0:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "a",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "a",
+      "kind": "fact",
+      "context": "finite order",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "finite",
+          "order"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object1"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "least positive exponent bounded powers generate",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "least",
+          "positive",
+          "exponent",
+          "bounded",
+          "powers"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:7593062cab7c74cdecec08d0:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "ha": {
+      "name": "ha",
+      "kind": "fact",
+      "type": "IsOfFinOrder a",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "predicate",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "a"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "\\/\\/ (orderOf a = (min {n : ℕ | n > 0 ∧ a ^ n = 1})) ∧ (Subgroup.closure ({a} : Set G) = {a ^ k | k : ℕ, k < orderOf a})",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "G",
+          "a"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P63

source

{
+  "name": "schema:p0-f12735802ba0:c8204e9d19a6dd5d730dccc7:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "G",
+      "kind": "object",
+      "context": "group",
+      "attrs": {
+        "symbols": [
+          "G"
+        ],
+        "keywords": [
+          "group"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "e",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "e"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "e'",
+      "kind": "object",
+      "context": "group element",
+      "attrs": {
+        "symbols": [
+          "e'"
+        ],
+        "keywords": [
+          "group",
+          "element"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "e",
+      "kind": "fact",
+      "context": "two sided identity",
+      "attrs": {
+        "symbols": [
+          "e"
+        ],
+        "keywords": [
+          "two",
+          "sided",
+          "identity"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact2": {
+      "name": "e'",
+      "kind": "fact",
+      "context": "two sided identity",
+      "attrs": {
+        "symbols": [
+          "e'"
+        ],
+        "keywords": [
+          "two",
+          "sided",
+          "identity"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object3"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "two identities equal",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "two",
+          "identities",
+          "equal"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:c8204e9d19a6dd5d730dccc7:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "G": {
+      "name": "G",
+      "kind": "object",
+      "type": "Type*",
+      "attrs": {
+        "binder_kind": "implicit",
+        "classified_by": "sort",
+        "origin": "deterministic_signature_projection",
+        "instances": [
+          "Group G"
+        ],
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "e": {
+      "name": "e",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "e'": {
+      "name": "e'",
+      "kind": "object",
+      "type": "G",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h_e": {
+      "name": "h_e",
+      "kind": "fact",
+      "type": "∀ g : G, e * g = g ∧ g * e = g",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G",
+          "e"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h_e'": {
+      "name": "h_e'",
+      "kind": "fact",
+      "type": "∀ g : G, e' * g = g ∧ g * e' = g",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "G",
+          "e'"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "e = e'",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "e",
+          "e'"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P64

source

{
+  "name": "schema:p0-f12735802ba0:b40279b634fffd0841ff0f5a:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": false,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "a",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "a"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "b",
+      "kind": "object",
+      "context": "integer",
+      "attrs": {
+        "symbols": [
+          "b"
+        ],
+        "keywords": [
+          "integer"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object3": {
+      "name": "r",
+      "kind": "object",
+      "context": "exponent",
+      "attrs": {
+        "symbols": [
+          "r"
+        ],
+        "keywords": [
+          "exponent"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object4": {
+      "name": "s",
+      "kind": "object",
+      "context": "exponent",
+      "attrs": {
+        "symbols": [
+          "s"
+        ],
+        "keywords": [
+          "exponent"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object5": {
+      "name": "n",
+      "kind": "object",
+      "context": "modulus",
+      "attrs": {
+        "symbols": [
+          "n"
+        ],
+        "keywords": [
+          "modulus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "fact1": {
+      "name": "b",
+      "kind": "fact",
+      "context": "congruent to power modulo n",
+      "attrs": {
+        "symbols": [
+          "b"
+        ],
+        "keywords": [
+          "congruent",
+          "to",
+          "power",
+          "modulo",
+          "n"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [
+          "object2"
+        ],
+        "reference_status": "explicit_symbol_candidates",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "ciphertext power returns original residue",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "ciphertext",
+          "power",
+          "returns",
+          "original",
+          "residue"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

{
+  "name": "schema:p0-f12735802ba0:b40279b634fffd0841ff0f5a:lean:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "lean",
+    "reference_completeness": "syntactic_only"
+  },
+  "roles": {
+    "a": {
+      "name": "a",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "b": {
+      "name": "b",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "r": {
+      "name": "r",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "s": {
+      "name": "s",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "n": {
+      "name": "n",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "t": {
+      "name": "t",
+      "kind": "object",
+      "type": "ℤ",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "default",
+        "origin": "deterministic_signature_projection",
+        "references": [],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h1": {
+      "name": "h1",
+      "kind": "fact",
+      "type": "b ≡ a^r [ZMOD n]",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "a",
+          "b",
+          "n",
+          "r"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "h2": {
+      "name": "h2",
+      "kind": "fact",
+      "type": "r * s = 1 + n * t",
+      "attrs": {
+        "binder_kind": "explicit",
+        "classified_by": "relation",
+        "origin": "deterministic_signature_projection",
+        "references": [
+          "n",
+          "r",
+          "s",
+          "t"
+        ],
+        "reference_status": "syntactic_candidates"
+      }
+    },
+    "goal": {
+      "name": "goal",
+      "kind": "goal",
+      "type": "b^s ≡ a [ZMOD n]",
+      "attrs": {
+        "exists_count": 0,
+        "forall_count": 0,
+        "is_iff": false,
+        "references": [
+          "a",
+          "b",
+          "n",
+          "s"
+        ],
+        "reference_status": "syntactic_candidates",
+        "origin": "deterministic_signature_projection"
+      }
+    }
+  }
+}

P65

source

{
+  "name": "schema:p0-f12735802ba0:f8d2e206681972927560be2c:source:v1",
+  "kind": "simplex",
+  "attrs": {
+    "side": "source",
+    "goal_has_exists": true,
+    "reference_completeness": "partial"
+  },
+  "roles": {
+    "object1": {
+      "name": "object1",
+      "kind": "object",
+      "context": "nonsquare rhombus",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "nonsquare",
+          "rhombus"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "object2": {
+      "name": "object2",
+      "kind": "object",
+      "context": "geometric symmetries",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "geometric",
+          "symmetries"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    },
+    "goal1": {
+      "name": "goal1",
+      "kind": "goal",
+      "context": "identify symmetry group size and classification",
+      "attrs": {
+        "symbols": [],
+        "keywords": [
+          "identify",
+          "symmetry",
+          "group",
+          "size",
+          "and"
+        ],
+        "introduced": "given",
+        "quantifier_status": "unreviewed",
+        "references": [],
+        "reference_status": "unknown",
+        "origin": "frozen_current_chat_annotation"
+      }
+    }
+  }
+}

lean

Insufficient projected roles; no object roles were invented.
\ No newline at end of file diff --git a/docs/simplex-schema.md b/docs/simplex-schema.md index 4a1c8d8..1306567 100644 --- a/docs/simplex-schema.md +++ b/docs/simplex-schema.md @@ -137,14 +137,20 @@ Private outputs under `experiments/P0-pilot/data/simplex-schemas-v1/`: - `registry.sqlite`: queryable catalog with the 115 schemas and scoped slots. - `schemas.json`: all 65 source/Lean pairs, retaining incomplete Lean projections. -- `schemas.html`: a local review of all 65 pairs. +- `schemas.html`: a local generated copy of the schema-only review tracked below. - `schema-inputs.json`: input hashes; an existing directory rejects changed inputs. -Tracked, text-free outputs: +Tracked outputs: - `experiments/P0-pilot/results/simplex-schema-index.json`: 65 item IDs, schema keys, role counts, coverage status and reference-candidate counts. - `experiments/P0-pilot/results/simplex-schema-summary.json`: coverage, limitations and hashes. +- [65-item schema review](reviews/simplex-schemas.html): an owner-approved, self-contained + HTML view of all 65 source/Lean pairs. It includes schema role descriptions and Lean + signature expressions, but no textbook paragraphs or full assistant judgment explanations. + Open the file in a browser after cloning, or download it from the repository; the Git web + interface may display HTML source instead of rendering it. The JSON indexes above remain + text-free counts/keys. Full source-inclusive inputs and assessment files remain gitignored. Replay from the repository root with private inputs present: @@ -155,7 +161,8 @@ PYTHONPATH=. python3 experiments/P0-pilot/build_schemas.py \ --key experiments/P0-pilot/labels/key.json \ --private-out experiments/P0-pilot/data/simplex-schemas-v1 \ --index experiments/P0-pilot/results/simplex-schema-index.json \ - --summary experiments/P0-pilot/results/simplex-schema-summary.json + --summary experiments/P0-pilot/results/simplex-schema-summary.json \ + --review-page docs/reviews/simplex-schemas.html ``` The original annotations, judgments, Qwen results and matcher thresholds remain unchanged. diff --git a/experiments/P0-pilot/README.md b/experiments/P0-pilot/README.md index adfb31b..8977f09 100644 --- a/experiments/P0-pilot/README.md +++ b/experiments/P0-pilot/README.md @@ -75,3 +75,7 @@ structural candidate queries, bindings and replay command. Private SQLite/JSON/H stay under `data/simplex-schemas-v1/`; tracked `results/simplex-schema-*.json` files contain only counts, opaque keys, provenance hashes and coverage status. This does not change the frozen diagnostic or claim complete semantic extraction or proof verification. + +The owner-approved schema-only HTML review is tracked at +`docs/reviews/simplex-schemas.html`. Regenerate it with the builder's `--review-page` option; +the raw inputs, full assessment explanations and SQLite snapshot remain gitignored. diff --git a/experiments/P0-pilot/build_schemas.py b/experiments/P0-pilot/build_schemas.py index 5f7ac11..95465c0 100644 --- a/experiments/P0-pilot/build_schemas.py +++ b/experiments/P0-pilot/build_schemas.py @@ -114,6 +114,8 @@ def main(): parser.add_argument("--private-out", required=True, type=Path) parser.add_argument("--index", required=True, type=Path) parser.add_argument("--summary", required=True, type=Path) + parser.add_argument("--review-page", type=Path, + help="Also export the owner-approved schema-only HTML review into the project") args = parser.parse_args() if "data" not in args.private_out.parts: parser.error("Private schemas must remain in the gitignored data/ directory") @@ -149,14 +151,20 @@ def main(): sides.append(f'

{side}

{html.escape(content)}
') sections.append(f'

{row["blind_id"]}

' + ''.join(sides) + '
') - (args.private_out / "schemas.html").write_text( + review_page = ( 'P0 semantic simplex schemas' '' '

65 semantic multi-role relation schemas

' - '

Private annotation seeds, not independently validated mathematical statements. ' + '

Schema annotation seeds, not independently validated mathematical statements. ' 'A simplex joins the objects, assumptions and conclusion in its slots. ' - 'References are partial symbol/syntax candidates.

' + ''.join(sections) + '') + 'References are partial symbol/syntax candidates. ' + 'This review contains schema annotations and Lean signature text, not textbook passages ' + 'or full assistant judgment explanations.

' + ''.join(sections) + '') + (args.private_out / "schemas.html").write_text(review_page, encoding="utf-8") + if args.review_page is not None: + args.review_page.parent.mkdir(parents=True, exist_ok=True) + args.review_page.write_text(review_page, encoding="utf-8") # JSON-only reload is independently checked; it does not use pickle. for row in snapshots: for side in ["source", "lean"]: diff --git a/experiments/P0-pilot/results/simplex-schema-summary.json b/experiments/P0-pilot/results/simplex-schema-summary.json index e63ef98..8e7ac8c 100644 --- a/experiments/P0-pilot/results/simplex-schema-summary.json +++ b/experiments/P0-pilot/results/simplex-schema-summary.json @@ -13,7 +13,7 @@ "items": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed", "assessments": "f12735802ba0d4d94b776a91581a13a508eab0ce90ba8973a6c9c4e4d1390272", "key": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836", - "builder": "3c8a7112f2d86737b646fbc9abfe5e9b8660efabc1023f2cc3357398445675e9", + "builder": "7b3a982101f620c1480d95b5e483ca6186a7e9c32ce587fb132a90bfb38a01bc", "schema_module": "958b81e89c0befeb32d24036c130f2b37bd2e881bd5b009acf873cbcdada50ae", "registry_module": "7b434b1eb178f597d4f60591a5ab74eff0c96a40fa751cb0ba75589b52e56271" },