U
plain-language theorem explainer
The structure U supplies the carrier type for atomic units in the Recognition module, consisting of a single field of type Unit to support structural equality as the recognition relation. Constructions of chains, atomic ticks, and aesthetic certificates cite it when building RecognitionStructure instances. The definition is a direct structural wrapper with no lemmas or computational reduction.
Claim. Let $U$ be the structure with a single field $a : 1$, where $1$ denotes the unit type.
background
The Recognition module opens with T1 (MP): Nothing cannot recognize itself. U acts as the type of events or units inside RecognitionStructure, on which the relation R is defined by structural equality. It imports the RS-native gauge from Constants.RSNativeUnits.U, whose doc-comment states: RS-native gauge: τ₀ = 1 tick, ℓ₀ = 1 voxel, c = 1.
proof idea
Direct structure definition. No lemmas or tactics are invoked; the declaration simply introduces the field a : Unit to enable equality-based recognition.
why it matters
U supplies the unit type required by Chain, AtomicTick, head, last, and Ledger in the same module, and is used downstream by BerlyneInvertedUCert and aestheticCost_zero_at_optimum. It anchors the T1 axiom and feeds the J-cost symmetry that produces the Berlyne inverted-U. The declaration closes the basic carrier for the eight-tick octave and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.