SimpleStructure
plain-language theorem explainer
SimpleStructure defines the minimal two-vertex recognition structure with universe the Boolean type and recognition holding exactly between distinct vertices. Modelers use it to test basic ledger balancing and tick scheduling before moving to continuous or phi-ladder models. The construction is a direct record literal with no proof steps or lemma applications.
Claim. Let $U = B$ (Boolean type) and $R(u,v) := u ≠ v$. The pair $(U, R)$ forms a RecognitionStructure.
background
RecognitionStructure is the record type with fields U : Type and R : U → U → Prop introduced in the Chain module as a minimal stub for recognition models. The ModelingExamples module builds concrete instances to demonstrate interaction with Ledger and AtomicTick. Upstream, the RSNativeUnits.U fixes the gauge with c = 1, while IntegrationGap.A sets the active edge count to 1 per fundamental tick. LedgerForcing.balanced requires event lists to be balanced, a property verified on this structure in sibling definitions. The local theoretical setting is a set of small finite examples that precede the full forcing chain from T0 to T8 and the Recognition Composition Law.
proof idea
The definition populates the RecognitionStructure record directly: the U field receives Bool and the R field receives the inequality function. No tactics or lemmas from upstream results are applied; the body is a pure structure constructor.
why it matters
This supplies the base instance for SimpleLedger and SimpleTicks, which verify conservation on closed chains and alternating schedules. It occupies the initial position in the Recognition forcing chain before phi-uniqueness (T5) and the eight-tick octave (T7) are imposed. The example allows concrete checks of the Recognition Composition Law on a two-vertex graph without invoking dimension D = 3 or the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.