Shared Charge, Different Shells

Abstract

Distinct observer shells may factor through the same charge readout while retaining different residual information.

Theorem 1.1 (Common Charge Projections Agree).

$$\begin{gathered} \forall X:{\mathrm{Type}}_u,Y_1:{\mathrm{Type}}_v,Y_2:{\mathrm{Type}}_w,C:{\mathrm{Type}}_z,shel{l}_1:X\to Y_1,shel{l}_2:X\to Y_2,charg{e}_1:Y_1\to C,charg{e}_2:Y_2\to C,charge:X\to C,x:X, \\ (\mathrm{CarriesCharge}\left(shel{l}_1,charg{e}_1,charge\right))\wedge (\mathrm{CarriesCharge}\left(shel{l}_2,charg{e}_2,charge\right))\Rightarrow \\ (charg{e}_1(shel{l}_1(x))=charg{e}_2(shel{l}_2(x))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/SharedChargeDifferentShells.common_charge_agreement (✓ std3). ∎

Source. Repository-derived.

Commentary.

If two shell maps both factor the same charge observation, their projected readings agree at every source point.

The equality is only after applying the respective charge projections; it does not identify the shell outputs themselves.

Theorem 1.2 (The Concrete Shells Carry the Same Charge).

$$((\mathrm{CarriesCharge}\left(coarseShell,id,fst\right))\wedge (\mathrm{CarriesCharge}\left(fineShell,fineCharge,fst\right))).$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/SharedChargeDifferentShells.concrete_shells_carry_same_charge (✓ std3). ∎

Source. Repository-derived.

Commentary.

The coarse Boolean shell reads the first coordinate, while the fine shell retains the full pair and projects its first coordinate as charge.

Both factorizations recover the same source charge, but the conjunction alone does not assert equal information content.

Theorem 1.3 (One Coarse Collision Is Separated by the Fine Shell).

$$((\mathrm{coarseShell}\left((true,false)\right)=\mathrm{coarseShell}\left((true,true)\right))\wedge (\mathrm{fineShell}\left((true,false)\right)\ne \mathrm{fineShell}\left((true,true)\right))).$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/SharedChargeDifferentShells.same_charge_different_observer_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

The inputs (true,false) and (true,true) have the same coarse first-coordinate reading.

Their fine-shell values remain distinct, giving a concrete residual distinction beyond the shared charge.

Theorem 1.4 (Shared Charge Does Not Force Equal Resolution).

$$(\exists x:\mathrm{Bool}\times \mathrm{Bool},y:\mathrm{Bool}\times \mathrm{Bool},((\mathrm{coarseShell}\left(x\right)=\mathrm{coarseShell}\left(y\right))\wedge (\mathrm{fineShell}\left(x\right)\ne \mathrm{fineShell}\left(y\right)))).$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/SharedChargeDifferentShells.shared_charge_does_not_force_same_resolution (✓ std3). ∎

Source. Repository-derived.

Commentary.

There exist two Boolean-pair inputs that collide under the coarse shell and are separated by the fine shell.

This existential counterexample refutes only equality of observer resolution from shared charge; it does not compare arbitrary shell orders.

References

• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/SharedChargeDifferentShells.common_charge_agreement
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/SharedChargeDifferentShells.concrete_shells_carry_same_charge
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/SharedChargeDifferentShells.same_charge_different_observer_witness
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/SharedChargeDifferentShells.shared_charge_does_not_force_same_resolution