Common-Rule Information Convergence

Abstract

Correct common facts align a shared rule, while distinct rules can still disagree.

Theorem 1.1 (Common facts align shared rules but not distinct rules).

$$\forall X,Z,U:\mathrm{Type},T:X\to Z,d,d_i,d_j:Z\to U,(\forall x:X,z_i,z_j:Z,(z_i=T(x)\wedge z_j=T(x))\Rightarrow d(z_i)=d(z_j))\wedge (\forall x:X,z:Z,(T(x)=z\wedge d_i(z)\ne d_j(z))\Rightarrow d_i(T(x))\ne d_j(T(x))).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CommonRuleInformationConvergence.common_rule_information_convergence (✓ std3). ∎

Source. Repository-derived.

Commentary.

The target is the canonical concept readout from source states to fully disclosed fact values. Two fact values are sufficient here when each is equal to that target value.

The first public conjunct applies one deterministic rule to two correct fact values. The second public conjunct applies distinct rules at a disclosed target value and preserves their disagreement.

Repository searches found no theorem containing both clauses. The existing disclosure-defect result instead concerns collisions and consequence recovery. The proof directly applies equality transport.

References

• Truth anchor: D5/S3/ConceptDynamics/CommonRuleInformationConvergence.common_rule_information_convergence
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition