IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.RecognitionLowerBound

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/RecognitionLowerBound.lean
   3
   4  Door A, first honest theorem layer: magnitude-only observables cannot see
   5  factor coordinates. This is not a complexity lower bound. It is the formal
   6  obstruction that kills Archimedean-only/J-cost-magnitude factoring heuristics.
   7-/
   8
   9import Mathlib
  10import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.FiniteMulCharacter
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace PrimitiveRecognitionCalculus
  15namespace Factorization
  16
  17open DistinctionNat
  18
  19/-- A magnitude-only observable factors through the product orbit position. -/
  20def MagnitudeOnlyObservable
  21    (F : DistinctionNat → DistinctionNat → Nat) : Prop :=
  22  ∀ a b c d : DistinctionNat,
  23    factorPairProduct a b = factorPairProduct c d → F a b = F c d
  24
  25/-- The displayed product magnitude is magnitude-only. -/
  26def productMagnitudeObservable (a b : DistinctionNat) : Nat :=
  27  archimedeanMagnitude (factorPairProduct a b)
  28
  29theorem productMagnitudeObservable_magnitudeOnly :
  30    MagnitudeOnlyObservable productMagnitudeObservable := by
  31  intro a b c d h
  32  unfold productMagnitudeObservable
  33  exact same_product_same_magnitude h
  34
  35/-- A left-factor extractor cannot be magnitude-only: the same product can have
  36different left coordinates. -/
  37theorem leftFactorObservable_not_magnitudeOnly :
  38    ¬ MagnitudeOnlyObservable (fun a _ => a.toNat) := by
  39  intro h
  40  have hsame := h (ofNat 2) (ofNat 6) (ofNat 3) (ofNat 4)
  41    two_six_product_eq_three_four
  42  simp at hsame
  43
  44/-- A right-factor extractor cannot be magnitude-only. -/
  45theorem rightFactorObservable_not_magnitudeOnly :
  46    ¬ MagnitudeOnlyObservable (fun _ b => b.toNat) := by
  47  intro h
  48  have hsame := h (ofNat 2) (ofNat 6) (ofNat 3) (ofNat 4)
  49    two_six_product_eq_three_four
  50  simp at hsame
  51
  52/-- Any observable obtained by applying a scalar post-processing function to
  53the product magnitude is still magnitude-only. This includes J-cost-style
  54ratio or magnitude scores unless they are coupled to residue or character data. -/
  55def productMagnitudePostprocess (φ : Nat → Nat)
  56    (a b : DistinctionNat) : Nat :=
  57  φ (productMagnitudeObservable a b)
  58
  59theorem productMagnitudePostprocess_magnitudeOnly (φ : Nat → Nat) :
  60    MagnitudeOnlyObservable (productMagnitudePostprocess φ) := by
  61  intro a b c d h
  62  unfold productMagnitudePostprocess
  63  rw [productMagnitudeObservable_magnitudeOnly a b c d h]
  64
  65/-- No scalar post-processing of product magnitude can equal the left factor
  66coordinate for all factor pairs. -/
  67theorem no_productMagnitudePostprocess_extracts_left_factor :
  68    ¬ ∃ φ : Nat → Nat,
  69      ∀ a b : DistinctionNat,
  70        productMagnitudePostprocess φ a b = a.toNat := by
  71  intro h
  72  rcases h with ⟨φ, hφ⟩
  73  have h2 := hφ (ofNat 2) (ofNat 6)
  74  have h3 := hφ (ofNat 3) (ofNat 4)
  75  have hsame :
  76      productMagnitudePostprocess φ (ofNat 2) (ofNat 6) =
  77        productMagnitudePostprocess φ (ofNat 3) (ofNat 4) :=
  78    productMagnitudePostprocess_magnitudeOnly φ
  79      (ofNat 2) (ofNat 6) (ofNat 3) (ofNat 4)
  80      two_six_product_eq_three_four
  81  rw [h2, h3] at hsame
  82  simp at hsame
  83
  84/-- No scalar post-processing of product magnitude can equal the right factor
  85coordinate for all factor pairs. -/
  86theorem no_productMagnitudePostprocess_extracts_right_factor :
  87    ¬ ∃ φ : Nat → Nat,
  88      ∀ a b : DistinctionNat,
  89        productMagnitudePostprocess φ a b = b.toNat := by
  90  intro h
  91  rcases h with ⟨φ, hφ⟩
  92  have h6 := hφ (ofNat 2) (ofNat 6)
  93  have h4 := hφ (ofNat 3) (ofNat 4)
  94  have hsame :
  95      productMagnitudePostprocess φ (ofNat 2) (ofNat 6) =
  96        productMagnitudePostprocess φ (ofNat 3) (ofNat 4) :=
  97    productMagnitudePostprocess_magnitudeOnly φ
  98      (ofNat 2) (ofNat 6) (ofNat 3) (ofNat 4)
  99      two_six_product_eq_three_four
 100  rw [h6, h4] at hsame
 101  simp at hsame
 102
 103/-- Door A certificate: product magnitude is a real invariant, but coordinate
 104extraction is not a magnitude-only operation. -/
 105structure RecognitionLowerBoundCertificate : Prop where
 106  product_magnitude_is_magnitude_only :
 107    MagnitudeOnlyObservable productMagnitudeObservable
 108  left_factor_not_magnitude_only :
 109    ¬ MagnitudeOnlyObservable (fun a _ => a.toNat)
 110  right_factor_not_magnitude_only :
 111    ¬ MagnitudeOnlyObservable (fun _ b => b.toNat)
 112  product_magnitude_postprocess_is_magnitude_only :
 113    ∀ φ : Nat → Nat, MagnitudeOnlyObservable (productMagnitudePostprocess φ)
 114  product_magnitude_postprocess_cannot_extract_left :
 115    ¬ ∃ φ : Nat → Nat,
 116      ∀ a b : DistinctionNat,
 117        productMagnitudePostprocess φ a b = a.toNat
 118  product_magnitude_postprocess_cannot_extract_right :
 119    ¬ ∃ φ : Nat → Nat,
 120      ∀ a b : DistinctionNat,
 121        productMagnitudePostprocess φ a b = b.toNat
 122
 123theorem recognition_lower_bound_certificate :
 124    RecognitionLowerBoundCertificate where
 125  product_magnitude_is_magnitude_only := productMagnitudeObservable_magnitudeOnly
 126  left_factor_not_magnitude_only := leftFactorObservable_not_magnitudeOnly
 127  right_factor_not_magnitude_only := rightFactorObservable_not_magnitudeOnly
 128  product_magnitude_postprocess_is_magnitude_only :=
 129    productMagnitudePostprocess_magnitudeOnly
 130  product_magnitude_postprocess_cannot_extract_left :=
 131    no_productMagnitudePostprocess_extracts_left_factor
 132  product_magnitude_postprocess_cannot_extract_right :=
 133    no_productMagnitudePostprocess_extracts_right_factor
 134
 135end Factorization
 136end PrimitiveRecognitionCalculus
 137end Foundation
 138end IndisputableMonolith
 139