"""
Proof: The viral expression "8 ÷ 2(2+2)" equals 1
Generated: 2026-03-28
"""
import json
import os
import sys

PROOF_ENGINE_ROOT = os.environ.get("PROOF_ENGINE_ROOT")
if not PROOF_ENGINE_ROOT:
    _d = os.path.dirname(os.path.abspath(__file__))
    while _d != os.path.dirname(_d):
        if os.path.isdir(os.path.join(_d, "proof-engine", "skills", "proof-engine", "scripts")):
            PROOF_ENGINE_ROOT = os.path.join(_d, "proof-engine", "skills", "proof-engine")
            break
        _d = os.path.dirname(_d)
    if not PROOF_ENGINE_ROOT:
        raise RuntimeError("PROOF_ENGINE_ROOT not set and skill dir not found via walk-up from proof.py")
sys.path.insert(0, PROOF_ENGINE_ROOT)
from datetime import date

from scripts.computations import compare, explain_calc, cross_check
from scripts.verify_citations import verify_all_citations, build_citation_detail

# ── 1. CLAIM INTERPRETATION (Rule 4) ──────────────────────────────────────────
CLAIM_NATURAL = 'The viral expression "8 ÷ 2(2+2)" equals 1'
CLAIM_FORMAL = {
    "subject": "8 ÷ 2(2+2)",
    "property": "numeric value under standard mathematical operator precedence",
    "operator": "==",
    "operator_note": (
        "Two competing conventions exist for this expression. "
        "(Convention A — Strict PEMDAS / ISO 80000-2): division and multiplication "
        "share equal precedence and are evaluated left-to-right; implicit multiplication "
        "(juxtaposition) is treated identically to explicit '×'. This convention is "
        "implemented by Python, most modern scientific calculators, and the US Common Core "
        "curriculum. Under it: 8 ÷ 2(2+2) = 8 ÷ 2 × 4 = 4 × 4 = 16. "
        "(Convention B — Juxtaposition-Priority): implicit multiplication binds more tightly "
        "than explicit division, so '2(2+2)' is treated as a single unit. Under it: "
        "8 ÷ [2×(2+2)] = 8 ÷ 8 = 1. "
        "The claimed answer is 1. This proof evaluates whether 1 is the correct result "
        "under the dominant modern convention (Convention A). It is not: the answer is 16. "
        "The juxtaposition convention (Convention B) is documented as the adversarial case."
    ),
    "threshold": 1,
}

# ── 2. FACT REGISTRY ──────────────────────────────────────────────────────────
FACT_REGISTRY = {
    "A1": {
        "label": "Value under strict PEMDAS (left-to-right, implicit = explicit mult)",
        "method": None,
        "result": None,
    },
    "A2": {
        "label": "Value under juxtaposition-priority convention",
        "method": None,
        "result": None,
    },
    "A3": {
        "label": "Python eval cross-check (implements strict PEMDAS)",
        "method": None,
        "result": None,
    },
    "B1": {
        "key": "wikipedia_order_of_ops",
        "label": "Wikipedia 'Order of operations' — both conventions documented",
    },
}

# ── 3. EMPIRICAL FACTS ────────────────────────────────────────────────────────
empirical_facts = {
    "wikipedia_order_of_ops": {
        "quote": (
            "Multiplication denoted by juxtaposition (also known as implied multiplication) "
            "creates a visual unit and is often given higher precedence than most other operations."
        ),
        "url": "https://en.wikipedia.org/wiki/Order_of_operations",
        "source_name": "Wikipedia — Order of operations",
    },
}

# ── 4. CITATION VERIFICATION (Rule 2) ─────────────────────────────────────────
citation_results = verify_all_citations(empirical_facts, wayback_fallback=True)

# ── 5. TYPE A COMPUTATIONS ────────────────────────────────────────────────────

# Convention A: strict PEMDAS — evaluate left to right
# Step 1: parentheses → 2+2 = 4
inner = explain_calc("2 + 2", locals(), label="A1-step1: parentheses 2+2")
# Step 2: left-to-right — 8 ÷ 2 first
div_result = explain_calc("8 / 2", locals(), label="A1-step2: left-to-right 8÷2")
# Step 3: then × inner
pemdas_result = explain_calc("div_result * inner", locals(), label="A1-step3: × (2+2)")

# Convention B: juxtaposition priority — 2(2+2) is one unit
juxt_unit = explain_calc("2 * inner", locals(), label="A2-step1: juxtaposition 2×(2+2)")
juxt_result = explain_calc("8 / juxt_unit", locals(), label="A2-step2: 8 ÷ [2(2+2)]")

# Cross-check A1 via Python expression (strict left-to-right)
python_eval = explain_calc("8 / 2 * (2 + 2)", locals(), label="A3: Python eval 8/2*(2+2)")

# ── 6. CROSS-CHECKS (Rule 6) ──────────────────────────────────────────────────
# A1 and A3 use two independent evaluation methods — both should give 16
pemdas_agrees_python = cross_check(
    pemdas_result, python_eval,
    tolerance=0.0, mode="absolute",
    label="A1 vs A3: step-by-step vs Python eval (both strict PEMDAS)"
)

# ── 7. ADVERSARIAL CHECKS (Rule 5) ────────────────────────────────────────────
adversarial_checks = [
    {
        "question": (
            "Do authoritative mathematical bodies endorse juxtaposition-priority "
            "(the convention that gives 1)?"
        ),
        "verification_performed": (
            "Reviewed the Wikipedia 'Order of operations' article and academic literature. "
            "The juxtaposition-priority convention is used in some academic physics and "
            "mathematics writing (e.g., 'Physical Review' style), and some textbooks state "
            "that implied multiplication ranks above explicit division. However, no major "
            "standards body (ISO, ANSI, NIST) mandates juxtaposition-priority for general "
            "arithmetic expressions — ISO 80000-2 treats multiplication and division as "
            "equal-precedence left-to-right operators. The juxtaposition convention is a "
            "domain-specific style choice, not a universal rule."
        ),
        "finding": (
            "Juxtaposition-priority is a legitimate but minority convention. It is not "
            "adopted by ISO 80000-2, Python, most modern calculators, or the US K-12 "
            "curriculum. The expression '8 ÷ 2(2+2)' is genuinely ambiguous; neither "
            "answer is 'wrong' in absolute terms — the ambiguity is the point."
        ),
        "breaks_proof": False,
    },
    {
        "question": (
            "Do major programming languages and calculators agree that the answer is 16 "
            "under strict PEMDAS?"
        ),
        "verification_performed": (
            "Python: eval('8 / 2 * (2 + 2)') = 16.0 (verified computationally in this "
            "script). WolframAlpha: evaluates '8÷2(2+2)' as 16 by default. Texas Instruments "
            "TI-84: returns 16. Desmos calculator: returns 16. All implement strict "
            "left-to-right evaluation for equal-precedence operators."
        ),
        "finding": (
            "All major computational tools that implement strict PEMDAS return 16. "
            "None return 1 under their default settings. This does not break the proof — "
            "it confirms that under the dominant modern convention, the answer is 16, "
            "disproving the claim of 1."
        ),
        "breaks_proof": False,
    },
    {
        "question": (
            "Could the expression be intentionally written to exploit ambiguity, making "
            "both 1 and 16 equally 'correct'?"
        ),
        "verification_performed": (
            "The expression deliberately omits parentheses to create ambiguity between "
            "'(8÷2)×(2+2)' and '8÷(2×(2+2))'. Mathematical style guides (APA, AMS) "
            "universally recommend using explicit parentheses to disambiguate such "
            "expressions. The 'war' persists because the expression is intentionally "
            "poorly written."
        ),
        "finding": (
            "The expression is a syntactic trap. The 'correct' answer depends entirely "
            "on convention. The claim that it 'equals 1' is convention-dependent, not "
            "universally true. Under the dominant modern standard, it equals 16."
        ),
        "breaks_proof": False,
    },
]

# ── 8. VERDICT AND STRUCTURED OUTPUT ──────────────────────────────────────────
if __name__ == "__main__":
    # Under strict PEMDAS (the dominant modern convention), the expression = 16, not 1.
    # The claim asserts == 1. We compare the actual result to the claimed threshold of 1.
    claim_holds = compare(
        pemdas_result, "==", CLAIM_FORMAL["threshold"],
        label="SC1: 8÷2(2+2) == 1 under strict PEMDAS?"
    )
    # Also document the juxtaposition result for completeness
    compare(
        juxt_result, "==", CLAIM_FORMAL["threshold"],
        label="SC2: 8÷2(2+2) == 1 under juxtaposition-priority?"
    )

    any_unverified = any(
        cr["status"] != "verified" for cr in citation_results.values()
    )

    if not claim_holds and not any_unverified:
        verdict = "DISPROVED"
    elif not claim_holds and any_unverified:
        verdict = "DISPROVED (with unverified citations)"
    else:
        verdict = "PROVED"  # unreachable given math, but required by template

    FACT_REGISTRY["A1"]["method"] = "explain_calc(): step-by-step strict PEMDAS"
    FACT_REGISTRY["A1"]["result"] = str(pemdas_result)
    FACT_REGISTRY["A2"]["method"] = "explain_calc(): juxtaposition-priority"
    FACT_REGISTRY["A2"]["result"] = str(juxt_result)
    FACT_REGISTRY["A3"]["method"] = "explain_calc(): Python 8/2*(2+2)"
    FACT_REGISTRY["A3"]["result"] = str(python_eval)

    citation_detail = build_citation_detail(FACT_REGISTRY, citation_results, empirical_facts)

    summary = {
        "fact_registry": {
            fid: {k: v for k, v in info.items()}
            for fid, info in FACT_REGISTRY.items()
        },
        "claim_formal": CLAIM_FORMAL,
        "claim_natural": CLAIM_NATURAL,
        "citations": citation_detail,
        "extractions": {
            # B1 establishes that the juxtaposition convention exists — no numeric value extracted
            "B1": {
                "value": citation_results["wikipedia_order_of_ops"]["status"],
                "value_in_quote": citation_results["wikipedia_order_of_ops"]["status"] in ("verified", "partial"),
                "quote_snippet": empirical_facts["wikipedia_order_of_ops"]["quote"][:80],
            },
        },
        "cross_checks": [
            {
                "description": "Step-by-step PEMDAS (A1) vs Python eval (A3) — both strict left-to-right",
                "values_compared": [str(pemdas_result), str(python_eval)],
                "agreement": pemdas_agrees_python,
            },
        ],
        "adversarial_checks": adversarial_checks,
        "verdict": verdict,
        "key_results": {
            "pemdas_result": pemdas_result,
            "juxtaposition_result": juxt_result,
            "claimed_value": CLAIM_FORMAL["threshold"],
            "claim_holds_under_pemdas": bool(claim_holds),
            "claim_holds_under_juxtaposition": bool(juxt_result == 1),
        },
        "generator": {
            "name": "proof-engine",
            "version": open(os.path.join(PROOF_ENGINE_ROOT, "VERSION")).read().strip(),
            "repo": "https://github.com/yaniv-golan/proof-engine",
            "generated_at": date.today().isoformat(),
        },
    }

    print("\n=== PROOF SUMMARY (JSON) ===")
    print(json.dumps(summary, indent=2, default=str))
