structure HexMatrixTheory.Det.Configextends HexMatrixTheory.KernelConfig : Type

Limits for determinant proof production. The symbolic heartbeat limit is in Lean's public units (one unit is 1,000 internal heartbeats); relation work counts distinct indexed sum tails. Neither symbolic limit affects numeric certificates. Packing applies only to the numeric certificate backend.

• packing : Bool
• maxHeartbeats : ℕ
• maxRelationWork : ℕ

def HexMatrixTheory.Det.elabConfig (cfg : Lean.Syntax) (init : Config := { }) (logExceptions : Bool := true) : Lean.Elab.Tactic.TacticM Config

Equations

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

@[instance_reducible]

instance HexMatrixTheory.Det.instToExprDetWitness_hexBareissTheory {R✝ : Type} [Lean.ToExpr R✝] : Lean.ToExpr (Hex.Matrix.DetWitness R✝)

Equations

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

def HexMatrixTheory.Det.instToExprDetWitness_hexBareissTheory.toExpr {R✝ : Type} [Lean.ToExpr R✝] : Hex.Matrix.DetWitness R✝ → Lean.Expr

Equations

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

inductive HexMatrixTheory.Det.Outcome (α : Type) : Type

The outcome of an attempt, per the matrix-tactic protocol; a failure throws.

• notApplicable {α : Type} (msg : Lean.MessageData) : Outcome α

  The goal or input is not in the fragment; the next handler may try.

• declined {α : Type} (msg : Lean.MessageData) : Outcome α

  In the fragment, but a capability is missing; the message names it.

• success {α : Type} (a : α) : Outcome α

  A value and a proof.

structure HexMatrixTheory.Det.Result : Type

The common result of computing a determinant independently of a target.

• value : Lean.Expr
• proof : Lean.Expr

def HexMatrixTheory.Det.detTarget? (target : Lean.Expr) : Option (Lean.Expr × Lean.Expr × Bool)

Recognize a determinant target: the matrix, the other side, and whether the determinant is on the right.

Equations

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

structure HexMatrixTheory.Det.Cert : Type

The certificate of a square literal: the witness, the row list of the integer matrix it certifies, and for a rational literal the rational row list and the row scales.

• lit : Literal.Recognized

  The recognized literal.

• witness : Hex.Matrix.DetWitness

  The witness of the integer matrix.

• rows : Array (Array ℤ)

  The integer rows.

• rat : Option (Array (Array ℚ) × Array ℕ)

  The rational rows and the positive scale of each, for a rational literal.

def HexMatrixTheory.Det.Cert.value (c : Cert) : ℚ

The certified determinant as a rational.

Equations

• c.value = match c.rat with | none => ↑c.witness.value | some (fst, s) => ↑c.witness.value / ↑(Array.foldl (fun (x1 x2 : ℕ) => x1 * x2) 1 s)

def HexMatrixTheory.Det.recognize (A : Lean.Expr) : Lean.MetaM (Outcome Literal.Recognized)

Recognize the numeric matrix fragment without evaluating its entries.

Equations

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

def HexMatrixTheory.Det.classify (target : Lean.Expr) : Lean.MetaM (Outcome (Lean.Expr × Lean.Expr × Bool × Literal.Recognized))

Classify the target before evaluating entries or running the producer.

Equations

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

def HexMatrixTheory.Det.certifyLiteral (lit : Literal.Recognized) : Lean.MetaM (Outcome Cert)

Certify a square literal over Int or Rat, as returned by recognize. A producer whose witness fails its own check is a failure, not a decline.

Equations

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

def HexMatrixTheory.Det.certify (A : Lean.Expr) : Lean.MetaM (Outcome Cert)

Recognize a closed square integer or rational literal and certify it.

Equations

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

structure HexMatrixTheory.Det.Proof : Type

The proof of Matrix.det A = v for the certificate's value v, with the value, the kernel check it rests on, and the row list of the literal.

• value : Lean.Expr

  The certified value, as a numeral.

• proof : Lean.Expr

  The proof term of Matrix.det A = value.

• check : Lean.Expr

  The certificate check the kernel evaluates.

• rowList : Lean.Expr

  The row list the literal is identified with.

def HexMatrixTheory.Det.packedBounds (c : Cert) : ℕ × ℕ

The entry bound and slot width of the packed check: k one more than the largest absolute value among the integer rows and the transform, and W the least positive width with n · k² < 2^W.

Equations

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

def HexMatrixTheory.Det.build (cfg : KernelConfig) (A : Lean.Expr) (c : Cert) : Lean.MetaM Proof

Build the proof of Matrix.det A = v for the certificate's value v.

Equations

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

def HexMatrixTheory.Det.diagnose (A : Lean.Expr) (c : Cert) (p : Proof) (e : Lean.Exception) : Lean.MetaM Lean.Exception

Diagnose a proof the kernel rejected: evaluate the certificate check with the kernel and test the identification of the literal with its row list along its route, reporting the first that fails.

Equations

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

def HexMatrixTheory.Det.checked (A : Lean.Expr) (c : Cert) (p : Proof) (target proof : Lean.Expr) : Lean.MetaM Lean.Expr

Add proof : target as an auxiliary lemma checked synchronously, so that a rejection is reported here, not later, and diagnosed.

Equations

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

def HexMatrixTheory.Det.proveGoal (cfg : KernelConfig) (target : Lean.Expr) : Lean.MetaM (Outcome Lean.Expr)

Prove a determinant target in either orientation.

Equations

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

def HexMatrixTheory.Det.certifiedProof (A : Lean.Expr) (c : Cert) (cfg : Config := { }) : Lean.MetaM Proof

The proof of Matrix.det A = v for the certified value v, checked.

Equations

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

structure HexMatrixTheory.Det.SymbolicHandler : Type

The single extension point for symbolic determinant computation and supplied-target comparison. Its functions share the same public configuration; the companion installs one handler when imported.

• compute : Config → Lean.Expr → Lean.MetaM (Outcome Result)
• prove : Config → Lean.Expr → Lean.MetaM (Outcome Lean.Expr)

opaque HexMatrixTheory.Det.symbolicHandler : IO.Ref (Option SymbolicHandler)

def HexMatrixTheory.Det.compute (cfg : Config) (A : Lean.Expr) : Lean.MetaM (Outcome Result)

Compute a determinant independently of a proposed answer. Closed numeric matrices use their certificate backend; the companion handles other literals.

Equations

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

def HexMatrixTheory.Det.certified (A : Lean.Expr) (cfg : Config := { }) : Lean.MetaM (Outcome Lean.Expr)

The det% A record: Certified Matrix.det A.

Equations

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

def HexMatrixTheory.Det.detTerm : Lean.ParserDescr

det% A computes the determinant of a closed integer or rational matrix literal A and returns a HexMatrixTheory.Certified Matrix.det A record with its value and proof. The !![…] notations are given an integer entry expectation.

Equations

• HexMatrixTheory.Det.detTerm = Lean.ParserDescr.node `HexMatrixTheory.Det.detTerm 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "det%") (Lean.ParserDescr.cat `term 1024))

def HexMatrixTheory.Det.elabMatrixArgument (t : Lean.Syntax) (carrier? : Option Lean.Expr := none) : Lean.Elab.TermElabM Lean.Expr

Elaborate a matrix with integer defaulting, then let surrounding annotations or local entries determine its carrier when the default does not fit.

Equations

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

def HexMatrixTheory.Det.elabDetTerm : Lean.Elab.Term.TermElab

Equations

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

def HexMatrixTheory.Det.normDet? (e : Lean.Expr) : Lean.MetaM (Option Lean.Meta.Simp.Result)

Rewrite Matrix.det A to its certified value when the Hex frontend applies; none when it declines.

Equations

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

def Hex.norm_det : Lean.Meta.Simp.Simproc

The Hex.norm_det simproc rewrites the determinant of a closed integer or rational matrix literal to its value through the Hex certificate. Unsupported inputs are unchanged; a producer failure or kernel rejection is an error.

Equations

• Hex.norm_det e = do let __do_lift ← liftM (HexMatrixTheory.Det.normDet? e) match __do_lift with | some r => pure (Lean.Meta.Simp.Step.done r) | none => pure Lean.Meta.Simp.Step.continue

def HexMatrixTheory.Det.detTac : Lean.ParserDescr

det closes supported determinant equalities using a numeric certificate or the registered symbolic handler. The numeric-only import retains its certificate normalization diagnostic. Extensions use @[no_fallback] so a committed error is preserved. The keyword remains usable as an identifier.

Equations

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

def HexMatrixTheory.Det.detResultTac : Lean.ParserDescr

Introduce a computed determinant and its equality proof into the current goal. Both local names are required.

Equations

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

def HexMatrixTheory.Det.evalDetResultTac : Lean.Elab.Tactic.Tactic

Equations

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

def HexMatrixTheory.Det.simpCertificate (msg : Lean.MessageData) : Lean.Elab.Tactic.TacticM Unit

Normalize using only the Hex certificate, reporting the original reason when it makes no progress. Errors from the simproc propagate unchanged.

Equations

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

def HexMatrixTheory.Det.detDiagnostic : Lean.Elab.Tactic.Tactic

Registered before the numeric handler, so tried after it (Lean reverses registration order at equal priority). Try Hex certificate normalization for determinant equations, reporting the classification reason when it makes no progress. Classification itself produces no certificate.

Equations

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

def HexMatrixTheory.Det.evalDetTac : Lean.Elab.Tactic.Tactic

Equations

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