theorem Hex.bhksIndicatorCandidates?_getD_candidate {f : ZPoly} {d : LiftData} {indicators : Array (Array Int)} {candidates : Array ZPoly} (h : bhksIndicatorCandidates? f d indicators = some candidates) (i : Nat) : i < indicators.size → ∃ (quotient : ZPoly), bhksIndicatorCandidate? f d (indicators.getD i #[]) = some (candidates.getD i 0, quotient)

Per-index extraction from a successful bhksIndicatorCandidates? fold. The fold records only candidate factors, not quotients, so the quotient is returned existentially for the corresponding successful bhksIndicatorCandidate? call.

def Hex.bhksRecover? (f : ZPoly) (d : LiftData) : Option (Array ZPoly)

Return the factors recovered by the lattice computation when all checks succeed.

Equations

• Hex.bhksRecover? f d = Hex.BhksRecoveryResult.toOption✝ (Hex.bhksRecoverClassified✝ f d)

theorem Hex.bhksRecover?_eq_some_of_checks (f : ZPoly) (d : LiftData) {candidates : Array ZPoly} (hrows : 1 ≤ (bhksLatticeBasis f d.p d.k d.liftedFactors).factorCount + (bhksLatticeBasis f d.p d.k d.liftedFactors).coeffWidth) (hnondeg : bhksDegenerateIndicatorPartition (bhksProjectedRows (bhksLatticeBasis f d.p d.k d.liftedFactors) hrows) (bhksEquivalenceClassIndicators (bhksProjectedRows (bhksLatticeBasis f d.p d.k d.liftedFactors) hrows)) = false) (hcand : bhksIndicatorCandidates? f d (bhksEquivalenceClassIndicators (bhksProjectedRows (bhksLatticeBasis f d.p d.k d.liftedFactors) hrows)) = some candidates) (hprod : candidates.polyProduct = f) : bhksRecover? f d = some candidates

If the executable BHKS recovery guards all pass, bhksRecover? returns the verified candidate array.

This lemma is the public proof-facing surface for callers that should not unfold the private failure classifier used by the executable.