> Full-text translation from Chinese. The original remains authoritative for its research claims; this translation is not independent mathematical verification.

# WSFC Round 12
## Generic Point-to-Segment Certificate Compiler: Automatic Feature Phases, Algebraic Root Isolation and First-Event Semantics

**English Title:** *Generic Point-to-Segment Certificate Compiler: Automatic Feature Phases, Algebraic Root Isolation, and First-Event Semantics*  
**Document ID:** `WSFC-R12-v0.1`  
**Version:** v0.1  
**Date:** 2026-09-23  
**Author:** Neo.K  
**AI Research Collaborator:** Aletheia / OpenAI GPT-5.6 Sol  
**Series:** Worm Sequence Freedom Closure  
**Prerequisite:** `WSFC-R11-v0.1`  
**Status:** `GENERIC COMPILER MVP / EXACT ROOT ISOLATION / SEMANTIC PHASE DECOMPOSITION`  
**Canonical Source:** UTF-8 Markdown

---

# Abstract

Round 11 corrected an important semantic bug:

$$
\boxed{
\text{supporting-line tangency}
\neq
\text{finite-segment contact}.
}
$$

Endpoint Slide safety therefore cannot be handled globally by a single supporting-line polynomial; it must be divided into phases according to the finite segment's nearest feature.

Round 12 generalizes this correction from the canonical example to a generic compiler.

Input:

$$
P_0,
\qquad
Q(t)=Q_0+tD,
\qquad
C,
\qquad
r,
\qquad
t\in[t_0,t_1].
$$

The first version requires all input coefficients to be rational.

Define:

$$
w=P_0-C,
$$

$$
v(t)=Q(t)-P_0.
$$

The compiler derives six core quantities exactly:

$$
A(t)=w\cdot v(t),
$$

$$
N(t)=\|v(t)\|^2,
$$

$$
S(t)=A(t)+N(t),
$$

$$
H_0=\|w\|^2-r^2,
$$

$$
L(t)
=
\operatorname{cross}(v(t),w)^2-r^2N(t),
$$

$$
H_1(t)
=
\|w+v(t)\|^2-r^2.
$$

The nearest feature is determined by:

$$
A(t),
\qquad
S(t),
\qquad
N(t)
$$

Safety uses the following phase-dependent quantities:

```text
FIXED_ENDPOINT
    -> H0

INTERIOR_PROJECTION
    -> L(t)

MOVING_ENDPOINT
    -> H1(t)

DEGENERATE_SEGMENT
    -> point-state branch
```

The compiler collects all real roots of:

- $A=0$;
- $S=0$;
- $N=0$;
- $L=0$;
- $H_1=0$

within the parameter domain.

Under affine motion their degrees are at most $2$, so the roots can be computed exactly; irrational roots retain an algebraic expression and a rational isolating interval.

All roots, together with the domain endpoints, form:

$$
\boxed{
\text{atomic parameter cells}.
}
$$

Inside every open cell:

- the nearest feature is unchanged;
- the active safety polynomial has no root;
- the safety sign is fixed.

The generic compiler can therefore automatically output:

```text
derived polynomials
exact/algebraic roots
isolating intervals
atomic cells
nearest feature per cell
active safety polynomial
safety sign
certificate-only boundaries
actual geometric events
first actual geometric event
proof DAG
```

The compiler in this round has passed two types of test.

### Test A — Round 11 canonical example

It automatically recovers:

$$
\boxed{
t=\frac12
}
$$

as the nearest-feature switch,

$$
\boxed{
t=\frac67
}
$$

as supporting-line tangency only,

and:

$$
\boxed{
t=1
}
$$

as the first actual collapse/contact.

### Test B — Irrational endpoint contact

Take:

$$
P_0=(3,0),
$$

$$
Q(t)=
\left(
2-t,\frac12
\right),
$$

a unit disc at the origin, and

$$
t\in[0,2].
$$

The compiler automatically finds the first actual contact:

$$
\boxed{
t_\star
=
2-\frac{\sqrt3}{2}.
}
$$

This is not a rational root.

The output retains all of:

```text
exact algebraic expression
decimal approximation
rational isolating interval
```

Thus Round 12 demonstrates for the first time that the compiler does not depend on a canonical toy case that happens to factor into rational roots.

---

# 1. Generic Input

First version:

```text
P0
Q0
D
C
r
parameter_interval
```

where:

$$
Q(t)=Q_0+tD.
$$

All scalar inputs use:

$$
\mathbb Q.
$$

---

# 2. Core Polynomials

## Dot Guard

$$
\boxed{
A(t)=w\cdot v(t).
}
$$

Degree:

$$
\le1.
$$

## Segment Norm

$$
\boxed{
N(t)=\|v(t)\|^2.
}
$$

Degree:

$$
\le2.
$$

## Projection Switch

$$
\boxed{
S(t)=A(t)+N(t).
}
$$

Degree:

$$
\le2.
$$

## Fixed Endpoint Safety

$$
\boxed{
H_0=\|w\|^2-r^2.
}
$$

Constant.

## Interior Safety

$$
\boxed{
L(t)
=
\operatorname{cross}(v(t),w)^2-r^2N(t).
}
$$

Degree:

$$
\le2.
$$

## Moving Endpoint Safety

$$
\boxed{
H_1(t)
=
\|w+v(t)\|^2-r^2.
}
$$

Degree:

$$
\le2.
$$

The entire generic segment certificate compiler therefore needs only quadratic algebra.

---

# 3. Nearest Feature Classifier

When:

$$
N(t)>0,
$$

we have:

$$
\boxed{
A(t)\ge0
\Rightarrow
\texttt{FIXED\_ENDPOINT}.
}
$$

If:

$$
A(t)<0,
$$

and:

$$
S(t)\ge0,
$$

then:

$$
\boxed{
\texttt{INTERIOR\_PROJECTION}.
}
$$

If:

$$
S(t)<0,
$$

then:

$$
\boxed{
\texttt{MOVING\_ENDPOINT}.
}
$$

If:

$$
N(t)=0,
$$

then:

$$
\boxed{
\texttt{DEGENERATE\_SEGMENT}.
}
$$

This is the feature state machine for a finite segment.

---

# 4. Root Set

The compiler does not look only for feature-switch roots.

The complete root set is:

$$
\boxed{
R
=
R_A
\cup
R_S
\cup
R_N
\cup
R_L
\cup
R_{H_1}.
}
$$

Here:

- $R_A$: fixed/interior phase boundaries;
- $R_S$: interior/moving-endpoint phase boundaries;
- $R_N$: segment collapse;
- $R_L$: line-clearance roots;
- $R_{H_1}$: moving-endpoint contact roots.

Include the domain endpoints as well.

---

# 5. Atomic Cells

Order the boundaries:

$$
t_0
=
\rho_0
<
\rho_1
<
\cdots
<
\rho_m
=
t_1.
$$

The atomic cells are:

$$
I_j
=
(\rho_j,\rho_{j+1}).
$$

No cell contains a root of any feature or safety polynomial.

Its sign vector is therefore fixed.

The compiler needs only one rational sample:

$$
\tau_j\in I_j
$$

to determine, throughout the cell:

```text
nearest feature
active safety polynomial
safety sign
```

This is a finite algebraic decomposition.

---

# 6. Algebraic Root Isolation

A quadratic irrational root is not converted into floating-point authority.

Retain:

```text
exact
approx
isolating_interval
```

For example, Test B gives:

$$
\boxed{
2-\frac{\sqrt3}{2}
}
$$

with a rational isolating interval.

Root comparison and phase ordering can therefore be progressively upgraded to a proof-assistant or interval-certified implementation.

---

# 7. Certificate Boundary vs. Actual Event

Every root carries its sources.

For example:

```text
projection_switch
supporting_line_clearance
moving_endpoint_clearance
norm_v_sq
```

The compiler then uses nearest-feature semantics to decide:

- whether a root is merely a certificate boundary;
- whether it is actual finite-segment contact;
- whether it is vertex collapse;
- whether several events occur simultaneously.

Thus:

$$
L(t)=0
$$

is no longer automatically treated as segment contact.

---

# 8. Canonical Test A

The compiler output for the Round 11 example recovers:

```text
1/2:
  NEAREST_FEATURE_SWITCH

6/7:
  SUPPORTING_LINE_TANGENCY_ONLY

1:
  VERTEX_COLLAPSE
  MOVING_ENDPOINT_CONTACT
```

The first actual event is:

$$
\boxed{
t=1.
}
$$

---

# 9. Irrational Test B

Take:

$$
P_0=(3,0),
$$

$$
Q(t)=
\left(
2-t,\frac12
\right).
$$

Moving-endpoint clearance is:

$$
H_1(t)
=
(2-t)^2+\frac14-1.
$$

Hence:

$$
H_1(t)=0
$$

gives:

$$
t
=
2\pm\frac{\sqrt3}{2}.
$$

The first contact within the domain:

$$
[0,2]
$$

is:

$$
\boxed{
2-\frac{\sqrt3}{2}.
}
$$

The compiler correctly labels it:

```text
ALGEBRAIC ROOT
MOVING_ENDPOINT_CONTACT
```

and outputs an isolating interval.

---

# 10. First Actual Event

The compiler does not use:

> the smallest polynomial root

as its first event.

Instead, it uses:

$$
\boxed{
\min
\{
t:
\text{root is active under finite-segment semantics}
\}.
}
$$

Consequently:

- inactive line tangency does not count;
- a feature switch does not count;
- collapse counts;
- active endpoint/interior contact counts.

This generalizes Round 11's semantic correction.

---

# 11. Proof DAG

The compiler output includes:

```text
derive polynomials
isolate roots
partition parameter domain
classify feature per cell
verify active safety sign
classify boundary roots
select first actual event
```

Every compilation therefore generates a theorem-responsibility trace as well.

---

# 12. Reference Compiler

This round establishes:

```text
wsfc_point_segment_certificate_compiler.py
```

It takes a JSON specification as input.

Output format:

```text
WSFC-SEGCOMP-0.1
```

The compiler itself uses:

```text
SymPy QQ polynomials
real_roots
rational isolating intervals
```

rather than a numerical root finder.

---

# 13. Formalization Target

The Lean draft adds generic primitives:

```text
NearestFeature
H
A
N
S
lineClearance
complete_square
classify_nearest_feature_TARGET
interior_phase_safe_TARGET
compiler_output_sound_TARGET
```

Here `complete_square` is already a ring-level no-sorry candidate.

The actual remaining formal challenge is:

> Formalize the atomic-cell root ordering and sign certificates generated at runtime into an acceptable finite partition.

---

# 14. A Compiler Is Not a Theorem Prover

The reference compiler can:

- derive exactly;
- isolate roots exactly;
- sample signs;
- build a DAG.

But a generic soundness theorem still needs proofs that:

> the roots are complete;
> signs are invariant in a root-free cell;
> the nearest-feature classifier is correct;
> the active safety sign implies safety of the entire finite segment.

The status is therefore:

```text
COMPILER IMPLEMENTED
CANONICAL/ALGEBRAIC TESTS PASS
GENERIC FORMAL SOUNDNESS OPEN
```

---

# 15. Next Step

The most natural work for Round 13 is not to introduce still more geometry.

Instead, it is:

$$
\boxed{
\textbf{Compiler Soundness Layer}.
}
$$

Priority proofs:

1. degree-$2$ root completeness;
2. root-free interval sign invariance;
3. atomic-cell nearest-feature invariance;
4. the phase safety theorem;
5. an exact/algebraic root-ordering certificate;
6. output DAG soundness.

This would make:

$$
\boxed{
\text{compiler output}
\Rightarrow
\text{finite-segment safety theorem}
}
$$

a generic target for the first time.

---

# Conclusion

Round 12 upgrades Round 11's manual correction into a generic compiler.

A finite-segment transition no longer relies on manually deciding:

$$
\boxed{
\text{which feature is nearest?}
}
$$

Instead, polynomial signs determine it automatically.

The overall workflow is:

$$
\boxed{
\text{Affine Motion}
\rightarrow
\text{Quadratic Polynomials}
\rightarrow
\text{Exact Root Isolation}
\rightarrow
\text{Feature Phases}
\rightarrow
\text{Phase Safety}
\rightarrow
\text{Actual Event}
\rightarrow
\text{Proof DAG}.
}
$$

This gives the WSFC Geometry State Runtime the beginnings of actual generic certificate-compilation capability.

===END===