Three Completion Tasks

Abstract

Identity, representative normalization, and future behavior are distinct completion tasks, with one same-readout implication recorded honestly.

Theorem 1.1 (Prime valuations can identify an ideal without a global generator).

$$\begin{gathered} \mathrm{DedekindDomain}(R)\wedge \mathrm{Nontrivial}(\mathrm{ClassGroup}(R))\Rightarrow \\ \exists I:\mathrm{Ideal}(R),\mathrm{PrimeValuationIdentityCompletion}(I)\wedge \neg \mathrm{IsPrincipal}(I)\wedge \neg \mathrm{UniqueGenerator}(I). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ThreeCompletionOrthogonality.prime_valuation_identity_without_global_generator (✓ std3). ∎

Source. Repository-derived.

Commentary.

Over a Dedekind domain with nontrivial class group, the imported prime valuation faithfulness theorem identifies a nonzero ideal supplied by the class group, while nonprincipality excludes every generator.

Theorem 1.2 (A PID has no valuation-identified nonprincipal witness).

$$\neg \exists I:\mathrm{Ideal}(\mathbb{Z}),\mathrm{PrimeValuationIdentityCompletion}(I)\wedge \neg \mathrm{IsPrincipal}(I).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ThreeCompletionOrthogonality.nontrivial_class_group_is_necessary_for_valuation_generator_gap (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every ideal of the integers is principal. This concrete counterexample shows why the nontrivial-class-group premise is necessary for the first strictness witness.

Theorem 1.3 (Class-group principality does not choose a unique generator).

$$\exists I:\mathrm{Ideal}(\mathbb{Z}),\mathrm{ClassGroupPrincipalityDecision}(I)\wedge \mathrm{IsPrincipal}(I)\wedge \neg \mathrm{UniqueGenerator}(I).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ThreeCompletionOrthogonality.class_group_principality_without_unique_generator (✓ std3). ∎

Source. Repository-derived.

Commentary.

The imported integer witnesses one and minus one generate the same nonzero principal ideal. The class-group criterion decides principality, but the ideal equation has more than one generator.

Theorem 1.4 (A closed behavior quotient can merge microscopic identities).

$$\begin{gathered} \forall n\in \mathbb{N},\mathrm{FactorsThrough}(qBool,\mathrm{iidTranscript}(n))\wedge \\ \mathrm{BehaviorCompletion}(qBool,\mathrm{iidTranscript}(n))\wedge \\ \exists x,y\in Bool,x\ne y\wedge \ker (qBool,x,y). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ThreeCompletionOrthogonality.future_behavior_quotient_merges_micro_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite repetition count, including zero, the constant Boolean transcript law factors through the one-point interface. False and true remain distinct states in the same Setoid.ker fiber.

Theorem 1.5 (Identity completion does not imply normalization completion).

$$\mathrm{IdentityCompletion}(idBool)\wedge \neg \mathrm{NormalizationCompletion}(trueBoolRelation).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ThreeCompletionOrthogonality.identity_completion_does_not_imply_normalization_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The identity readout separates Boolean states, while the indiscriminate Boolean representative relation has two representatives per object.

Theorem 1.6 (Normalization completion does not imply identity completion).

$$\mathrm{NormalizationCompletion}(equalityBoolRelation)\wedge \neg \mathrm{IdentityCompletion}(constantBoolInterface).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ThreeCompletionOrthogonality.normalization_completion_does_not_imply_identity_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Equality chooses one Boolean representative for each object, while the constant interface still merges false and true.

Theorem 1.7 (Normalization completion does not imply behavior completion).

$$\mathrm{NormalizationCompletion}(equalityBoolRelation)\wedge \neg \mathrm{BehaviorCompletion}(constantBoolInterface,identityBoolFuture).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ThreeCompletionOrthogonality.normalization_completion_does_not_imply_behavior_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Unique equality representatives coexist with a constant readout and an identity-valued future that differs inside its fiber.

Theorem 1.8 (Behavior completion does not imply identity completion).

$$\mathrm{BehaviorCompletion}(constantBoolInterface,constantFuture)\wedge \neg \mathrm{IdentityCompletion}(constantBoolInterface).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ThreeCompletionOrthogonality.behavior_completion_does_not_imply_identity_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

A constant future is closed on the constant Boolean interface, but that interface does not identify its two microscopic states.

Theorem 1.9 (Behavior completion does not imply normalization completion).

$$\mathrm{BehaviorCompletion}(constantBoolInterface,constantFuture)\wedge \neg \mathrm{NormalizationCompletion}(trueBoolRelation).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ThreeCompletionOrthogonality.behavior_completion_does_not_imply_normalization_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Constant Boolean behavior closes, while an indiscriminate representative relation still fails uniqueness.

Theorem 1.10 (Identity under one readout implies every deterministic behavior).

$$\forall q,f,\mathrm{IdentityCompletion}(q)\Rightarrow \mathrm{BehaviorCompletion}(q,f).$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ThreeCompletionOrthogonality.same_readout_identity_implies_behavior_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The sixth requested nonimplication direction is false under the formalized same-readout semantics: injectivity turns equal readouts into equal states, so every deterministic future is fiber-constant.

References

• Truth anchor: D5/S3/Observer/Completion/ThreeCompletionOrthogonality.behavior_completion_does_not_imply_identity_completion
• Truth anchor: D5/S3/Observer/Completion/ThreeCompletionOrthogonality.behavior_completion_does_not_imply_normalization_completion
• Truth anchor: D5/S3/Observer/Completion/ThreeCompletionOrthogonality.class_group_principality_without_unique_generator
• Truth anchor: D5/S3/Observer/Completion/ThreeCompletionOrthogonality.future_behavior_quotient_merges_micro_identity
• Truth anchor: D5/S3/Observer/Completion/ThreeCompletionOrthogonality.identity_completion_does_not_imply_normalization_completion
• Truth anchor: D5/S3/Observer/Completion/ThreeCompletionOrthogonality.nontrivial_class_group_is_necessary_for_valuation_generator_gap
• Truth anchor: D5/S3/Observer/Completion/ThreeCompletionOrthogonality.normalization_completion_does_not_imply_behavior_completion
• Truth anchor: D5/S3/Observer/Completion/ThreeCompletionOrthogonality.normalization_completion_does_not_imply_identity_completion
• Truth anchor: D5/S3/Observer/Completion/ThreeCompletionOrthogonality.prime_valuation_identity_without_global_generator
• Truth anchor: D5/S3/Observer/Completion/ThreeCompletionOrthogonality.same_readout_identity_implies_behavior_completion
• Dependency: D5/S3/Factorization/Embeddings/DirichletUnitCompletion
• Dependency: D5/S3/Factorization/IdealClassGroups/IdealIdentityPrincipalityGeneratorLayers
• Dependency: D5/S3/Factorization/IdealClassGroups/LocalPrincipalityBlindness
• Dependency: D5/S3/Observer/MeasureSeparation/FactorizedTranscriptKernelBarrier