structure Hex.Nat.Squfof.Limits : Type

• multipliers : Nat
• steps : Nat
• queueCapacity : Nat

def Hex.Nat.Squfof.instReprLimits.repr : Limits → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Nat.Squfof.instReprLimits : Repr Limits

Equations

• Hex.Nat.Squfof.instReprLimits = { reprPrec := Hex.Nat.Squfof.instReprLimits.repr }

@[instance_reducible]

instance Hex.Nat.Squfof.instDecidableEqLimits : DecidableEq Limits

Equations

• Hex.Nat.Squfof.instDecidableEqLimits = Hex.Nat.Squfof.instDecidableEqLimits.decEq

def Hex.Nat.Squfof.instDecidableEqLimits.decEq (x✝ x✝¹ : Limits) : Decidable (x✝ = x✝¹)

Equations

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

inductive Hex.Nat.Squfof.Policy : Type

Explicit placement of bounded SQUFOF work in a factorization portfolio. first runs before rho; rescue runs after the producer's existing splitters fail. Both retain the caller's limits at each composite worklist entry.

• off : Policy
• first (limits : Limits) : Policy
• rescue (limits : Limits) : Policy

@[instance_reducible]

instance Hex.Nat.Squfof.instReprPolicy : Repr Policy

Equations

• Hex.Nat.Squfof.instReprPolicy = { reprPrec := Hex.Nat.Squfof.instReprPolicy.repr }

def Hex.Nat.Squfof.instReprPolicy.repr : Policy → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hex.Nat.Squfof.instReprPolicy.repr Hex.Nat.Squfof.Policy.off prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.Nat.Squfof.Policy.off")).group prec✝

@[instance_reducible]

instance Hex.Nat.Squfof.instDecidableEqPolicy : DecidableEq Policy

Equations

• Hex.Nat.Squfof.instDecidableEqPolicy = Hex.Nat.Squfof.instDecidableEqPolicy.decEq

def Hex.Nat.Squfof.instDecidableEqPolicy.decEq (x✝ x✝¹ : Policy) : Decidable (x✝ = x✝¹)

Equations

• Hex.Nat.Squfof.instDecidableEqPolicy.decEq Hex.Nat.Squfof.Policy.off Hex.Nat.Squfof.Policy.off = isTrue ⋯
• Hex.Nat.Squfof.instDecidableEqPolicy.decEq Hex.Nat.Squfof.Policy.off (Hex.Nat.Squfof.Policy.first limits) = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqPolicy.decEq Hex.Nat.Squfof.Policy.off (Hex.Nat.Squfof.Policy.rescue limits) = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqPolicy.decEq (Hex.Nat.Squfof.Policy.first limits) Hex.Nat.Squfof.Policy.off = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqPolicy.decEq (Hex.Nat.Squfof.Policy.first a) (Hex.Nat.Squfof.Policy.first b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqPolicy.decEq (Hex.Nat.Squfof.Policy.first limits) (Hex.Nat.Squfof.Policy.rescue limits_1) = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqPolicy.decEq (Hex.Nat.Squfof.Policy.rescue limits) Hex.Nat.Squfof.Policy.off = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqPolicy.decEq (Hex.Nat.Squfof.Policy.rescue limits) (Hex.Nat.Squfof.Policy.first limits_1) = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqPolicy.decEq (Hex.Nat.Squfof.Policy.rescue a) (Hex.Nat.Squfof.Policy.rescue b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Hex.Nat.Squfof.Policy.attemptCap : Policy → Nat

Maximum multiplier attempts authorized at one worklist entry.

Equations

• Hex.Nat.Squfof.Policy.off.attemptCap = 0
• (Hex.Nat.Squfof.Policy.first a).attemptCap = if a.steps = 0 then 0 else min a.multipliers 16
• (Hex.Nat.Squfof.Policy.rescue a).attemptCap = if a.steps = 0 then 0 else min a.multipliers 16

inductive Hex.Nat.Squfof.Outcome : Type

• factor (divisor : Nat) : Outcome
• noFactor : Outcome
• exhausted : Outcome
• unsupported : Outcome

def Hex.Nat.Squfof.instReprOutcome.repr : Outcome → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Nat.Squfof.instReprOutcome : Repr Outcome

Equations

• Hex.Nat.Squfof.instReprOutcome = { reprPrec := Hex.Nat.Squfof.instReprOutcome.repr }

@[instance_reducible]

instance Hex.Nat.Squfof.instDecidableEqOutcome : DecidableEq Outcome

Equations

• Hex.Nat.Squfof.instDecidableEqOutcome = Hex.Nat.Squfof.instDecidableEqOutcome.decEq

def Hex.Nat.Squfof.instDecidableEqOutcome.decEq (x✝ x✝¹ : Outcome) : Decidable (x✝ = x✝¹)

Equations

• Hex.Nat.Squfof.instDecidableEqOutcome.decEq (Hex.Nat.Squfof.Outcome.factor a) (Hex.Nat.Squfof.Outcome.factor b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq (Hex.Nat.Squfof.Outcome.factor divisor) Hex.Nat.Squfof.Outcome.noFactor = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq (Hex.Nat.Squfof.Outcome.factor divisor) Hex.Nat.Squfof.Outcome.exhausted = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq (Hex.Nat.Squfof.Outcome.factor divisor) Hex.Nat.Squfof.Outcome.unsupported = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.noFactor (Hex.Nat.Squfof.Outcome.factor divisor) = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.noFactor Hex.Nat.Squfof.Outcome.noFactor = isTrue ⋯
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.noFactor Hex.Nat.Squfof.Outcome.exhausted = isFalse Hex.Nat.Squfof.instDecidableEqOutcome.decEq._proof_7✝
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.noFactor Hex.Nat.Squfof.Outcome.unsupported = isFalse Hex.Nat.Squfof.instDecidableEqOutcome.decEq._proof_8✝
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.exhausted (Hex.Nat.Squfof.Outcome.factor divisor) = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.exhausted Hex.Nat.Squfof.Outcome.noFactor = isFalse Hex.Nat.Squfof.instDecidableEqOutcome.decEq._proof_10✝
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.exhausted Hex.Nat.Squfof.Outcome.exhausted = isTrue ⋯
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.exhausted Hex.Nat.Squfof.Outcome.unsupported = isFalse Hex.Nat.Squfof.instDecidableEqOutcome.decEq._proof_11✝
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.unsupported (Hex.Nat.Squfof.Outcome.factor divisor) = isFalse ⋯
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.unsupported Hex.Nat.Squfof.Outcome.noFactor = isFalse Hex.Nat.Squfof.instDecidableEqOutcome.decEq._proof_13✝
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.unsupported Hex.Nat.Squfof.Outcome.exhausted = isFalse Hex.Nat.Squfof.instDecidableEqOutcome.decEq._proof_14✝
• Hex.Nat.Squfof.instDecidableEqOutcome.decEq Hex.Nat.Squfof.Outcome.unsupported Hex.Nat.Squfof.Outcome.unsupported = isTrue ⋯

structure Hex.Nat.Squfof.Result : Type

• outcome : Outcome
• attempts : Nat
• steps : Nat
• peakQueue : Nat

def Hex.Nat.Squfof.instReprResult.repr : Result → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Nat.Squfof.instReprResult : Repr Result

Equations

• Hex.Nat.Squfof.instReprResult = { reprPrec := Hex.Nat.Squfof.instReprResult.repr }

def Hex.Nat.Squfof.instDecidableEqResult.decEq (x✝ x✝¹ : Result) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.Nat.Squfof.instDecidableEqResult : DecidableEq Result

Equations

• Hex.Nat.Squfof.instDecidableEqResult = Hex.Nat.Squfof.instDecidableEqResult.decEq

def Hex.Nat.Squfof.multipliers : List Nat

The prescribed multiplier order.

Equations

• Hex.Nat.Squfof.multipliers = [1, 3, 5, 7, 11, 15, 21, 33, 35, 55, 77, 105, 165, 231, 385, 1155]

structure Hex.Nat.Squfof.Form : Type

• qprev : Nat
• p : Nat
• q : Nat

def Hex.Nat.Squfof.instReprForm.repr : Form → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Nat.Squfof.instReprForm : Repr Form

Equations

• Hex.Nat.Squfof.instReprForm = { reprPrec := Hex.Nat.Squfof.instReprForm.repr }

@[instance_reducible]

instance Hex.Nat.Squfof.instDecidableEqForm : DecidableEq Form

Equations

• Hex.Nat.Squfof.instDecidableEqForm = Hex.Nat.Squfof.instDecidableEqForm.decEq

def Hex.Nat.Squfof.instDecidableEqForm.decEq (x✝ x✝¹ : Form) : Decidable (x✝ = x✝¹)

Equations

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

@[reducible, inline]

abbrev Hex.Nat.Squfof.Pair : Type

Equations

• Hex.Nat.Squfof.Pair = (Nat × Nat)

inductive Hex.Nat.Squfof.Stop : Type

• factor : Stop
• repeated : Stop
• exhausted : Stop
• queueFull : Stop
• arithmetic : Stop
• skipped : Stop

@[instance_reducible]

instance Hex.Nat.Squfof.instReprStop : Repr Stop

Equations

• Hex.Nat.Squfof.instReprStop = { reprPrec := Hex.Nat.Squfof.instReprStop.repr }

def Hex.Nat.Squfof.instReprStop.repr : Stop → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hex.Nat.Squfof.instReprStop.repr Hex.Nat.Squfof.Stop.factor prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.Nat.Squfof.Stop.factor")).group prec✝

@[instance_reducible]

instance Hex.Nat.Squfof.instDecidableEqStop : DecidableEq Stop

Equations

• Hex.Nat.Squfof.instDecidableEqStop x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Hex.Nat.Squfof.Attempt (n : Nat) : Type

• divisor : Option { d : Nat // 1 < d ∧ d < n ∧ d ∣ n }
• stop : Stop
• steps : Nat
• peakQueue : Nat
• forwardSteps : Nat
• reverseSteps : Nat
• remaining : Nat

@[instance_reducible]

instance Hex.Nat.Squfof.instReprAttempt {n✝ : Nat} : Repr (Attempt n✝)

Equations

• Hex.Nat.Squfof.instReprAttempt = { reprPrec := Hex.Nat.Squfof.instReprAttempt.repr }

def Hex.Nat.Squfof.instReprAttempt.repr {n✝ : Nat} : Attempt n✝ → Nat → Std.Format

Equations

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

def Hex.Nat.Squfof.instDecidableEqAttempt.decEq {n✝ : Nat} (x✝ x✝¹ : Attempt n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.Nat.Squfof.instDecidableEqAttempt {n✝ : Nat} : DecidableEq (Attempt n✝)

Equations

• Hex.Nat.Squfof.instDecidableEqAttempt = Hex.Nat.Squfof.instDecidableEqAttempt.decEq

def Hex.Nat.Squfof.nextForm (f : Form) (b : Nat) (pnext : Int) : Option Form

One exact continued-fraction transition, given its quotient and next P.

Equations

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

def Hex.Nat.Squfof.reverseForm (D S : Nat) (f : Form) (r : Nat) : Option Form

Reverse initialization from a square form.

Equations

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

def Hex.Nat.Squfof.afterMatch (queue : List Pair) (r p : Nat) : Option (List Pair)

The first matching queued form removes itself and the whole FIFO prefix.

Equations

• Hex.Nat.Squfof.afterMatch [] r p = none
• Hex.Nat.Squfof.afterMatch ((g, t) :: rest) r p = if g = r ∧ t = p % r then some rest else Hex.Nat.Squfof.afterMatch rest r p

def Hex.Nat.Squfof.runMultiplier (n k : Nat) (limits : Limits) : Attempt n

Run one multiplier with the same kernel used by the public schedule.

Equations

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

def Hex.Nat.Squfof.factor (n : Nat) (limits : Limits := { }) : Result

Equations

• Hex.Nat.Squfof.factor n limits = Hex.Nat.Squfof.CheckedResult.public✝ (Hex.Nat.Squfof.factorCore✝ n limits)

theorem Hex.Nat.Squfof.factor_attempts (n : Nat) (limits : Limits) : (factor n limits).attempts ≤ min limits.multipliers 16

theorem Hex.Nat.Squfof.factor_steps (n : Nat) (limits : Limits) : (factor n limits).steps ≤ (factor n limits).attempts * limits.steps

theorem Hex.Nat.Squfof.factor_queue (n : Nat) (limits : Limits) : (factor n limits).peakQueue ≤ limits.queueCapacity

theorem Hex.Nat.Squfof.factor_spec {n : Nat} {limits : Limits} {d : Nat} (h : (factor n limits).outcome = Outcome.factor d) : 1 < d ∧ d < n ∧ d ∣ n