def Hex.NumberTower.Flattening.Sound {T : NumberTower} (F : T.Flattening) : Prop

Mathematical meaning of a checked primitive presentation.

Equations

• One or more equations did not get rendered due to their size.

def Hex.NumberTower.Flatten.Generator.Matches {T : NumberTower} (generator : Generator T) : Prop

A recovered runtime generator denotes its selected absolute value in the fixed tower embedding.

Equations

• generator.Matches = (T.toComplex generator.value = generator.root.toComplex)

def Hex.NumberTower.Flatten.Candidate.Matches {T : NumberTower} (candidate : Candidate T) : Prop

The accumulated tower element denotes the selected primitive value.

Equations

• candidate.Matches = (T.toComplex candidate.value = candidate.root.toComplex)

def Hex.NumberTower.Flatten.Candidate.Represents {T : NumberTower} (candidate : Candidate T) (generators : List (Generator T)) : Prop

Every accumulated generator coordinate denotes the corresponding absolute generator in the candidate presentation.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.NumberTower.flatten?_sound (T : NumberTower) {F : T.Flattening} (h : T.flatten? = some F) : F.Sound

Every returned primitive presentation has inverse coordinate maps, preserves arithmetic, and commutes with the fixed complex embeddings.

theorem Hex.NumberTower.flatten?_isSome (T : NumberTower) : T.flatten?.isSome = true

Exactification, primitive search, and coordinate recovery always produce a checked primitive presentation.

theorem Hex.NumberTower.flatten_toComplex (T : NumberTower) {F : T.Flattening} (h : T.flatten? = some F) (a : T.Elem) : PolyQuot.toComplex (F.toPrimitive a) F.root.rep ⋯ = T.toComplex a

The forward primitive coordinate map preserves the fixed complex value.

theorem Hex.NumberTower.flatten_fromComplex (T : NumberTower) {F : T.Flattening} (h : T.flatten? = some F) (a : PolyQuot F.root.p F.root.x) : T.toComplex (F.fromPrimitive a) = a.toComplex F.root.rep ⋯

The inverse primitive coordinate map preserves the fixed complex value.