"A real number is rational if and only if its decimal expansion is eventually periodic."

"""
Proof: A real number is rational if and only if its decimal expansion is eventually periodic.
Generated: 2026-03-28

This is a pure-math proof verified computationally in both directions:
  (⇒) Every rational p/q has an eventually periodic decimal expansion (long division + pigeonhole).
  (⇐) Every eventually periodic decimal equals a rational number (algebraic conversion).
"""
import json
import os
import sys
from fractions import Fraction

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

# ============================================================================
# 1. CLAIM INTERPRETATION (Rule 4)
# ============================================================================
CLAIM_NATURAL = "A real number is rational if and only if its decimal expansion is eventually periodic."
CLAIM_FORMAL = {
    "subject": "real numbers and their decimal expansions",
    "property": "biconditional equivalence between rationality and eventual periodicity",
    "operator": "==",
    "operator_note": (
        "This is a biconditional (iff) claim with two directions: "
        "(1) rational ⇒ eventually periodic, and (2) eventually periodic ⇒ rational. "
        "Both must hold for the claim to be PROVED. "
        "'Eventually periodic' means there exist non-negative integers k (pre-period length) "
        "and p ≥ 1 (period length) such that for all n ≥ k, digit d(n) = d(n+p). "
        "A terminating decimal is eventually periodic with repeating 0s (or equivalently 9s). "
        "We verify computationally by testing both directions on a comprehensive set of cases."
    ),
    "threshold": True,
}

# ============================================================================
# 2. FACT REGISTRY — A-types only for pure math
# ============================================================================
FACT_REGISTRY = {
    "A1": {
        "label": "Direction 1: Long division of p/q produces eventually periodic digits (pigeonhole on remainders)",
        "method": None,
        "result": None,
    },
    "A2": {
        "label": "Direction 2: Every eventually periodic decimal converts to a fraction p/q",
        "method": None,
        "result": None,
    },
    "A3": {
        "label": "Cross-check: Python Fraction confirms rational ↔ periodic equivalence",
        "method": None,
        "result": None,
    },
}

# ============================================================================
# 3. COMPUTATION — Direction 1: Rational → Eventually Periodic
# ============================================================================

def long_division(p, q, max_digits=2000):
    """Perform long division of |p|/|q| and detect the repeating cycle.

    Returns (pre_period_digits, period_digits) where:
      - pre_period_digits: list of digits before the repeating block
      - period_digits: list of digits in the repeating block (empty if terminates)

    Uses the pigeonhole principle: there are only q possible remainders (0..q-1),
    so within at most q steps a remainder must repeat, starting a cycle.
    """
    p, q = abs(p), abs(q)
    assert q > 0, "Denominator must be positive"

    integer_part = p // q
    remainder = p % q

    digits = []
    remainder_positions = {}  # remainder -> position where it first appeared

    while remainder != 0 and remainder not in remainder_positions:
        remainder_positions[remainder] = len(digits)
        remainder *= 10
        digit = remainder // q
        remainder = remainder % q
        digits.append(digit)

    if remainder == 0:
        # Terminating decimal — period is [0] (repeating zeros)
        return digits, [0]
    else:
        cycle_start = remainder_positions[remainder]
        pre_period = digits[:cycle_start]
        period = digits[cycle_start:]
        return pre_period, period


def verify_direction_1(test_cases):
    """Verify that for each rational p/q, long division produces a periodic expansion,
    and that reconstructing the fraction from the expansion yields the original."""
    all_passed = True
    for p, q in test_cases:
        pre, period = long_division(p, q)
        if len(period) == 0:
            print(f"  FAIL: {p}/{q} returned empty period")
            all_passed = False
            continue

        # Verify pigeonhole bound: period length ≤ q
        if len(period) > abs(q):
            print(f"  FAIL: {p}/{q} period length {len(period)} exceeds q={abs(q)}")
            all_passed = False
            continue

        # Reconstruct the decimal from pre-period and period, convert back to fraction
        reconstructed = periodic_decimal_to_fraction(
            p >= 0, abs(p) // abs(q), pre, period
        )
        original = Fraction(p, q)
        if reconstructed != original:
            print(f"  FAIL: {p}/{q} reconstruction mismatch: got {reconstructed}")
            all_passed = False

    return all_passed


# ============================================================================
# 4. COMPUTATION — Direction 2: Eventually Periodic → Rational
# ============================================================================

def periodic_decimal_to_fraction(positive, integer_part, pre_period_digits, period_digits):
    """Convert an eventually periodic decimal to a Fraction.

    Algorithm: If x = N.d₁d₂...dₖ(r₁r₂...rₚ)  where (r₁...rₚ) repeats,
    then let k = len(pre_period_digits), p = len(period_digits).

    Multiply by 10^k:        10^k · x = (integer with pre-period) + 0.(r₁r₂...rₚ)
    Multiply by 10^(k+p):    10^(k+p) · x = (integer with pre-period and one cycle) + 0.(r₁r₂...rₚ)

    Subtract: (10^(k+p) - 10^k) · x = difference of the two integer parts
    So x = difference / (10^(k+p) - 10^k), which is rational.
    """
    k = len(pre_period_digits)
    p = len(period_digits)

    # Build the integer from all digits (pre-period + one period)
    all_digits = pre_period_digits + period_digits
    # Build the integer from pre-period digits only
    pre_digits = pre_period_digits

    # Numerator of the fractional part:
    # full_num = integer formed by (pre_period_digits + period_digits)
    # pre_num = integer formed by (pre_period_digits) [0 if empty]
    full_num = 0
    for d in all_digits:
        full_num = full_num * 10 + d
    pre_num = 0
    for d in pre_digits:
        pre_num = pre_num * 10 + d

    # Handle the all-zeros period (terminating decimal)
    if all(d == 0 for d in period_digits):
        # Terminating: fractional part = pre_num / 10^k
        if k == 0:
            frac = Fraction(integer_part)
        else:
            frac = Fraction(integer_part) + Fraction(pre_num, 10 ** k)
    else:
        # Non-terminating periodic:
        # fractional part = (full_num - pre_num) / (10^(k+p) - 10^k)
        denominator = 10 ** (k + p) - 10 ** k
        numerator = full_num - pre_num
        frac = Fraction(integer_part) + Fraction(numerator, denominator)

    if not positive:
        frac = -frac
    return frac


def verify_direction_2(test_cases):
    """Verify that various eventually periodic decimals convert to rationals,
    and that long division of the result reproduces the original expansion."""
    all_passed = True
    for desc, positive, integer_part, pre, period, expected_fraction in test_cases:
        result = periodic_decimal_to_fraction(positive, integer_part, pre, period)
        if result != expected_fraction:
            print(f"  FAIL [{desc}]: expected {expected_fraction}, got {result}")
            all_passed = False
        else:
            # Round-trip: long divide the result and check we get back the same expansion
            p_val, q_val = result.numerator, result.denominator
            if q_val != 0 and p_val != 0:
                rt_pre, rt_period = long_division(abs(p_val), abs(q_val))
                # Normalize: strip leading zeros from period if needed
                rt_frac = periodic_decimal_to_fraction(
                    result >= 0, abs(p_val) // abs(q_val), rt_pre, rt_period
                )
                if rt_frac != result:
                    print(f"  FAIL [{desc}]: round-trip mismatch: {result} → {rt_frac}")
                    all_passed = False
    return all_passed


# ============================================================================
# 5. TEST CASES
# ============================================================================

# Direction 1 test cases: (p, q) pairs covering diverse rationals
direction_1_cases = [
    # Terminating decimals
    (1, 2),     # 0.5
    (1, 4),     # 0.25
    (1, 5),     # 0.2
    (1, 8),     # 0.125
    (3, 16),    # 0.1875
    (7, 20),    # 0.35
    (1, 25),    # 0.04
    (1, 125),   # 0.008
    # Purely repeating decimals
    (1, 3),     # 0.(3)
    (1, 7),     # 0.(142857)
    (1, 9),     # 0.(1)
    (1, 11),    # 0.(09)
    (1, 13),    # 0.(076923)
    (2, 3),     # 0.(6)
    (5, 7),     # 0.(714285)
    (1, 37),    # 0.(027)
    (1, 41),    # period 5
    (1, 97),    # period 96
    (1, 101),   # period 4
    # Mixed: pre-period + period
    (1, 6),     # 0.1(6)
    (1, 12),    # 0.08(3)
    (7, 12),    # 0.58(3)
    (1, 14),    # mixed
    (1, 15),    # 0.0(6)
    (1, 22),    # 0.0(45)
    (1, 60),    # 0.01(6)
    (17, 90),   # 0.18(8)
    # Larger denominators
    (1, 97),    # period 96 (maximal for prime 97)
    (1, 127),   # period 42
    (1, 239),   # large period
    # Negative rationals
    (-1, 3),
    (-7, 12),
    # Integer rationals
    (5, 1),
    (0, 1),
    (100, 4),
]

# Direction 2 test cases: (desc, positive, integer_part, pre_period, period, expected_fraction)
direction_2_cases = [
    ("1/3 = 0.(3)", True, 0, [], [3], Fraction(1, 3)),
    ("1/7 = 0.(142857)", True, 0, [], [1, 4, 2, 8, 5, 7], Fraction(1, 7)),
    ("1/6 = 0.1(6)", True, 0, [1], [6], Fraction(1, 6)),
    ("1/11 = 0.(09)", True, 0, [], [0, 9], Fraction(1, 11)),
    ("7/12 = 0.58(3)", True, 0, [5, 8], [3], Fraction(7, 12)),
    ("0.5 = 1/2", True, 0, [5], [0], Fraction(1, 2)),
    ("0.125 = 1/8", True, 0, [1, 2, 5], [0], Fraction(1, 8)),
    ("0.(9) = 1", True, 0, [], [9], Fraction(1, 1)),
    ("2.0(3) = 61/30", True, 2, [0], [3], Fraction(61, 30)),
    ("0.(012345679) = 1/81", True, 0, [], [0, 1, 2, 3, 4, 5, 6, 7, 9], Fraction(1, 81)),
    ("-0.(3) = -1/3", False, 0, [], [3], Fraction(-1, 3)),
    ("3.(0) = 3", True, 3, [], [0], Fraction(3, 1)),
    ("0.1(6) = 1/6", True, 0, [1], [6], Fraction(1, 6)),
    ("0.08(3) = 1/12", True, 0, [0, 8], [3], Fraction(1, 12)),
]

# ============================================================================
# 6. CROSS-CHECK: Independent method using Python's Fraction (Rule 6)
# ============================================================================

def crosscheck_via_fraction(max_q=200):
    """Independent cross-check: for all rationals p/q with 1 ≤ q ≤ max_q, 0 ≤ p < q,
    verify that long_division produces a valid periodic expansion and that
    periodic_decimal_to_fraction inverts it exactly.

    This is independent because it exhaustively tests all rationals in range
    rather than using hand-picked cases, and uses Python's Fraction for
    exact arithmetic as the ground truth."""
    failures = 0
    tested = 0
    for q in range(1, max_q + 1):
        for p in range(0, q):
            tested += 1
            original = Fraction(p, q)

            # Direction 1: rational → periodic expansion
            pre, period = long_division(p, q)

            # Direction 2: periodic expansion → rational
            reconstructed = periodic_decimal_to_fraction(True, 0, pre, period)

            if reconstructed != original:
                if failures < 5:
                    print(f"  Cross-check FAIL: {p}/{q} = {original}, reconstructed = {reconstructed}")
                failures += 1

    return tested, failures


# ============================================================================
# 7. ADVERSARIAL CHECKS (Rule 5)
# ============================================================================
adversarial_checks = [
    {
        "question": "Does 0.(9) = 1 break the uniqueness of decimal expansions?",
        "verification_performed": (
            "Tested 0.(9) conversion: periodic_decimal_to_fraction(True, 0, [], [9]) "
            "returns Fraction(1, 1) = 1. This is correct — 0.999... = 1 is a well-known "
            "identity. Decimal representations are not unique, but the theorem holds: "
            "both 1.0(0) and 0.(9) are eventually periodic representations of the rational number 1."
        ),
        "finding": "0.(9) = 1 is handled correctly. Non-uniqueness of decimal representation does not affect the theorem.",
        "breaks_proof": False,
    },
    {
        "question": "Are there irrational numbers with 'almost periodic' expansions that could be mistaken for periodic?",
        "verification_performed": (
            "Considered numbers like √2 = 1.41421356... — the digits never repeat. "
            "The Champernowne constant 0.123456789101112... contains every finite digit string "
            "but is not periodic. Liouville's number has a pattern but is not eventually periodic. "
            "The proof's correctness does not depend on detecting periodicity in arbitrary digit "
            "strings — it depends on the algebraic structure: long division of p/q necessarily "
            "cycles (pigeonhole on q remainders), and any periodic decimal can be algebraically "
            "converted to p/q."
        ),
        "finding": "Almost-periodic irrationals do not affect the proof. The proof works from the algebraic structure, not from digit pattern detection.",
        "breaks_proof": False,
    },
    {
        "question": "Does the proof handle edge cases: 0, negative numbers, integers?",
        "verification_performed": (
            "Tested: 0/1 = 0.0(0) — terminates, periodic with period [0]. "
            "-1/3 = -0.(3) — sign handled separately, fractional part periodic. "
            "5/1 = 5.0(0) — integer, terminates. "
            "100/4 = 25.0(0) — integer result from non-trivial fraction. "
            "All pass both directions."
        ),
        "finding": "Edge cases (zero, negatives, integers) are handled correctly.",
        "breaks_proof": False,
    },
    {
        "question": "Could the pigeonhole argument fail for very large denominators?",
        "verification_performed": (
            "The pigeonhole principle guarantees repetition within q steps for denominator q. "
            "Tested with q=97 (period 96, maximal for a prime), q=127 (period 42), q=239. "
            "The exhaustive cross-check tests all q up to 200. The mathematical argument is "
            "watertight: q possible remainders means at most q steps before a repeat."
        ),
        "finding": "Pigeonhole bound holds for all tested denominators. The argument is valid for all positive q.",
        "breaks_proof": False,
    },
]

# ============================================================================
# 8. VERDICT AND STRUCTURED OUTPUT
# ============================================================================
if __name__ == "__main__":
    print("=" * 70)
    print("PROOF: Rational ↔ Eventually Periodic Decimal Expansion")
    print("=" * 70)

    # --- Direction 1 ---
    print("\n--- Direction 1: Rational ⇒ Eventually Periodic ---")
    print(f"Testing {len(direction_1_cases)} rational numbers via long division...")
    d1_passed = verify_direction_1(direction_1_cases)
    A1_result = d1_passed
    print(f"Direction 1 result: {'ALL PASSED' if d1_passed else 'FAILURES DETECTED'}")

    # Demonstrate the pigeonhole argument on 1/7
    print("\nExample — long division of 1/7:")
    pre, period = long_division(1, 7)
    print(f"  Pre-period digits: {pre}")
    print(f"  Period digits: {period}")
    print(f"  Decimal: 0.({''.join(map(str, period))})")
    explain_calc("len(period)", {"period": period}, label="Period length for 1/7")
    period_bound = explain_calc("q", {"q": 7}, label="Pigeonhole upper bound (= denominator)")
    print(f"  Period length ≤ q: {len(period)} ≤ 7 ✓")

    # --- Direction 2 ---
    print("\n--- Direction 2: Eventually Periodic ⇒ Rational ---")
    print(f"Testing {len(direction_2_cases)} periodic decimals...")
    d2_passed = verify_direction_2(direction_2_cases)
    A2_result = d2_passed
    print(f"Direction 2 result: {'ALL PASSED' if d2_passed else 'FAILURES DETECTED'}")

    # Demonstrate the algebraic conversion on 0.(142857)
    print("\nExample — converting 0.(142857) to a fraction:")
    result_frac = periodic_decimal_to_fraction(True, 0, [], [1, 4, 2, 8, 5, 7])
    print(f"  0.(142857) = {result_frac.numerator}/{result_frac.denominator}")
    explain_calc("142857 / 999999", {"x": 142857, "y": 999999},
                 label="Algebraic: repeating block / (10^p - 1)")

    # Demonstrate 0.999... = 1
    print("\nEdge case — 0.(9):")
    nines_frac = periodic_decimal_to_fraction(True, 0, [], [9])
    print(f"  0.(9) = {nines_frac.numerator}/{nines_frac.denominator} = {float(nines_frac)}")

    # --- Cross-check ---
    print("\n--- Cross-Check: Exhaustive test for q = 1..200 ---")
    tested, failures = crosscheck_via_fraction(max_q=200)
    A3_result = failures == 0
    explain_calc("tested", {"tested": tested}, label="Total rationals tested")
    explain_calc("failures", {"failures": failures}, label="Failures found")
    print(f"Cross-check: {tested} rationals tested, {failures} failures")

    # --- Biconditional verdict ---
    both_directions = compare(A1_result, "==", True, label="Direction 1 (rational ⇒ periodic)")
    both_directions2 = compare(A2_result, "==", True, label="Direction 2 (periodic ⇒ rational)")
    crosscheck_ok = compare(A3_result, "==", True, label="Cross-check (exhaustive q≤200)")

    claim_holds = compare(
        A1_result and A2_result and A3_result, "==", CLAIM_FORMAL["threshold"],
        label="Biconditional: both directions verified + cross-check"
    )
    verdict = "PROVED" if claim_holds else "DISPROVED"

    # --- Adversarial checks ---
    print("\n--- Adversarial Checks ---")
    for ac in adversarial_checks:
        print(f"  Q: {ac['question']}")
        print(f"  Finding: {ac['finding']}")
        print(f"  Breaks proof: {ac['breaks_proof']}")
        print()

    # --- Update fact registry ---
    FACT_REGISTRY["A1"]["method"] = (
        "Long division of p/q tracking remainders; pigeonhole principle guarantees "
        "remainder repetition within q steps, creating a periodic cycle. "
        f"Tested on {len(direction_1_cases)} rationals including terminating, "
        "purely repeating, and mixed cases."
    )
    FACT_REGISTRY["A1"]["result"] = f"All {len(direction_1_cases)} cases passed: expansion is eventually periodic and round-trips to original fraction"

    FACT_REGISTRY["A2"]["method"] = (
        "Algebraic conversion: for decimal 0.d₁...dₖ(r₁...rₚ), multiply by 10^(k+p) and 10^k, "
        "subtract to eliminate the repeating part, yielding a ratio of integers. "
        f"Tested on {len(direction_2_cases)} periodic decimals."
    )
    FACT_REGISTRY["A2"]["result"] = f"All {len(direction_2_cases)} cases converted to correct fractions and round-tripped"

    FACT_REGISTRY["A3"]["method"] = (
        "Exhaustive test of all p/q with 1 ≤ q ≤ 200, 0 ≤ p < q: "
        "long_division → periodic_decimal_to_fraction must return original Fraction(p,q). "
        "Uses Python's Fraction for exact arithmetic as independent ground truth."
    )
    FACT_REGISTRY["A3"]["result"] = f"{tested} rationals tested, {failures} failures"

    # --- JSON summary ---
    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,
        "cross_checks": [
            {
                "description": "Exhaustive round-trip test for all rationals p/q with q ≤ 200",
                "values_compared": [f"{tested} tested", f"{failures} failures"],
                "agreement": failures == 0,
            },
            {
                "description": "Direction 1 hand-picked cases vs Direction 2 reconstruction",
                "values_compared": [str(A1_result), str(A2_result)],
                "agreement": A1_result and A2_result,
            },
        ],
        "adversarial_checks": adversarial_checks,
        "verdict": verdict,
        "key_results": {
            "direction_1_passed": A1_result,
            "direction_2_passed": A2_result,
            "crosscheck_passed": A3_result,
            "total_rationals_exhaustively_tested": tested,
            "exhaustive_failures": failures,
            "claim_holds": claim_holds,
        },
        "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))