PacketBridge.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Full lattices in the existing packet model

The packet development records a chosen integer basis in its full-lattice structure. Our finite-generation definition produces that basis. This conversion preserves the actual submodule and multiplier order.

def OAI.DukePrimeDegree.FullLattice.toPacket line 20
Source documentation
Equip a full lattice with the basis expected by the packet model.
```
noncomputable def FullLattice.toPacket (M : FullLattice K)
    (hn : Module.finrank ℚ K = n) : PrimeDegreePackets.FullLattice n K where
…
```
Mentions: OAI.DukePrimeDegree.FullLattice, OAI.PrimeDegreePackets.FullLattice
lemma OAI.DukePrimeDegree.FullLattice.toPacket_carrier line 26
lemma OAI.DukePrimeDegree.FullLattice.toPacket_multiplierOrder line 29
def OAI.DukePrimeDegree.EmbeddingOrder.toRealOrder line 38
Source documentation
Convert the complex-embedding ordering to the real-embedding ordering used by the row-lattice packet model. Total reality makes this bijective.
```
noncomputable def EmbeddingOrder.toRealOrder [NumberField.IsTotallyReal K]
    (σ : EmbeddingOrder K n) : PrimeDegreePackets.OrderedEmbeddings n K :=
…
```
Mentions: OAI.DukePrimeDegree.EmbeddingOrder, OAI.PrimeDegreePackets.OrderedEmbeddings
lemma OAI.DukePrimeDegree.EmbeddingOrder.toRealOrder_apply line 57