Coordinated numerical refinement

This module contains the untrusted scheduling policy shared by tactic-side candidate search. A stage coordinates three independent sources of enclosure error: Dyadic rounding, Taylor approximation, and spatial subdivision.

The schedule never proves a theorem. A selected stage must still close the ordinary Boolean checker and apply its existing Golden Theorem.

structure LeanCert.Tactic.NumericalRefinementStage : Type

One finite numerical-refinement attempt. index is zero-based.

• index : Nat
• dyadicPrecision : Int
• taylorDepth : Nat
• subdivisionDepth : Nat

def LeanCert.Tactic.instDecidableEqNumericalRefinementStage.decEq (x✝ x✝¹ : NumericalRefinementStage) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.instDecidableEqNumericalRefinementStage : DecidableEq NumericalRefinementStage

Equations

• LeanCert.Tactic.instDecidableEqNumericalRefinementStage = LeanCert.Tactic.instDecidableEqNumericalRefinementStage.decEq

@[instance_reducible]

instance LeanCert.Tactic.instReprNumericalRefinementStage : Repr NumericalRefinementStage

Equations

• LeanCert.Tactic.instReprNumericalRefinementStage = { reprPrec := LeanCert.Tactic.instReprNumericalRefinementStage.repr }

def LeanCert.Tactic.instReprNumericalRefinementStage.repr : NumericalRefinementStage → Nat → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.instInhabitedNumericalRefinementStage : Inhabited NumericalRefinementStage

Equations

• LeanCert.Tactic.instInhabitedNumericalRefinementStage = { default := LeanCert.Tactic.instInhabitedNumericalRefinementStage.default }

structure LeanCert.Tactic.NumericalRefinementPolicy : Type

Deterministic policy for coordinated candidate refinement.

• initialDyadicPrecision : Int
• dyadicPrecisionStep : Nat
• initialTaylorDepth : Nat
• taylorDepthStep : Nat
• maxSubdivisionDepth : Nat
• stageCount : Nat

def LeanCert.Tactic.instDecidableEqNumericalRefinementPolicy.decEq (x✝ x✝¹ : NumericalRefinementPolicy) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.instDecidableEqNumericalRefinementPolicy : DecidableEq NumericalRefinementPolicy

Equations

• LeanCert.Tactic.instDecidableEqNumericalRefinementPolicy = LeanCert.Tactic.instDecidableEqNumericalRefinementPolicy.decEq

@[instance_reducible]

instance LeanCert.Tactic.instReprNumericalRefinementPolicy : Repr NumericalRefinementPolicy

Equations

• LeanCert.Tactic.instReprNumericalRefinementPolicy = { reprPrec := LeanCert.Tactic.instReprNumericalRefinementPolicy.repr }

def LeanCert.Tactic.instReprNumericalRefinementPolicy.repr : NumericalRefinementPolicy → Nat → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Tactic.instInhabitedNumericalRefinementPolicy : Inhabited NumericalRefinementPolicy

Equations

• LeanCert.Tactic.instInhabitedNumericalRefinementPolicy = { default := LeanCert.Tactic.instInhabitedNumericalRefinementPolicy.default }

def LeanCert.Tactic.NumericalRefinementPolicy.subdivisionDepthAt (policy : NumericalRefinementPolicy) (index : Nat) : Nat

Spatial depth at a stage, linearly ramped from zero to the configured maximum. A singleton schedule receives the full configured depth.

Equations

• policy.subdivisionDepthAt index = if policy.stageCount ≤ 1 then policy.maxSubdivisionDepth else policy.maxSubdivisionDepth * index / (policy.stageCount - 1)

def LeanCert.Tactic.NumericalRefinementPolicy.stageAt (policy : NumericalRefinementPolicy) (index : Nat) : NumericalRefinementStage

Materialize one stage of the policy.

Equations

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

def LeanCert.Tactic.NumericalRefinementPolicy.stages (policy : NumericalRefinementPolicy) : List NumericalRefinementStage

All configured stages in increasing refinement order.

Equations

• policy.stages = List.map policy.stageAt (List.range policy.stageCount)

def LeanCert.Tactic.NumericalRefinementPolicy.adaptive (initialTaylorDepth maxSubdivisionDepth : Nat) : NumericalRefinementPolicy

Default three-stage policy used by the semantic tactic router.

Equations

• LeanCert.Tactic.NumericalRefinementPolicy.adaptive initialTaylorDepth maxSubdivisionDepth = { initialTaylorDepth := initialTaylorDepth, maxSubdivisionDepth := maxSubdivisionDepth }

def LeanCert.Tactic.NumericalRefinementPolicy.fixedTaylor (taylorDepth maxSubdivisionDepth : Nat) : NumericalRefinementPolicy

Refine Dyadic rounding and spatial depth while holding a user-specified Taylor depth fixed.

Equations

• LeanCert.Tactic.NumericalRefinementPolicy.fixedTaylor taylorDepth maxSubdivisionDepth = { initialTaylorDepth := taylorDepth, taylorDepthStep := 0, maxSubdivisionDepth := maxSubdivisionDepth }