# Mathematical construction and exact optimization

## 1. Quantifiers before intelligence estimates

Fix authorized public information d, low state l, protected high state h, and an
adversarial action a. The desired local law is

    (next_low(l,h,a), observation(l,h,a)) = reference(l).

This universally quantifies over high states and actions. It does not bound the
attacker's planning quality, reasoning speed, or familiarity with the design.
Induction then equates every finite public transcript generated from the same
low state and public input schedule. Adaptive choices are included: the local
law holds for every action after every compatible history.

The equality must include next LOW state. Equality of only the current output
can leave hidden differences that become observable later. A fixed number of
release slots comes from the public schedule, not the adversary's decision to
halt. Different high-side execution lengths must be hidden within those slots.

For a stochastic version, require equality of conditional output/low-transition
kernels, including relevant receiver side information. The deterministic law in
this prototype is a stronger pointwise construction for its listed observations.
It is not a formalization of Shannon entropy in Lean.

## 2. A useful canonical gate

Let f(x) be a uniquely defined authorized result. Let V(x,y) be a private, bounded
verifier satisfying

    V(x,y)=true implies y=f(x).

Release the accepted y, or compute f(x) independently if the proposal is absent
or invalid. All branches return f(x). Serialize it canonically and release it at
a public deadline. Verification time, proof text, diagnostics, process failure,
and whether fallback ran are not public outputs.

This is a total fallback construction, NOT merely fail-closed rejection. An
externally visible rejection creates a success-versus-failure bit. A sound
verifier alone does not remove that bit.

`lab.py` includes a nonconstant useful example: sort an integer list. A proposed
sorted list is accepted only when its order and exact multiset are correct;
otherwise the trusted path sorts the original list. All 65,792 small-domain
input/proposal cases returned the authorized sorted result. This verifies a
finite demonstrator, not a hardware gate or an asymptotic proof about the Python
implementation. The generic Lean theorem assumes verifier soundness and does not
formalize this particular Python verifier.

The benefits and costs must be honest. This pattern can use an untrusted worker
to reduce private trusted computation when checking is cheaper than discovery.
It does not guarantee a latency benefit under public fixed-deadline release.
Observable power or reclaimed CPU capacity must not reintroduce the distinction.
A universal bounded-deadline fallback for arbitrary scientific discovery is not
constructed here.

## 3. A robust thermal existence certificate

We model temperature deviation from a trusted operating reference by

    theta[t+1] = a[t] theta[t] + b(s,r) u[t] + w[t],

with

    0 <= a[t] <= rho = 9/10,
    |u[t]| <= P = 1,
    |w[t]| <= eta = 1/1000,
    b(s,r) = max(0,20-2s-r)/1000.

s and r are nonnegative integer control settings in an illustrative catalogue.
s represents attenuation effort; r represents regulation effort. They are NOT
meters, watts, or known parameters of the BitWhisper experiment. The affine
bound, cost, and utility are assumed inputs used to demonstrate synthesis.

The untrusted receiver sees only a trusted quantized health observation:

    -1 if theta <= -55/1000,
     0 if |theta| < 55/1000,
    +1 if theta >= 55/1000.

Raw sensor values, analog heat sensing, independent clocks, and thermal effects
on observable throttling/fans/latency are NOT available in this observation
model. This is an explicit restriction and a deployment obligation, not an
inference that physical heat flow vanishes.

A general invariant is obtained by finding R such that

    |theta[0]| <= R,
    rho R + b P + eta <= R < m,

where m is the distance to the nearest quantizer threshold. Then

    |theta[t+1]| <= rho |theta[t]| + b P + eta <= R,

so every allowed action and disturbance sequence keeps the public observation
at zero for every time. This includes adversarially chosen load sequences and
variation of a[t] anywhere within its bound.

The minimum invariant radius after a zero initial state is

    R_* = (b P + eta)/(1-rho).

At s=7,r=2, b=4/1000 and R_*=1/20. Explicitly,

    (9/10)(1/20) + 4/1000 + 1/1000 = 1/20 < 55/1000.

Thus the winner has a 5/1000 margin from the observation threshold. The winning
invariant also permits any initial state with magnitude at most 1/20. The
configuration search and counterexample trajectories use zero initialization.

This is zero distinguishability of the modeled quantized thermal observation,
not merely a small empirical bitrate. Raw thermal trajectories are still
different. A test explicitly checks that the protected public traces coincide
while their raw temperature trajectories differ.

## 4. Why the integer feasibility condition is exact in this catalogue

Write g=max(0,20-2s-r). Then

    R_* = (g+1)/100.

The strict observation condition R_* < 55/1000 holds exactly when the integer
residual gain g <= 4, equivalently

    2s+r >= 16.

All settings violating this condition have g>=5. Under the same permissible
constant disturbance w=1/1000, compare u=0 and u=1. The quiet trajectory stays
below the threshold. For the least unsafe gain g=5, the hot trajectory is

    theta[t] = (3/50) (1-(9/10)^t).

At step 23 it is below 55/1000; at step 24 it exceeds that threshold. Larger
integer g crosses no later. Exact Fraction arithmetic checks every such setting.
The near-miss s=7,r=1 therefore leaks a distinguishable bit by step 24, despite
passing a shorter observation test.

The stronger all-time safety result does not come from these finite tests. It
comes from the invariant inequality. The finite tests give counterexamples to
all failing integer settings in the original catalogue.

## 5. The solved optimization

Assume hardening cost and useful-service score

    J(s,r)=s^2+2r^2,
    U(r)=100-5r,

and require U>=80, so r<=4. These are declared engineering-model curves, not
measurements of actual throughput or model capability. Output correctness is
100% for admitted tasks in the abstract total-fallback model; service score is
a separate, assumed performance objective.

The variable-cost problem is

    minimize s^2+2r^2
    subject to s,r natural numbers,
               2s+r>=16,
               r<=4.

The digital core has five switches. Each missing control leaves a separately
observable coordinate, with explicit action-pair witnesses. Consequently all
five are mandatory in this catalogue and their fixed cost is irrelevant to the
thermal argmin. There are 32*11*5=1760 tested configurations. The s<=10 range is
not concealing a better solution: at s=10 residual gain is already zero, so any
larger s is dominated by s=10 at equal r.

### Global lower bound, independent of enumeration

For all real s,r,

    9(s^2+2r^2) = 2(2s+r)^2 + (s-4r)^2.

If s,r>=0 and 2s+r>=16, then

    J(s,r) >= 512/9 = 56 + 8/9.

For integer s,r the cost is an integer, hence J>=57. The feasible witness
(s,r)=(7,2) has cost 49+8=57 and service score 90. It therefore attains the global
minimum, not merely the best observed value.

The continuous relaxation is minimized at s=64/9,r=16/9, with cost 512/9. The
integer witness's cost exceeds that continuous optimum by only 1/9.

The source-level Lean proof uses a different elementary argument: for s>=8,
s^2>=64; for s=0,...,7, feasibility forces a corresponding lower bound on r and
its square. This establishes the same all-natural-number bound without requiring
Mathlib's polynomial tactics. It now kernel-checks under Lean 4.19.0; see the publication receipt.

### Utility frontier

At a service-score floor of 80 or 90, the optimum is (7,2), cost 57, score 90.
Requiring the full score 100 forces r=0 and s>=8; (8,0) has cost 64. The two
nondominated cost/service choices in the base model are therefore (57,90) and
(64,100). Neither is a universal recommendation: the objective determines the
appropriate point.

## 6. Sensitivity and robustness

The exact search was repeated with one changed envelope parameter at a time:

| Change | Least-cost certified setting | Cost | Declared service score |
|---|---|---:|---:|
| Base envelope | s=7,r=2 | 57 | 90 |
| Disturbance bound doubled | s=8,r=1 | 66 | 95 |
| rho raised from .90 to .92 | s=8,r=1 | 66 | 95 |
| Adversarial load bound doubled | s=8,r=2 | 72 | 90 |

Every changed scenario invalidates the original winner's certificate. Each new
winner was independently checked for the absence of a cheaper integer candidate,
using an objective-derived bounding box rather than the optimizer's search box.
For these changed envelopes the search optimizes the stated invariant-certificate
class; it does not assert every uncertified setting is physically insecure.

This is the deployment method: measure or otherwise justify conservative
parameter bounds, synthesize the optimum for those bounds, then revalidate when
the bounds change. Nominal averages are not adversarial envelopes.

## 7. Lean coverage and remaining obligations

The kernel-checked source covers canonical release under a soundness hypothesis,
trace composition from a low-state/output unwinding law, digital-core output
independence and five negative controls, an integer envelope invariant, exact
near-miss arithmetic, and a globally optimal feasible integer witness.

The integer envelope rounds upward in milli-temperature units:

    M[0]=0,
    M[t+1]=ceil(.9 M[t]+g+1).

For g<=4, M<=50 is invariant. The kernel-checked Lean source establishes this integer
recurrence property. The real-valued recurrence-to-ceiling-envelope argument,
concrete implementation refinement, sensor mediation, and physical calibration
are not machine-checked. No claim of novelty is made for the underlying invariant
or integer-optimization techniques; the contribution here is this explicit
combined benchmark, executable search, counterexamples, and certificate packet.