Golden Thread Blowup

Abstract

Golden completion curves share the same completed value while their first blow-up coordinate and tangent retain the observer origin.

Theorem 1.1 (Golden Thread Curve Zero).

$\forall c : R, (g o l d e n T h re a d C u r v ec 0 = R e a l . g o l d e n R a t i o) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_curve_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

This theorem establishes golden thread curve zero in the module’s typed setting.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.2 (Golden Thread Curve Sub Golden).

$\forall c : R, h : R, (1 - h \times c \neq = 0) \Rightarrow (g o l d e n T h re a d C u r v ec h - R e a l . g o l d e n R a t i o = (h \times c) \times (R e a l . g o l d e n R a t i o - R e a l . g o l d e n C o nj) / (1 - h \times c)) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_curve_sub_golden (✓ std3). ∎

Source. Repository-derived.

Commentary.

Difference from the completed fixed point in the inverse projective chart.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.3 (Golden Thread Curve Sub Conjugate).

$\forall c : R, h : R, (1 - h \times c \neq = 0) \Rightarrow (g o l d e n T h re a d C u r v ec h - R e a l . g o l d e n C o nj = (R e a l . g o l d e n R a t i o - R e a l . g o l d e n C o nj) / (1 - h \times c)) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_curve_sub_conjugate (✓ std3). ∎

Source. Repository-derived.

Commentary.

Difference from the conjugate fixed point in the inverse projective chart.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.4 (Golden Cross Ratio Thread Curve).

$\forall c : R, h : R, (1 - h \times c \neq = 0) \Rightarrow (g o l d e n C ross R a t i o (g o l d e n T h re a d C u r v ec h) = h \times c) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_cross_ratio_thread_curve (✓ std3). ∎

Source. Repository-derived.

Commentary.

The inverse chart recovers the prescribed projective coordinate exactly.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.5 (Golden Thread Curve Has Deriv At).

$\forall c : R, (H a sDer i v A t (g o l d e n T h re a d C u r v ec) (c \times (R e a l . g o l d e n R a t i o - R e a l . g o l d e n C o nj)) 0) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_curve_hasDerivAt (✓ std3). ∎

Source. Repository-derived.

Commentary.

The inverse golden chart has first derivative c(φ-ψ) at completion.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.6 (Golden Thread Curve Has Deriv At Sqrt Five).

$\forall c : R, (H a sDer i v A t (g o l d e n T h re a d C u r v ec) (c \times R e a l . s q r t 5) 0) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_curve_hasDerivAt_sqrt_five (✓ std3). ∎

Source. Repository-derived.

Commentary.

The tangent coefficient displays the discriminant gap sqrt 5.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.7 (Golden Thread Completion Value eq).

$\forall c_{1} : R, c_{2} : R, (g o l d e n T h re a d C u r v e c_{1} 0 = g o l d e n T h re a d C u r v e c_{2} 0) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_completion_value_eq (✓ std3). ∎

Source. Repository-derived.

Commentary.

Two origin coefficients give the same completed value.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.8 (Golden Thread Tangent Injective).

$(F u n c t i o n . I nj ec t i v e (λ c : R \mapsto c \times R e a l . s q r t 5)) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_tangent_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

Distinct origin coefficients give distinct completion tangents.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.9 (Golden Geometric Thread Cross Ratio).

$\forall c : R, n : N, (1 - g o l d e n P ro j ec t i v e M u lt i pl i e r^{n} \times c \neq = 0) \Rightarrow (g o l d e n C ross R a t i o (g o l d e n G eo m e t r i c T h re a d c n) = g o l d e n P ro j ec t i v e M u lt i pl i e r^{n} \times c) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_geometric_thread_cross_ratio (✓ std3). ∎

Source. Repository-derived.

Commentary.

At any depth where the inverse affine chart is defined, the blow-up coordinate is exactly c * multiplier^n.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.10 (Golden Geometric Thread Origin Recovery).

$\forall c : R, n : N, (1 - g o l d e n P ro j ec t i v e M u lt i pl i e r^{n} \times c \neq = 0) \Rightarrow ((g o l d e n P ro j ec t i v e M u lt i pl i e r^{- 1})^{n} \times g o l d e n C ross R a t i o (g o l d e n G eo m e t r i c T h re a d c n) = c) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_geometric_thread_origin_recovery (✓ std3). ∎

Source. Repository-derived.

Commentary.

Since the multiplier is nonzero, renormalization recovers the origin coefficient at every finite depth.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

References

Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_cross_ratio_thread_curve
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_geometric_thread_cross_ratio
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_geometric_thread_origin_recovery
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_completion_value_eq
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_curve_hasDerivAt
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_curve_hasDerivAt_sqrt_five
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_curve_sub_conjugate
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_curve_sub_golden
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_curve_zero
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenThreadBlowup.golden_thread_tangent_injective
Dependency: D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative

Keyboard shortcuts

trureturing Blueprint

Golden Thread Blowup

Abstract

References