Py.Cafe

"""Streamlit app for py.cafe: the block structure of reversed odd Collatz trajectories.

Port of `Test seq.ipynb`. Reverse the odd terms of a Collatz trajectory, read each
term's second binary digit, and split the digit stream (after the first term whose
binary starts `100`) into the blocks `10 01010` and `01010`.
"""

from dataclasses import dataclass

import streamlit as st

PATTERNS = ("1001010", "01010")


@dataclass(frozen=True)
class Block:
    """One block of the digit stream: its digits and the trajectory terms carrying them."""

    digits: str
    terms: tuple[int, ...]

    @property
    def pattern(self) -> str:
        """The pattern this block is checked against, chosen by its first digit."""
        return PATTERNS[0] if self.digits[0] == "1" else PATTERNS[1]

    @property
    def ok(self) -> bool:
        """Whether the block agrees with its pattern (a truncated last block may be a prefix)."""
        return self.pattern.startswith(self.digits)

    @property
    def wrong(self) -> tuple[bool, ...]:
        """Per digit: whether it differs from the pattern."""
        return tuple(d != p for d, p in zip(self.digits, self.pattern))


@dataclass(frozen=True)
class Decomposition:
    """The reversed trajectory from 1 up to the anchor, and the blocks that follow it."""

    start: tuple[int, ...]
    blocks: tuple[Block, ...]

    @property
    def anchor(self) -> int:
        """The first term whose binary starts with `100`."""
        return self.start[-1]

    @property
    def first_failure(self) -> Block | None:
        """The first block that breaks the pattern, if any."""
        return next((b for b in self.blocks if not b.ok), None)


def odd_trajectory(n: int) -> list[int]:
    """Odd terms of the Collatz trajectory of n, excluding the final 1."""
    if n < 1:
        raise ValueError(f"expected a positive integer, got {n}")
    result = []
    while True:
        while n % 2 == 0:
            n //= 2
        if n == 1:
            return result
        result.append(n)
        n = 3 * n + 1


def second_digit(x: int) -> str:
    """The binary digit just below the leading 1."""
    return bin(x)[3]


def decompose(n: int) -> Decomposition | None:
    """Split the reversed odd trajectory of n into blocks; None if no term starts with `100`."""
    seq = odd_trajectory(n)[::-1]
    anchor = next((i for i, x in enumerate(seq) if bin(x)[2:5] == "100"), None)
    if anchor is None:
        return None
    blocks = []
    i = anchor + 1
    while i < len(seq):
        length = len(PATTERNS[0] if second_digit(seq[i]) == "1" else PATTERNS[1])
        terms = tuple(seq[i : i + length])
        blocks.append(Block("".join(map(second_digit, terms)), terms))
        i += length
    return Decomposition((1, *seq[: anchor + 1]), tuple(blocks))


@st.cache_data(show_spinner=False)
def verify(n_max: int) -> tuple[int, int, int | None]:
    """Check every odd start below n_max: (checked, without anchor, first counterexample)."""
    checked = no_anchor = 0
    for n in range(1, n_max, 2):
        d = decompose(n)
        checked += 1
        if d is None:
            no_anchor += 1
        elif d.first_failure is not None:
            return checked, no_anchor, n
    return checked, no_anchor, None


def digits_html(b: Block) -> str:
    """A block's digits, the `10` head split off so `01010` parts align, wrong digits in red."""
    pieces = [f'<span class="bad">{d}</span>' if w else d for d, w in zip(b.digits, b.wrong)]
    if b.digits[0] == "1":
        return f"{''.join(pieces[:2])} {''.join(pieces[2:])}"
    return "   " + "".join(pieces)


def binary_marked(x: int) -> str:
    """Binary of x as Markdown with the second digit in bold."""
    b = bin(x)[2:]
    return f"`{b[0]}`**`{b[1]}`**`{b[2:]}`"


TABLE_CSS = """<style>
.blocks {border-collapse: collapse; width: 100%; margin-bottom: 1rem;}
.blocks th {text-align: left; font-weight: 600; opacity: .7; padding: .3rem .6rem;
  border-bottom: 1px solid rgba(128,128,128,.45);}
.blocks td {padding: .35rem .6rem; border-bottom: 1px solid rgba(128,128,128,.2);
  vertical-align: top;}
.blocks .narrow {width: 1%; white-space: nowrap;}
.blocks .digits {font-family: ui-monospace, SFMono-Regular, Menlo, Consolas, monospace;
  white-space: pre; font-size: 1.05rem;}
.blocks .term {display: inline-block; font-family: ui-monospace, Menlo, Consolas, monospace;
  font-size: .85rem; padding: .05rem .45rem; margin: .12rem .3rem .12rem 0;
  border-radius: .4rem; background: rgba(128,128,128,.14);
  border: 1px solid rgba(128,128,128,.3); position: relative;}
.blocks .term .bin {display: none; position: absolute; bottom: 125%; left: 50%;
  transform: translateX(-50%); z-index: 10; white-space: nowrap; padding: .15rem .5rem;
  border-radius: .35rem; background: #262730; color: #fafafa; font-size: .8rem;
  box-shadow: 0 2px 6px rgba(0,0,0,.3);}
.blocks .term:hover .bin {display: block;}
.blocks .bin b {background: #ffbd45; color: #262730; padding: 0 .12rem;
  margin: 0 .05rem; border-radius: .2rem;}
.blocks .anchorbin {margin-left: .4rem; opacity: .75;}
.blocks .anchorbin u {text-decoration-color: #ffbd45; text-decoration-thickness: 2px;
  text-underline-offset: 3px;}
.blocks .digits .bad {color: #ff4b4b; font-weight: 700;}
.blocks .term.bad {background: rgba(255,75,75,.18); border-color: #ff4b4b; font-weight: 600;}
</style>"""


def binary_html(x: int) -> str:
    """Binary of x as HTML with the second digit in bold."""
    b = bin(x)[2:]
    if len(b) == 1:  # 1 has no second digit
        return b
    return f"{b[0]}<b>{b[1]}</b>{b[2:]}"


def term_chip(x: int, bad: bool = False) -> str:
    """One term as a chip, its binary shown on hover."""
    return f'<span class="term{" bad" if bad else ""}">{x}<span class="bin">{binary_html(x)}</span></span>'


def anchor_chip(x: int) -> str:
    """The anchor term as a chip with its binary inline, the leading `100` underlined."""
    b = bin(x)[2:]
    return f'<span class="term">{x}<span class="anchorbin"><u>{b[:3]}</u>{b[3:]}</span></span>'


def table_html(d: Decomposition) -> str:
    """The trajectory as an HTML table: the start up to the anchor, then one row per block."""
    start = "".join(map(term_chip, d.start[:-1])) + anchor_chip(d.anchor)
    rows = [f'<tr><td class="narrow"></td><td>{start}</td></tr>']
    for b in d.blocks:
        terms = "".join(term_chip(x, w) for x, w in zip(b.terms, b.wrong))
        rows.append(f'<tr><td class="digits narrow">{digits_html(b)}</td><td>{terms}</td></tr>')
    head = '<tr><th class="narrow">Block</th><th>Terms (reversed trajectory)</th></tr>'
    return f'<table class="blocks">{head}{"".join(rows)}</table>'


st.set_page_config(page_title="Collatz blocks", page_icon="🔁", layout="wide")
st.title("Collatz blocks")
st.markdown(
    "Take the **odd** terms of the Collatz trajectory of *n*, read them **backwards** "
    "from 1, and note each term's **second binary digit**. After the first term whose "
    "binary starts with `100`, the digit stream seems to split into just two blocks:"
)
st.code("10 01010\n   01010", language=None)

tab_explore, tab_verify = st.tabs(["Explore one number", "Verify a range"])

with tab_explore:
    n = int(st.number_input("Starting number n", min_value=1, value=837799, step=2))
    d = decompose(n)
    if d is None:
        st.info(f"No term of the trajectory of {n} starts with `100` in binary.")
    else:
        failure = d.first_failure
        m1, m2, m3 = st.columns(3)
        m1.metric("Odd terms", len(odd_trajectory(n)))
        m2.metric("Blocks", len(d.blocks))
        m3.metric("Pattern", "holds ✅" if failure is None else "breaks ❌")
        st.markdown(TABLE_CSS + table_html(d), unsafe_allow_html=True)
        if failure is not None:
            st.error(f"Block `{failure.digits}` does not match `{failure.pattern}`.")
        with st.expander("Binary view"):
            st.markdown(
                "\n".join(
                    f"- {x}: {binary_marked(x)}" for b in d.blocks for x in b.terms
                )
            )

with tab_verify:
    n_max = int(
        st.number_input(
            "Check all odd n below", min_value=3, max_value=1_000_000, value=100_000
        )
    )
    if st.button("Run check", type="primary"):
        with st.spinner(f"Checking odd n < {n_max:,} …"):
            checked, no_anchor, counterexample = verify(n_max)
        if counterexample is None:
            st.success(
                f"The pattern holds for all {checked:,} odd starting numbers "
                f"({no_anchor:,} have no `100` term)."
            )
        else:
            st.error(f"Counterexample: n = {counterexample}. See it in the first tab.")