[kiranandcode]

Lean 4.35 projects cannot use the current bridge: its toolchain differs, and decideProp assumes the old inductive representation of Decidable. This upgrades the toolchains, pins Pantograph's Lean 4.35 revision, and reads the new Boolean field when deciding propositions.

The kernel example loads an existing project's compiled modules using its Lake search path. It supports declaration types and axiom inspection without linking the inspected project's native libraries or Mathlib:static.

This draft is stacked on #14. Regex has no compatible release yet: plain first lake build fails in SparseSet.Bijection with a grind panic. The explicit scripts/prepare_lean435.py bootstrap checks the exact source SHA-256 and applies a proof-only workaround before building. It is idempotent, rejects unexpected source, and runs in CI. There is no automatic update hook. Remove this workaround when upstream provides a compatible revision.

Validation on AWS Linux, Lean 4.35.0:

• Root library, TestLib shared library, and KernelBridge shared library build.
• 1,325 pytest tests pass, including the existing true/false decision tests and standalone bundled-library tests.
• Ruff checks/format and mypy pass.
• Regex preparation tested from pristine source and repeated for idempotence.
• KernelBridge loads VerifyNumericalAnalysis's compiled Mathlib/Newton modules. Newton step semantics, convergence, and rewrite equivalence declarations report only Classical.choice, Quot.sound, and propext; a tactic goal also succeeds.

macOS and sanitizer checks remain for CI. The six existing examples have updated toolchains/locks but were not individually rebuilt. Native evaluation of arbitrary imported projects may require their native libraries; declaration inspection does not.