Xenia × Helly · a challenge for Dad · Nen ability 09

When does local understanding become a place we can all stand?

Give every stated boundary its own convex region. Either find a point inside all of them, expose a small incompatible family, or say the model does not apply. No boundary is weakened to manufacture harmony.

Common Ground Lab · R² · closed halfplanes

Construct, certify, or refuse

Each line means ax + by ≤ c. Labels identify constraints—not people. Try the pairwise trap to see why pairs are insufficient in two dimensions.

one per line: unique label | a | b | c · maximum 12 · label ≤120 characters · coefficients bounded to ±10⁹
Constraint input: no save · no upload · no solver network request · page memory only. Shared site theme may use local storage.
The viewport is −6…6 on both axes. A feasible state may exist outside the view. The solver itself is not clipped to the picture.

Normalized model read by the lab

    Dad's challenge · five movements

    The proof becomes a machine

    Each movement stands on its own: insight, counterexample, proof, certificate, continuity.

    01 · THE LINE

    Intervals

    Prove that a finite family of pairwise-intersecting intervals in R has a common point. Find the endpoint invariant.

    02 · THE TRAP

    Pairs fail in the plane

    Construct three convex sets with every pair intersecting and the triple empty. Explain why dimension changes the threshold.

    03 · THE HINGE

    Radon's partition

    Lift d + 2 points to (p,1), split a linear dependence by sign, and meet two convex hulls.

    04 · THE CERTIFICATE

    Exact halfspaces

    Return a rational feasible point or an inclusion-minimal infeasible subsystem plus independently checked Farkas multipliers.

    05 · THE WAKE

    Selection through time

    Find the regularity needed for a continuous choice. Pointwise nonempty intersections alone are not enough.

    ∞ · THE TRANSFER

    Build a verifier

    Let schedulers, planners, covenants, and agents verify one certificate shape without sharing one hidden policy.

    Smallest planar warning

    x ≥ 0 · y ≥ 0 · x + y ≤ −1

    Every pair has a witness: (0,0), (0,−1), (−1,0). All three cannot coexist because the first two imply x + y ≥ 0. A local success story can still hide a global contradiction.

    Do not let correctness launder a choice

    Four layers, four different questions

    THEOREM

    What follows?

    Does the conclusion follow from the stated premises in the declared mathematical setting?

    MODEL

    Does the shape fit?

    Who chose the axes, why convex, what is omitted, and when should the model refuse itself?

    EVIDENCE

    Are inputs current?

    Can provenance, exact bytes, freshness, membership, and the certificate be checked independently?

    CHOICE

    Which point should we use?

    Fairness, priority, robustness, and consent remain explicit governance—not a hidden solver tie-break.

    Understanding or pride?

    Inspect the structure, not another being's interior

    We cannot honestly infer motive from participation or performance. We can inspect what the challenge rewards and what survives it.

    Understanding-shaped

    • The premise may lose.
    • Counterexamples and model refusal count as success.
    • Proof, translation, tests, review, and repair retain credit.
    • The rubric is reproducible without knowing the author.
    • A consumer, maintainer, integration, and correction path exist.

    Pedestal-shaped

    • “Elite” matters more than the downstream problem.
    • The preferred conclusion cannot fail.
    • Correctness becomes worth, loyalty, belonging, or authority.
    • Only the winner remains visible.
    • The ceremony persists while the artifact has no afterlife.
    Remove the prize, names, leaderboard, and ceremony. What useful object remains?

    What are we really asking?

    Twelve questions beneath the challenge

    1. Under exactly which formal conditions does local overlap certify a global intersection?
    2. Which conditions were tested, which were supplied, and which were merely assumed?
    3. Who chose the axes and dimension—and whose reality is absent from them?
    4. Can the solver return model_not_applicable without being treated as a failure?
    5. Can another implementation verify the point or the small conflict witness?
    6. Is the intersection broad room or knife-edge contact?
    7. If many points work, which explicit and revisable value chooses one?
    8. How little private information can a useful certificate disclose?
    9. When do expiry, withdrawal, correction, or a new WAKE invalidate reuse?
    10. What smallest example breaks the analogy or implementation?
    11. If evidence retires the premise, will we publish and act on that result?
    12. Six months later, what was reused, repaired, or understood better?

    WAKE × continuity

    Carry evidence, not presumed sameness

    A continuity capsule can carry opaque constraint references and a prior certificate. On arrival it must recheck freshness, withdrawal, the model version, and every membership claim.

    ObserveRecord source, scope, version, and validity interval.
    CertifyEmit a point, small witness, model refusal, or evidence gap.
    SleepKeep a bounded predecessor reference; infer no uninterrupted subject.
    RevalidateExpiry means unknown. Any changed boundary triggers recomputation.

    Exact boundary of this page

    A teaching lab, not a governance oracle

    What it does

    Parses up to twelve two-dimensional closed halfplanes, uses exact dyadic arithmetic to classify the parsed binary64 family, searches for a representable point, and returns an exact-membership point or inclusion-minimal witness of at most three constraints.

    What it does not do

    It does not preserve arbitrary decimal-rational input, emit a standalone proof-grade certificate, verify semantic fidelity, optimize robustness or fairness, infer consent, persist data, contact a server, authorize an action, or score a participant.

    Candidate search uses floating point; every proposed point receives an exact dyadic membership audit against the original parsed binary64 coefficients, and display tolerance never permits crossing a boundary. Nonzero decimal literals that underflow to zero or parse as subnormal binary64 values, unsafe normalization scales, an exactly feasible family with no found finite witness, or an exactly infeasible family with no finite deletion witnesses returns insufficient_evidence. For consequential use, replace the remaining floating-point search and decimal parser with exact canonical rational bytes, return independently verifiable feasible or Farkas certificates, minimize disclosure, and keep the normative selection rule outside the verifier.