twoStep
plain-language theorem explainer
twoStep instantiates the Chain structure over M as a single recognition step on the unit element. Researchers verifying basic flux identities in the Recognition module cite it as a minimal test case. The definition directly supplies the three fields of Chain with n set to 1 and the recognition condition holding by construction.
Claim. Let $M$ be the recognition structure with universe $U$ and relation recog. Define the chain with $n=1$, the map $f$ sending every element of Fin(2) to the unit, and the condition that recog holds between the two consecutive elements, satisfied by direct construction.
background
The module addresses T1 (MP): Nothing cannot recognize itself. Chain records a finite sequence of recognitions via n, a map from Fin(n+1) to U, and the requirement that the recognition relation R holds on each adjacent pair. M is the concrete structure using U and recog. L is the ledger with debit and credit both constantly 1. Upstream, chainFlux is defined as phi at the last element minus phi at the head, and chainFlux_zero_of_balanced states that any balanced ledger yields zero flux.
proof idea
The definition populates the Chain fields directly: n equals 1, f is the constant function returning the unit, and ok is proved by introducing the index and applying trivial. The attached example first establishes balance by reflexivity on every unit then invokes chainFlux_zero_of_balanced.
why it matters
It supplies the concrete chain instance used to demonstrate zero flux on balanced ledgers, directly supporting the MP statement T1. No further downstream theorems are recorded. It anchors the basic Recognition axioms before any appeal to J-uniqueness, the phi-ladder, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.