IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PhysicalPeriodReadout

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/PhysicalPeriodReadout.lean
   3
   4  Door B interface only. This file states what a physical or quantum-like
   5  period readout must certify before it can be used for factorization. It does
   6  not posit that such a readout exists.
   7-/
   8
   9import Mathlib
  10import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.RecognitionLowerBound
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace PrimitiveRecognitionCalculus
  15namespace Factorization
  16
  17open DistinctionNat
  18
  19/-- A certified period readout for a base `a` modulo `N`. -/
  20structure CertifiedPeriodReadout (N : DistinctionNat) (hN : N ≠ zero)
  21    (a : DistinctionNat) : Type where
  22  exponent : DistinctionNat
  23  witness : PeriodWitness N hN a exponent
  24
  25/-- A certified factor readout is stronger than a period readout: it exposes a
  26proper divisor certified by the period data. This is the minimal Lean-facing
  27interface a physical period-finder must satisfy. -/
  28structure CertifiedFactorReadout (N : DistinctionNat) (hN : N ≠ zero)
  29    (a : DistinctionNat) : Type where
  30  exponent : DistinctionNat
  31  factor_witness : ProperDivisorFromPeriod N hN a exponent
  32
  33theorem certifiedFactorReadout_to_nontrivialFactorization
  34    {N a : DistinctionNat} {hN : N ≠ zero}
  35    (r : CertifiedFactorReadout N hN a) :
  36    nontrivialFactorization N := by
  37  exact period_divisor_to_nontrivialFactorization r.factor_witness
  38
  39/-- The interface separates period certification from a factorization theorem.
  40The device, algorithm, or physical substrate must supply the certificate. -/
  41structure PhysicalPeriodReadoutCertificate : Prop where
  42  certified_factor_readout_extracts_factorization :
  43    ∀ {N a : DistinctionNat} {hN : N ≠ zero},
  44      CertifiedFactorReadout N hN a → nontrivialFactorization N
  45
  46theorem physical_period_readout_certificate :
  47    PhysicalPeriodReadoutCertificate where
  48  certified_factor_readout_extracts_factorization := by
  49    intro N a hN r
  50    exact certifiedFactorReadout_to_nontrivialFactorization r
  51
  52end Factorization
  53end PrimitiveRecognitionCalculus
  54end Foundation
  55end IndisputableMonolith
  56