Skip to content

Can two systems make a shared term precise?

The finite checker either finds a rule that preserves the declared cases, returns a safe partial answer, preserves an authorized choice, or shows why the term is not determined by the shared fields.

Problem being tested

Two systems may use a shared term while their local rules leave its joint meaning underdetermined. An unchecked model can suggest a bridge, but cannot establish that the bridge stays inside the shared vocabulary, preserves protected consequences and refusals, or avoids creating new authority.

Mathematical and institutional boundary

FRSL-1 is a finite relational language. The reference engine exhaustively checks its declared finite structures. A full package defines the target on that model class. A partial package certifies disjoint RELY and REFUSE regions and routes the residual to ESCALATE. Same-reduct expansions with different target values certify fixed-language non-definability. Inequivalent admissible minima remain CHOICE_REQUIRED; the engine does not convert mathematical non-uniqueness into institutional selection.

Run the source profile

$ bulla experimental invent bulla/examples/invention/definable.json -o result.json
$ bulla experimental verify-invention bulla/examples/invention/definable.json result.json
$ bulla experimental explain-invention result.json

The command surface is experimental. In the 0.44 release line it is available from source, not promised as a stable package API.

What the verifier establishes

  • the result binds the exact problem, synthesis policy, verifier, and package or certificate;
  • emitted formulas use only the permitted shared vocabulary;
  • full and partial regions satisfy their finite semantic obligations;
  • protected consequences and prior refusal cells are preserved;
  • objective countermodels replay independently; timeout or incomplete search remains resource indeterminacy.

SMTInterpol and model-generated candidates are untrusted accelerators. The exhaustive semantics and standalone checker control acceptance.

What the supplied evidence supports

Availability: experimental code ships in Bulla 0.44.1 under bulla.experimental; it is not part of the stable API. Evidence: team-authored finite cases, machine-planted oracles, internal replay, bounded finite models, and stated completeness assumptions. The finite Lean spine and executable checks do not establish a constructive Beth theorem for geometric sites, an end-to-end verified JSON-to-Lean compiler, unbounded first-order extraction, foreign-domain generality, or open-world completeness.

Read the public research record: Interpolant Envelope. See all maturity boundaries on What Exists Today.