IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.SubstrateDichotomy

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/SubstrateDichotomy.lean
   3
   4  The factoring-speedup fork, stated honestly.
   5
   6  The arithmetic layer is closed: the orbit semiring is isomorphic to `Nat` as an
   7  ordered commutative semiring, so any factoring procedure expressible in orbit
   8  arithmetic has the same operation count as the corresponding `Nat` procedure
   9  (transport). No arithmetic speedup is possible.
  10
  11  The only surviving channel is a physical recognition readout (Door B,
  12  `PhysicalPeriodReadout`). This module records the resulting dichotomy:
  13
  14  * Branch B (coherent substrate). If the substrate supplies a certified factor
  15    readout, `N` factors nontrivially. This conditional is PROVED.
  16  * Branch A (definite ledger). The magnitude observable available to a
  17    definite-ledger substrate cannot extract a factor coordinate. PROVED.
  18
  19  Which branch the RS substrate realizes for factorization is still open. A
  20  previous reading treated the proved `Signal8` interference layer as only
  21  constant-dimensional and concluded that the current substrate is Branch A.
  22  That reading was too strong: `Gravity.MacroscopicLedger` formalizes finite
  23  many-body ledger carriers as `PiTensorProduct` powers of `Signal8`, and
  24  `Gravity.QuantumChannel.PhysicalChannelAmplitudeLinear` proves amplitude
  25  linearity for the many-body physical channel lift.
  26
  27  The remaining open node is narrower and sharper: no theorem here constructs a
  28  period-readout dynamics on that many-body amplitude carrier, nor proves that
  29  such a readout has polynomial resource scaling. The tensor/amplitude substrate
  30  exists; the factoring-specific transform does not.
  31
  32  This file asserts neither branch antecedent. It proves both conditionals and
  33  names the open node.
  34-/
  35
  36import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PhysicalPeriodReadout
  37
  38namespace IndisputableMonolith
  39namespace Foundation
  40namespace PrimitiveRecognitionCalculus
  41namespace Factorization
  42
  43open DistinctionNat
  44
  45/-- Branch B antecedent: the substrate supplies a certified factor readout for
  46some base modulo `N`. This is exactly the Door B oracle. It is NOT proved to hold
  47for the RS substrate; see the module docstring. A factoring *speedup* is the
  48stronger claim that this antecedent can be delivered uniformly in `N` at cost
  49below classical factoring, which is the open performance problem. -/
  50def CoherentSubstrateDeliversFactor (N : DistinctionNat) (hN : N ≠ zero) : Prop :=
  51  ∃ a : DistinctionNat, Nonempty (CertifiedFactorReadout N hN a)
  52
  53/-- Branch B conditional (PROVED): if the substrate delivers a certified factor
  54readout, `N` factors nontrivially. The reduction is unconditional; only the
  55antecedent is open. -/
  56theorem coherentSubstrate_delivers_factorization
  57    {N : DistinctionNat} {hN : N ≠ zero}
  58    (h : CoherentSubstrateDeliversFactor N hN) :
  59    nontrivialFactorization N := by
  60  rcases h with ⟨a, ⟨r⟩⟩
  61  exact certifiedFactorReadout_to_nontrivialFactorization r
  62
  63/-- Branch A obstruction (PROVED, restated from the recognition lower bound): the
  64product-magnitude observable available to a definite-ledger substrate cannot
  65extract a factor coordinate. A definite ledger that reads only Archimedean
  66magnitude is blind to the factor chart. -/
  67theorem definiteLedger_magnitude_cannot_extract_factor :
  68    ¬ MagnitudeOnlyObservable (fun a _ => a.toNat) :=
  69  leftFactorObservable_not_magnitudeOnly
  70
  71/-- The honest dichotomy certificate. Both conditionals are theorems. The Branch B
  72antecedent `CoherentSubstrateDeliversFactor` is the open foundational node and is
  73NOT asserted here. -/
  74structure SubstrateDichotomyCertificate : Prop where
  75  branchB_conditional :
  76    ∀ {N : DistinctionNat} {hN : N ≠ zero},
  77      CoherentSubstrateDeliversFactor N hN → nontrivialFactorization N
  78  branchA_obstruction :
  79    ¬ MagnitudeOnlyObservable (fun a _ => a.toNat)
  80
  81theorem substrate_dichotomy_certificate : SubstrateDichotomyCertificate where
  82  branchB_conditional := by
  83    intro N hN h
  84    exact coherentSubstrate_delivers_factorization h
  85  branchA_obstruction := definiteLedger_magnitude_cannot_extract_factor
  86
  87end Factorization
  88end PrimitiveRecognitionCalculus
  89end Foundation
  90end IndisputableMonolith
  91