Repository navigation
docs(13410): 3 lecture cells chiffrees (XOR/AND, palindrome, conservation) in Z3-Python-03-Tactics (density 1051 -> 1267) - #16621
Conversation
…tion) in Z3-Python-03-Tactics (density 1051 -> 1267)
Anchored readings (all on real executed outputs, no exercise stubs):
- lectz3tac-01 (after Interpretation vecteurs de bits, anchored on cell
db8a4ca1 output): a=254/b=1 are exact bitwise complements; XOR=11111111
implies AND=00000000 (second constraint redundant); 2^8=256 valid pairs,
Z3 returns one. Non mesure: model-choice criterion.
- lectz3tac-02 (after palindrome cell 8989b5f3 output): 01000010 = 64+2 =
66 recomposed; bit-by-bit symmetry verified; sat = one arbitrary model
(00100100 = 36 also valid), not a minimum - Optimize absent. Non mesure:
total model count.
- lectz3tac-03 (after transfer cell 0ece8020 output): deltas +30/-30/0 sum
to zero; totals 350 = 350 recomposed; sat proves coherence on the fixed
concrete state only, not for all initial states (unsat-of-negation would
be required). Non mesure: solve time.
Proofs: originals deep-equal in order (32 kept / 35 total, new ids
filtered); all 14 code cells byte-identical (source+outputs);
json.dumps(indent=1,ensure_ascii=False)+"\n" == raw before AND after;
my insertion diff has 0 deletion lines; ids lectz3tac-01..03 strictly
alphanumeric+dash (nbformat 4.5), metadata {}, lines end \n except last.
Accent register 0.48% < 1.5% -> unaccented French matched.
Hook disclosure: pre-commit fix-hr-separator normalized ONE pre-existing
line in header cell 024ee023 ('---' -> '***', setext-hazard rule). Not
part of the grain content; re-staged and re-committed per protocol.
All other originals untouched (verified post-hook: only 024ee023 differs,
single line 19).
Density measured separately post-insertion: 1267 (threshold 1200,
below_threshold count 0).
See #13410
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
|
closing-keyword + PR-number reference(s) that would auto-close a PR on squash: [' GitHub interprète Le discriminateur est la nature du numéro, pas le contexte du mot-clé : Pour passer ce gate :
|
Golden-Set Execution (H.7 P3)✅ 8/8 notebooks passed (certified reproducible)
Pinned lockfile: |
github-actions
Bot
added
the
variation-adjacency-deep-med
|
✅ No prose/output mismatch detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
…only density tranche Pair attested: Z3-Python-03 Tactics (SMT/Z3-API). Paraphyte-preservant verification (python-compare vs origin/main): all code cells byte-identical (source + outputs + execution_count) — 14/14; changes are markdown-only additions (+3 cells). Command run: python scripts/notebook_tools/check_twin_parity.py --update --pair "Z3-Python-03 Tactics" --by "myia-po-2026:CoursIA" Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
2 participants
Grain: DEEP/notebook-python -- lane myia-po-2026:CoursIA -- prev: DEEP/ci-fix (See #16615)
Summary
Density grain EPIC #13410 on
MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-Python-03-Tactics.ipynb(Python kernel, fresh SMT family for this lane). Three reading cells anchored on real executed outputs, one per code section previously flowing into a section header (or thin interpretation) without numeric reading.Content
db8a4ca1output): the printed paira = 254 (binaire : 11111110)/b = 1 (binaire : 00000001)are exact bitwise complements;a XOR b = 11111111impliesa AND b = 00000000(second constraint redundant); solution space = 2^8 = 256 pairs, Z3 returns one. Non mesure: model-choice criterion.8989b5f3output):01000010= 64 + 2 = 66 recomposed; bit-by-bit symmetry (b7=b0, b6=b1, b5=b2, b4=b3);sat= one arbitrary model among several (00100100 = 36 also valid), not a minimum —Optimizeabsent. Non mesure: total model count.0ece8020output): deltas +30 / -30 / 0 sum to zero; totals350=350recomposed;satproves coherence on the fixed concrete state only, not for all initial states. Non mesure: solve time.No exercise stub anchored (cells d679f119/e6f8fc07/2b4b4d43 untouched and un-restated). Accent register measured 0.48% < 1.5% -> unaccented French.
Proofs
json.dumps(nb, indent=1, ensure_ascii=False)+"\n"== raw before AND after edit.git diff -U0 | grep -c '^-[^-]'== 0.lectz3tac-01..03strictly alphanumeric+dash (nbformat 4.5, incident enrich(iit,#13410): densite ICT dissociation PhAT self-reference + saillance/pregnance — lectures de sorties chiffrees #16427), metadata {}, each line ends \n except last.fix-hr-separatornormalized ONE pre-existing line in header cell024ee023(---->***, setext-hazard rule); re-staged and re-committed per protocol (the commit's single deletion line).Test plan
pedagogy_density.py --jsonon the notebook: ok, density 1267 >= 1200See #13410
🤖 Generated with Claude Code