Scaling-Register Rigidity

Abstract

Typed realization carries analytic uniqueness through the registered action to conditional total-code rigidity.

Definition 1.1 (A scaling register is a nontrivial coordinatewise exponential).

Lean statement: D5/S3/Zeros/ScalingRegisterRigidity.ScalingRegister

Formalization. D5/S3/Zeros/ScalingRegisterRigidity.ScalingRegister (✓ std3).

Source. Repository-derived.

Commentary.

For a ledger length ell and factor family R, ScalingRegister(ell,R) means that some g gives R(s,a)=exp(g(s)ell(a)) for every s and a, and that R(s,a) differs from one at some coordinate. This is the formal carrier of Definition 23.2’s dependence and nontriviality clauses.

Honest scope declaration: the predicate does not internalize “unrecorded” ledger custody. Address independence is the formal proxy for an explicit global ledger factor; the institutional classification itself remains at the narrative layer.

Theorem 1.2 (A nontrivial register is not address-independent).

$$\forall x2\in \mathrm{LedgerLength},\forall x3\in \left(\forall x3\in \mathrm{Complex},\forall x4\in \cdot ,\mathrm{Complex}\right),\forall x4\in \mathrm{ScalingRegister}\left(x2,x3\right),\neg \mathrm{AddressIndependent}\left(x3\right)$$

Proof. Machine-checked in Lean as D5/S3/Zeros/ScalingRegisterRigidity.scaling_register_not_address_independent (✓ std3). ∎

Source. Repository-derived.

Commentary.

At the zero address every exponential register equals one. Address independence would therefore make every coordinate one, contradicting the explicit nontrivial witness.

Definition 1.3 (A register acts on the tagged data field).

Lean statement: D5/S3/Zeros/ScalingRegisterRigidity.applyRegister

Formalization. D5/S3/Zeros/ScalingRegisterRigidity.applyRegister (✓ std3).

Source. Repository-derived.

Commentary.

For data X.data(a,s), applyRegister(R,X) replaces that value by R(s,a)X.data(a,s), while preserving the rules and ledger fields.

Theorem 1.4 (A nontrivial register changes nowhere-zero data).

$$\forall x3\in \left(\forall x3\in \mathrm{Complex},\forall x4\in \cdot ,\mathrm{Complex}\right),\forall x4\in \mathrm{TotalCode},\left(\forall x5\in \cdot ,\forall x6\in \mathrm{Complex},\mathrm{TotalCodedata}\left(x4,x5,x6\right)\ne 0\right)\Rightarrow \left(\left(\exists x6\in \mathrm{Complex},\exists x7\in \cdot ,x3\left(x6,x7\right)\ne 1\right)\Rightarrow \mathrm{applyRegister}\left(x3,x4\right)\ne x4\right)$$

Proof. Machine-checked in Lean as D5/S3/Zeros/ScalingRegisterRigidity.applyRegister_ne_of_nontrivial (✓ std3). ∎

Source. Repository-derived.

Commentary.

At the nontrivial witness, equality of total codes would equate the data values R(s,a)X.data(a,s) and X.data(a,s). Cancelling the explicitly nonzero data value forces R(s,a)=1, a contradiction.

Definition 1.5 (Realization projects object data and carries register actions).

Lean statement: D5/S3/Zeros/ScalingRegisterRigidity.RealizesAt

Formalization. D5/S3/Zeros/ScalingRegisterRigidity.RealizesAt (✓ std3).

Source. Repository-derived.

Commentary.

RealizesAt(a,X,f) records both that the declared address projection of X.data reads as f and that the same projection sends applyRegister(R,X) to the pointwise product R(s,a)f(s). The compatibility clause is a defining model law, not a bridge assumption derived from mathlib.

Theorem 1.6 (Realized same germ and same total code force a trivial register).

$$\begin{array}{c}U\subseteq \mathbb{C},f,\tilde{f}:\mathbb{C}\to \mathbb{C},\mathrm{AnalyticOnNhd}(f,U),\mathrm{AnalyticOnNhd}(\tilde{f},U),\\ \mathrm{IsPreconnected}(U),s_0\in U,f{=}_{\mathrm{nhds}(s_0)}\tilde{f},\\ R:\mathbb{C}\to A\to \mathbb{C},X:\mathrm{TotalCode}(A\to \mathbb{C}\to \mathbb{C},Q,L),\\ \mathrm{RealizesAt}(a,X,f),\mathrm{RealizesAt}(a,\mathrm{applyRegister}(R,X),\tilde{f}),\\ \forall a,s,X_{\mathrm{data}}(a,s)\ne 0,\mathrm{applyRegister}(R,X)=X\end{array}\Rightarrow \left(f=\tilde{f}\text{ on }U\right)\wedge \left(\forall s,\tilde{f}(s)=R(s,a)f(s)\right)\wedge \left(\forall s,a,R(s,a)=1\right).$$

Proof. Machine-checked in Lean as D5/S3/Zeros/ScalingRegisterRigidity.realized_same_germ_same_total_code_forces_trivial_register (✓ std3). ∎

Source. Repository-derived.

Commentary.

Analytic continuation uniqueness identifies the two readings on U. The RealizesAt model law then identifies the registered reading pointwise with R(s,a)f(s). Finally, a non-one witness and nowhere-zero data would produce an applyRegister object change, contradicting equal total code.

Honest scope declaration: this is conditional on the typed realization relations and does not internalize unrecorded ledger custody.

Theorem 1.7 (Realized code-preserving continuations exclude scaling registers).

$$\forall x3\in \mathrm{AnalyticOnNhd}\left(\cdot ,\cdot \right),\forall x4\in \mathrm{AnalyticOnNhd}\left(\cdot ,\cdot \right),\forall x5\in \mathrm{IsPreconnected}\left(\cdot \right),\forall x7\in \cdot \in \cdot ,\forall x8\in \mathrm{EventuallyEq}\left(\mathrm{nhds}\left(\cdot \right),\cdot ,\cdot \right),\forall x13\in \mathrm{LedgerLength},\forall x14\in \left(\forall x14\in \mathrm{Complex},\forall x15\in \cdot ,\mathrm{Complex}\right),\forall x15\in \mathrm{TotalCode},\forall x16\in \cdot ,\forall x17\in \mathrm{RealizesAt}\left(x16,x15,\cdot \right),\forall x18\in \mathrm{RealizesAt}\left(x16,\mathrm{applyRegister}\left(x14,x15\right),\cdot \right),\left(\forall x19\in \cdot ,\forall x20\in \mathrm{Complex},\mathrm{TotalCodedata}\left(x15,x19,x20\right)\ne 0\right)\Rightarrow \left(\mathrm{applyRegister}\left(x14,x15\right)=x15\Rightarrow \left(\neg \mathrm{ScalingRegister}\left(x13,x14\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Zeros/ScalingRegisterRigidity.realized_same_germ_same_total_code_excludes_scaling_register (✓ std3). ∎

Source. Repository-derived.

Commentary.

The realized rigidity theorem makes R pointwise one, contradicting the nontriviality witness required by ScalingRegister. This is the explicit ScalingRegister exclusion and retains every realization and code premise.

Theorem 1.8 (The scaling-register predicate has a concrete witness).

$$\mathrm{ScalingRegister}\left(\mathrm{castAddHom}\left(\mathrm{Real}\right),\forall x0\in \mathrm{Type},\forall x1\in \mathrm{Type},\exp \left(\mathrm{ofReal}\left(\mathrm{pi}\right)\cdot \mathrm{I}\cdot \mathrm{cast}\left(x1\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Zeros/ScalingRegisterRigidity.integer_scaling_register_exists (✓ std3). ∎

Source. Repository-derived.

Commentary.

On the integer ledger, the cast-to-real length and the factor exp(pi i n) satisfy the register shape, while n=1 evaluates to minus one rather than one. This kernel-checked counterexample-style witness prevents the main exclusion theorem from succeeding merely because ScalingRegister is empty.

References

• Truth anchor: D5/S3/Zeros/ScalingRegisterRigidity.RealizesAt
• Truth anchor: D5/S3/Zeros/ScalingRegisterRigidity.ScalingRegister
• Truth anchor: D5/S3/Zeros/ScalingRegisterRigidity.applyRegister
• Truth anchor: D5/S3/Zeros/ScalingRegisterRigidity.applyRegister_ne_of_nontrivial
• Truth anchor: D5/S3/Zeros/ScalingRegisterRigidity.integer_scaling_register_exists
• Truth anchor: D5/S3/Zeros/ScalingRegisterRigidity.realized_same_germ_same_total_code_excludes_scaling_register
• Truth anchor: D5/S3/Zeros/ScalingRegisterRigidity.realized_same_germ_same_total_code_forces_trivial_register
• Truth anchor: D5/S3/Zeros/ScalingRegisterRigidity.scaling_register_not_address_independent
• Dependency: D5/S0/Conventions/TotalCode
• Dependency: D5/S3/Zeros/CompletedZeta