pith. machine review for the scientific record. sign in
structure definition def or abbrev high

U

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  95structure U where
  96  a : Unit
  97
  98/-- Recognition relation by structural equality -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.