eulerChar1D_filledBox
plain-language theorem explainer
A filled 1-D lattice segment with a+1 vertices and a unit edges has Euler characteristic N0-N1=1, independent of length. Cosmology and foam-topology readers cite it as the 1-D contractible normalization: a solid interval is topologically a point. The proof is a one-line ring cancellation on integers.
Claim. For every integer $a$, $(a+1)-a=1$. Interpreting $N_0=a+1$ lattice points and $N_1=a$ unit edges on a filled segment, the 1-D Euler characteristic satisfies $N_0-N_1=1$, independent of the segment length.
background
Phase 18 of the Recognition cosmology stack reads out the cubical Euler characteristic of the assembled recognition foam: $\chi=N_0-N_1+N_2-N_3$ (occupied vertices, unit edges, unit squares, unit cubes). Two structural facts make the numeric readout scale-free. The first is contractible normalization: a filled $d$-box has $\chi=1$ no matter how large its side lengths are, so deviations from 1 measure genuine topology (extra components, tunnels, voids), never mere size.
This declaration is the 1-D case of that normalization. A filled segment of $a+1$ lattice points carries $a$ unit edges; the alternating sum collapses to $(a+1)-a$. Sibling identities handle the filled rectangle ($N_0-N_1+N_2=1$) and the filled 3-box. Inclusion-exclusion ($\chi(A\cup B)+\chi(A\cap B)=\chi(A)+\chi(B)$) then lets the readout sum over locked domains assembled by the birth law.
proof idea
Pure integer arithmetic. The goal $(a+1)-a=1$ is discharged by the ring tactic: expand and cancel. No combinatorial lemmas, no cell-counting definitions, and no appeal to higher-dimensional Euler identities are required. The geometric reading (vertices minus edges on a path graph) sits entirely in the doc-comment; the formal statement is the identity alone.
why it matters
It anchors §1 of the foam-topology module: size-independent $\chi=1$ for a solid region is the signature that the cosmic-web-style genus statistic is topological rather than metric. Together with the 2-D and 3-D filled-box theorems and the inclusion-exclusion valuation, it justifies reading $k$ disjoint solid domains as $\chi=k$ and a single contractible domain as $\chi=1$. Downstream classical numerics (polar law vs Thue-Morse foam, freeze-out curves) rely on this baseline; the Lean graph currently lists no formal used_by edges, so the declaration is a leaf normalization lemma inside the proved (0-sorry) Phase-18 stack. Framework context: D=3 spatial dimensions and the eight-tick octave fix the ambient cubical complex on which this 1-D identity is the simplest face.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.