Truthful Reporting Blocks an Inverted Spectrum

Abstract

Exact public recovery forces phenomenal agreement; an inverted pair refutes it.

Theorem 1.1 (Truthful public reporting forces phenomenal agreement).

$$\forall State\in Type,Phenomenal\in Type,Public\in Type,p\in State\to Phenomenal,q\in State\to Public,x\in State,y\in State,\mathrm{TruthfulPublicReport}\left(p,q\right)\Rightarrow \left(q\left(x\right)=q\left(y\right)\Rightarrow p\left(x\right)=p\left(y\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Reporting/TruthfulReportBlocksInvertedSpectrum.truthful_public_report_forces_phenomenal_agreement (✓ std3). ∎

Source. Repository-derived.

Commentary.

TruthfulPublicReport(p, q) requires a total recovery map from every public value to a phenomenal value, with p equal to that map after q. Thus the phenomenal readout is determined entirely by the public readout.

Consequently, any two states in the same public fiber must have the same phenomenal value. The conclusion concerns every pair of states, not only values in a chosen or observed part of the public image.

References

• Truth anchor: D5/S3/ConceptDynamics/Reporting/TruthfulReportBlocksInvertedSpectrum.truthful_public_report_forces_phenomenal_agreement