IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.RecognitionLowerBound
Magnitude-only observables on a product of multiplicative characters see only the product orbit, never the separate left or right factors. The module packages that obstruction as a certificate: any post-processing of the product magnitude still cannot recover a single factor. Downstream period-readout arguments cite it to justify why physical readout must use more than pure magnitude data.
claimA magnitude-only observable on a finite multiplicative character factors through the product orbit position. In particular, the product-magnitude map is magnitude-only, while the left- and right-factor projections are not; no post-processing of the product magnitude recovers either factor. The module exports a recognition lower-bound certificate recording this obstruction.
background
In the Primitive Recognition Calculus factorization layer, observables act on finite multiplicative characters (imported from FiniteMulCharacter). A magnitude-only observable is one that depends only on the absolute size of the character value, not on phase or factor ordering.
The product orbit position is the joint magnitude of a left and right factor. The module introduces the product-magnitude observable and shows it is magnitude-only, then contrasts it with the left- and right-factor observables, which fail to be magnitude-only.
Post-processing is allowed: any function of the product magnitude remains magnitude-only. The lower-bound claim is that no such post-processing can extract a single factor. That obstruction is packaged as RecognitionLowerBoundCertificate.
proof idea
The module is a short factorization argument, not a pure definition dump. It defines MagnitudeOnlyObservable and the product-magnitude map, proves the product map is magnitude-only, and proves the left- and right-factor maps are not. It then lifts the product map through arbitrary post-processing and shows, by the magnitude-only property, that neither factor is recoverable. The certificate constructor assembles these facts into a single named witness for downstream use.
why it matters in Recognition Science
Physical period readout (PhysicalPeriodReadout) imports this module to justify that a pure magnitude channel cannot separate factors on the recognition side. In the Recognition Science foundation, that lower bound supports the claim that readout of periods and octave structure needs more structure than a single product magnitude (consistent with the eight-tick / T7 forcing context). The certificate is the portable object later layers cite when they argue that recognition must retain factor-sensitive data rather than collapse to $|xy|$.
scope and limits
- Does not construct a physical measurement protocol or experimental bound.
- Does not treat continuous or infinite character groups beyond the finite multiplicative setting.
- Does not claim phase-sensitive or non-magnitude observables are impossible.
- Does not derive numerical constants (phi, alpha, mass rungs) from the certificate.
- Does not by itself force D = 3 or the eight-tick octave.
used by (1)
depends on (1)
declarations in this module (11)
-
def
MagnitudeOnlyObservable -
def
productMagnitudeObservable -
theorem
productMagnitudeObservable_magnitudeOnly -
theorem
leftFactorObservable_not_magnitudeOnly -
theorem
rightFactorObservable_not_magnitudeOnly -
def
productMagnitudePostprocess -
theorem
productMagnitudePostprocess_magnitudeOnly -
theorem
no_productMagnitudePostprocess_extracts_left_factor -
theorem
no_productMagnitudePostprocess_extracts_right_factor -
structure
RecognitionLowerBoundCertificate -
theorem
recognition_lower_bound_certificate