TFPT scientific source excerpt
Original repository path: experiments/theory-contracts/clock-source-twist-transport-20261015/PROOF.md
Original file SHA-256: 9d3b3ba713b1a2ef450b5287dc15baf7c29fac224365f6b5ee70f39a261baebc
Inclusive original lines: 44-76
Line numbers below refer to the original source.
This bounded excerpt is source evidence; it is not a new proof/checker run.
Conversation metadata and personal execution details are omitted where indicated.

000044 | made by this contract.
000045 | 
000046 | ## 2. A fixed-source affine lift fails for an exact reason
000047 | 
000048 | Let A be a lattice isometry and suppose an affine action p -> Ap+r preserves
000049 | the *same* displayed K_delta for every p, with no oscillator or Hamiltonian
000050 | change. Comparing linear coefficients in p gives necessarily
000051 | 
000052 |     A^T(r+delta)=delta,  hence r=A delta-delta.
000053 | 
000054 | The constant then vanishes because |A delta|=|delta|. To map Ls onto itself,
000055 | r must belong to Ls. For an isometry with A²=-I this entails
000056 | 
000057 |     (I+A)r = -2 delta in Ls.
000058 | 
000059 | But adjacent coordinates of 2 delta differ by 1/4, whereas coordinate
000060 | differences of every Ls vector are integers. Consequently 2 delta is not in
000061 | Ls, for any alpha. There is **no affine charge-lattice lift of any such A**
000062 | which preserves this same K_delta. This includes every lattice-conjugate of
000063 | the actual J when both objects are compared in the same source frame.
000064 | 
000065 | For alpha=1/4 the checker obtains explicitly
000066 | 
000067 |     delta=(-15,-11,-7,-3,1,5,9,13)/32,
000068 |     J delta-delta=(13,-2,5,-2,-3,-2,-11,-2)/16, not in Ls.
000069 | 
000070 | This excludes the specified fixed-sector affine identification. It does not
000071 | exclude a clock which transports backgrounds, an operator with another
000072 | specified charge action, or a larger source construction. A clock action
000073 | does not in general have to commute with one fixed Hamiltonian.
000074 | 
000075 | Keeping the original fixed q does not rescue that identification:
000076 | Jq=(-1,1,-1,1,-1,1,-1,1) is not q. No affine constant can remove the