Lean4の定理の証明エラーを修正します

既存Lean4プロジェクトの定理1件について、小規模な証明エラーを修正します。Std・mathlibの版、命題、依存関係を購入前に確認し、対応できる範囲を見積ります。 【5,000円の内容】 合意した定理1件の最小修正パッチ、変更理由の日本語説明、固定環境での再現手順、検証ログを納品します。新規理論整備、未証明の研究定理、全体移植・環境構築は含みません。情報と制作範囲を双方で確定してから7日を目安に、購入前に納期を合意します。修正不能と判明した場合はキャンセルを相談し、診断だけで満額の完成納品扱いにはしません。 【検証条件】 Lean・依存の版を固定し、全納品Leanファイルをビルド対象に含めます。lake build成功ログと各納品定理の#print axioms結果を添え、数学的な意図とLeanの型の対応を説明します。許容公理はpropext・Classical.choice・Quot.soundのみ、または公理なし。sorry/admit、独自axiom、native評価由来の追加公理で完成扱いにしません。型・仮定・結論の変更は事前合意が必要です。 【AI・権利・課題】 調査・修正案・説明作成に生成AIを使い、コードを実検証します。依頼コード・資料を外部AIへ送る前に、使用サービス、送信情報、目的を確認し、同意を得ます。共有は権限のある最小限の資料に限り、第三者ライセンス表示を保持します。利用範囲は事前合意します。評価対象の提出課題・試験・レポートの代作や完成答案は作成しません。 【訂正・質問】 納品後7日以内に連絡いただいた合意内容への不備・誤記・数学的誤りは無償訂正します。別枠で同期限内の不明点への質問を1往復まで受け付けます。別定理・新しい版への対応は追加相談です。