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.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.
{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}{
"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"
}
}
}
}Insufficient projected roles; no object roles were invented.