IR061 — Exponential jet identity

For x_ell=ell*L/2, exp((i+j*sqrt2)*x_ell)=(sqrt2)^(i*ell)*c^(j*ell); jets multiply by (i+j*sqrt2)^k. Prove this through finite exponential identities and tails.

Method: native-ring. Induction: none. Risk: high.

This is a human-readable planning contract, not a parsed kernel formula or accepted proof.

Planned prerequisites and notation

• IR027 — Identification with the requested constant
• IR022 — Exponential addition and integer powers
• IR033 — Quadratic powers and coefficient height
• IR058 — Polynomial-to-exponential tail transfer
• IRD16 — AuxJet
• IRD19 — NodeBracket