Active Semicircle

Abstract

A reflected rational response is negative exactly inside an active semicircle and diverges negatively at its right-half-plane pole.

Definition 1.1 (The reflected rational response).

Lean statement: D5/S3/Analytic/Boundary/ActiveSemicircle.activeSemicircleResponse

Formalization. D5/S3/Analytic/Boundary/ActiveSemicircle.activeSemicircleResponse (✓ std3).

Source. Repository-derived.

Commentary.

The response adds the two reflected first-order rational terms with centers at horizontal coordinates delta and minus delta.

Theorem 1.2 (Negativity is exactly the open semicircle).

$\forall d e lt a \in Real (), g amma \in Real (), x \in Real (), t \in Real (), (0 < d e lt a \land (0 < x \land (x - d e lt a)^{2} + (t - g amma)^{2} \neq = 0)) \Rightarrow (a c t i v e S e mi c i rc l e R es p o n se (d e lt a, g amma, x, t) < 0 \Leftrightarrow (x)^{2} + (t - g amma)^{2} < (d e lt a)^{2})$

Proof. Machine-checked in Lean as D5/S3/Analytic/Boundary/ActiveSemicircle.active_semicircle_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source statement is made analytically well-formed by requiring positive delta, positive horizontal coordinate x, and a nonzero pole denominator. The last premise prevents Lean’s totalized division by zero from silently assigning a value at the pole.

A common denominator is strictly positive on this domain. Its numerator factors as two times x times the signed radial defect, so the response is negative exactly when the point is inside the circle of radius delta centered at the boundary coordinate gamma.

Theorem 1.3 (The non-pole semicircle boundary attains zero).

$\forall d e lt a \in Real (), g amma \in Real (), x \in Real (), t \in Real (), ((0 < d e lt a \land (0 < x \land (x - d e lt a)^{2} + (t - g amma)^{2} \neq = 0)) \land (x)^{2} + (t - g amma)^{2} = (d e lt a)^{2}) \Rightarrow a c t i v e S e mi c i rc l e R es p o n se (d e lt a, g amma, x, t) = 0$

Proof. Machine-checked in Lean as D5/S3/Analytic/Boundary/ActiveSemicircle.active_semicircle_boundary_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

On the bounding circle, away from the rational pole, the radial factor vanishes and the response is exactly zero. This supplies the equality case adjoining the strict negative interior.

Theorem 1.4 (The two axis endpoints lie on the zero boundary).

$\forall d e lt a \in Real (), g amma \in Real (), 0 < d e lt a \Rightarrow (((0)^{2} + (g amma - d e lt a - g amma)^{2} = (d e lt a)^{2} \land a c t i v e S e mi c i rc l e R es p o n se (d e lt a, g amma, 0, g amma - d e lt a) = 0) \land ((0)^{2} + (g amma + d e lt a - g amma)^{2} = (d e lt a)^{2} \land a c t i v e S e mi c i rc l e R es p o n se (d e lt a, g amma, 0, g amma + d e lt a) = 0))$

Proof. Machine-checked in Lean as D5/S3/Analytic/Boundary/ActiveSemicircle.active_semicircle_axis_endpoints (✓ std3). ∎

Source. Repository-derived.

Commentary.

The circle meets the critical axis at gamma minus delta and gamma plus delta. Both points satisfy the circle equation and attain zero response.

Theorem 1.5 (Left approach to the pole is unbounded below).

$\forall d e lt a \in Real (), g amma \in Real (), B \in Real (), 0 < d e lt a \Rightarrow (\exists x \in Real (), 0 < x \land (x < d e lt a \land a c t i v e S e mi c i rc l e R es p o n se (d e lt a, g amma, x, g amma) < B))$

Proof. Machine-checked in Lean as D5/S3/Analytic/Boundary/ActiveSemicircle.active_semicircle_response_unbounded_near_pole (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every real bound, an explicit point strictly between the critical axis and the pole has response below that bound. The construction uses x equals delta minus delta divided by n plus two.

Theorem 1.6 (A bounded background cannot preserve nonnegativity).

$\forall d e lt a \in Real (), g amma \in Real (), b \in Real () \to Real (), B \in Real (), (0 < d e lt a \land (\forall u \in Real (), (0 < u \land u < d e lt a) \Rightarrow b (u) \leq B)) \Rightarrow (\exists x \in Real (), 0 < x \land (x < d e lt a \land a c t i v e S e mi c i rc l e R es p o n se (d e lt a, g amma, x, g amma) + b (x) < 0))$

Proof. Machine-checked in Lean as D5/S3/Analytic/Boundary/ActiveSemicircle.active_semicircle_bounded_background_loses_nonnegativity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Any additional contribution bounded above between the axis and the pole is dominated by the negative divergence. Thus the total response is strictly negative at some nearby point.

References

Truth anchor: D5/S3/Analytic/Boundary/ActiveSemicircle.activeSemicircleResponse
Truth anchor: D5/S3/Analytic/Boundary/ActiveSemicircle.active_semicircle_axis_endpoints
Truth anchor: D5/S3/Analytic/Boundary/ActiveSemicircle.active_semicircle_boundary_zero
Truth anchor: D5/S3/Analytic/Boundary/ActiveSemicircle.active_semicircle_bounded_background_loses_nonnegativity
Truth anchor: D5/S3/Analytic/Boundary/ActiveSemicircle.active_semicircle_criterion
Truth anchor: D5/S3/Analytic/Boundary/ActiveSemicircle.active_semicircle_response_unbounded_near_pole

Keyboard shortcuts

trureturing Blueprint

Active Semicircle

Abstract

References