TFPT scientific source excerpt
Original repository path: documents/experiments--lean4-carrier-rigidity--note_carrier_rigidity_lean4/sections/004-section-interface-table-tfpt-paper-2-texorpdfstring-left.tex
Original file SHA-256: f2ea10f3093559607504bf934d02a75194293319594aed0e72e3296e8e21d756
Inclusive original lines: 167-190
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.

000167 | \paragraph{What remains is upstream TFPT theory work.}
000168 | The Lean chain takes the Stage D quadruple
000169 | $(\omega, \texttt{ContractionInjective},
000170 | \texttt{ContractionSurjective}, \texttt{Nontrivial}\,E_-)$
000171 | as input. The remaining open question is whether TFPT itself
000172 | produces such a quadruple from the boundary kernel. Concretely:
000173 | 
000174 | \begin{itemize}[leftmargin=1.6em, itemsep=1pt]
000175 | \item \emph{Existence of $\omega$.}\ Paper 2's Yukawa-type
000176 |     argument should produce an explicit alternating trilinear
000177 |     form on $E_-$. This is a representation-theoretic statement
000178 |     about the boundary kernel output, not a Lean engineering
000179 |     statement.
000180 | \item \emph{Verification of the two predicates.}\ Once $\omega$
000181 |     is constructed, the two predicates need to be checked.
000182 |     These checks are local algebraic statements (injectivity:
000183 |     no nonzero $v$ vanishes against all wedges; surjectivity:
000184 |     every dual functional on $\Lambda^2 E_-$ is realised as a
000185 |     contraction).
000186 | \end{itemize}
000187 | 
000188 | Neither task requires modifying the present Lean chain. They are
000189 | TFPT mathematical work, properly upstream of this experiment.
000190 |