structure Hex.Conway.Rebuild.Entry : Type

One committed table row: the prime, the degree, and the Conway polynomial's coefficients stored ascending by degree.

• p : Nat

  The characteristic.

• n : Nat

  The extension degree.

• coeffs : List Nat

  Coefficients of C(p, n), ascending by degree, so the last entry is the leading 1.

@[instance_reducible]

instance Hex.Conway.Rebuild.instInhabitedEntry : Inhabited Entry

Equations

• Hex.Conway.Rebuild.instInhabitedEntry = { default := Hex.Conway.Rebuild.instInhabitedEntry.default }

def Hex.Conway.Rebuild.readCache (path : System.FilePath) : IO (Array Entry)

Read the committed Lübeck cache and return its entries in file order.

Fails with a readable message rather than an exception when the file is absent or does not have the expansion input’s JSON shape, since the usual cause is running the command from outside the package root.

Equations

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

def Hex.Conway.Rebuild.selectScope (entries : Array Entry) (scope : List (Nat × Nat)) : Array Entry

Keep the entries inside the requested scope, ordered by prime then degree so the generated match reads in the same order as Lübeck's table.

The scope gives a maximum degree per prime rather than one maximum for all of them. The complete offline generator instead accepts an exact pair list. The proof cost of an entry grows with both the prime and the degree, so a uniform bound would either stop the small primes short of what the budget affords or push the large ones past it.

Equations

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

def Hex.Conway.Rebuild.renderInvocation (scope : List (Nat × Nat)) (path : String) : String

Render the scope back as the command that produced it, for the commented-out line the replacement carries.

Equations

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

def Hex.Conway.Rebuild.renderTable (entries : Array Entry) (invocation : String) : String

Render the regenerated coefficient table, including the commented-out invocation above it.

def Hex.Conway.Rebuild.scopeEntry : Lean.ParserDescr

One scope entry, written p:maxDegree.

Equations

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

def Hex.Conway.Rebuild.rebuildLuebeck : Lean.ParserDescr

Scope specification: a maximum degree per prime, written scope [2:8, 3:6]. Degrees below the maximum that Lübeck's table happens not to list are simply absent, so a gap in the source is tolerated rather than fatal.

Equations

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

def Hex.Conway.Rebuild.elabRebuild : Lean.Elab.Command.CommandElab

Equations

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